Documentation
Leroy
.
Measure
.
Aux
Search
return to top
source
Imports
Init
Leroy.Further_Topology
Mathlib.Data.Real.Basic
Mathlib.Order.BoundedOrder.Basic
Imported by
sInf_epsilon_eq_zero
sInf_epsilon_eq_zero'
source
theorem
sInf_epsilon_eq_zero
:
sInf
{
ε
:
ℝ
|
ε
>
0
}
=
0
source
theorem
sInf_epsilon_eq_zero'
:
sInf
{
ε
:
NNReal
|
ε
>
0
}
=
0