Documentation
MeanFourier
.
Mathlib
.
Basic
.
Real
.
ENatENNReal
Search
return to top
source
Imports
Init
Mathlib.Basic.Real.ENatENNReal
Imported by
ENat
.
toENNReal_le_natCast
source
@[simp]
theorem
ENat
.
toENNReal_le_natCast
{
m
:
ℕ∞
}
{
n
:
ℕ
}
:
↑
m
≤
↑
n
↔
m
≤
↑
n