Mathematics in Lean
1. イントロダクション
2. 基礎
3. 論理
4. Sets and Functions
5. Elementary Number Theory
6. Structures
7. Hierarchies
8. Topology
9. Differential Calculus
10. Integration and Measure Theory
Index
Mathematics in Lean
Index
Index
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
実
A
absolute value
absurd
anonymous constructor
apply
,
[1]
assumption
B
bounded quantifiers
by_cases
by_contra
C
calc
cases
change
check
command
open
commands
check
commutative ring
congr
constructor
continuity
contradiction
contrapose
convert
D
definitional equality
differential calculus
divisibility
dsimp
E
elementary calculus
erw
exact
,
[1]
,
[2]
excluded middle
exfalso
exponential
ext
extensionality
F
field_simp
Filter
from
G
gcd
goal
group (algebraic structure)
(tactic)
H
have
,
[1]
I
implicit argument
inequalities
injective function
integration
,
[1]
intro
L
lambda abstraction
lattice
lcm
left
let
linarith
local context
logarithm
M
max
measure theory
metric space
,
[1]
min
monotone function
N
namespace
norm_num
normed space
O
open
order relation
P
partial order
proof state
push_neg
R
rcases
reflexivity
repeat
rewrite
rfl
right
ring (algebraic structure)
(tactic)
rintro
rw
,
[1]
rwa
S
set operations
show
simp
,
[1]
surjective function
T
tactic
field_simp
tactics
abel
apply
,
[1]
assumption
by_cases
by_contra and by_contradiction
calc
cases
change
congr
constructor
continuity
contradiction
contrapose
convert
dsimp
erw
exact
,
[1]
,
[2]
exfalso
ext
from
group
have
,
[1]
intro
left
let
linarith
noncomm_ring
norm_num
push_neg
rcases
refl and reflexivity
repeat
right
ring
rintro
rw and rewrite
,
[1]
rwa
show
simp
,
[1]
use
this
topological space
topology
U
use
実
実数