HepLean Documentation
Init
.
Data
.
Nat
.
MinMax
Search
Google site search
return to top
source
Imports
Init.ByCases
Imported by
Nat
.
min_eq_min
Nat
.
min_comm
Nat
.
instCommutativeMin
Nat
.
min_le_right
Nat
.
min_le_left
Nat
.
min_eq_left
Nat
.
min_eq_right
Nat
.
le_min_of_le_of_le
Nat
.
le_min
Nat
.
lt_min
Nat
.
max_eq_max
Nat
.
max_comm
Nat
.
instCommutativeMax
Nat
.
le_max_left
Nat
.
le_max_right
min lemmas
#
source
theorem
Nat
.
min_eq_min
{b :
Nat
}
(a :
Nat
)
:
a
.min
b
=
min
a
b
source
theorem
Nat
.
min_comm
(a b :
Nat
)
:
min
a
b
=
min
b
a
source
instance
Nat
.
instCommutativeMin
:
Std.Commutative
min
Equations
Nat.instCommutativeMin
=
⋯
source
theorem
Nat
.
min_le_right
(a b :
Nat
)
:
min
a
b
≤
b
source
theorem
Nat
.
min_le_left
(a b :
Nat
)
:
min
a
b
≤
a
source
theorem
Nat
.
min_eq_left
{a b :
Nat
}
(h :
a
≤
b
)
:
min
a
b
=
a
source
theorem
Nat
.
min_eq_right
{a b :
Nat
}
(h :
b
≤
a
)
:
min
a
b
=
b
source
theorem
Nat
.
le_min_of_le_of_le
{a b c :
Nat
}
:
a
≤
b
→
a
≤
c
→
a
≤
min
b
c
source
theorem
Nat
.
le_min
{a b c :
Nat
}
:
a
≤
min
b
c
↔
a
≤
b
∧
a
≤
c
source
theorem
Nat
.
lt_min
{a b c :
Nat
}
:
a
<
min
b
c
↔
a
<
b
∧
a
<
c
max lemmas
#
source
theorem
Nat
.
max_eq_max
{b :
Nat
}
(a :
Nat
)
:
a
.max
b
=
max
a
b
source
theorem
Nat
.
max_comm
(a b :
Nat
)
:
max
a
b
=
max
b
a
source
instance
Nat
.
instCommutativeMax
:
Std.Commutative
max
Equations
Nat.instCommutativeMax
=
⋯
source
theorem
Nat
.
le_max_left
(a b :
Nat
)
:
a
≤
max
a
b
source
theorem
Nat
.
le_max_right
(a b :
Nat
)
:
b
≤
max
a
b