Documentation
MeanFourier
.
Mathlib
.
Data
.
EReal
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Data.EReal.Basic
Imported by
EReal
.
ennrealtoEReal_le_natCast
source
@[simp]
theorem
EReal
.
ennrealtoEReal_le_natCast
{
r
:
ENNReal
}
{
n
:
ℕ
}
:
↑
r
≤
↑
n
↔
r
≤
↑
n