Documentation

noncomputable def ENat.floor :

ENNReal → ℕ∞

⌊r⌋ₑ is the greatest extended natural n such that n ≤ r.

Instances For

noncomputable def ENat.ceil :

ENNReal → ℕ∞

⌈r⌉ₑ is the least extended natural n such that r ≤ n

Instances For

def ENat.«term⌊_⌋ₑ» :

Lean.ParserDescr

⌊r⌋ₑ is the greatest extended natural n such that n ≤ r.

Instances For

def ENat.«term⌈_⌉ₑ» :

Lean.ParserDescr

⌈r⌉ₑ is the least extended natural n such that r ≤ n

Instances For

@[simp]

theorem ENat.floor_top :

⌊⊤⌋ₑ = ⊤

@[simp]

theorem ENat.ceil_top :

⌈⊤⌉ₑ = ⊤

@[simp]

theorem ENat.floor_coe (r : NNReal) :

⌊↑r⌋ₑ = ↑⌊r⌋₊

@[simp]

theorem ENat.ceil_coe (r : NNReal) :

⌈↑r⌉ₑ = ↑⌈r⌉₊

@[simp]

theorem ENat.floor_eq_top {r : ENNReal} :

⌊r⌋ₑ = ⊤ ↔ r = ⊤

@[simp]

theorem ENat.ceil_eq_top {r : ENNReal} :

⌈r⌉ₑ = ⊤ ↔ r = ⊤

theorem ENat.floor_lt_top {r : ENNReal} :

⌊r⌋ₑ < ⊤ ↔ r < ⊤

@[simp]

theorem ENat.ceil_lt_top {r : ENNReal} :

⌈r⌉ₑ < ⊤ ↔ r < ⊤

@[simp]

theorem ENat.le_floor {r : ENNReal} {n : ℕ∞} :

n ≤ ⌊r⌋ₑ ↔ ↑n ≤ r

@[simp]

theorem ENat.ceil_le {r : ENNReal} {n : ℕ∞} :

⌈r⌉ₑ ≤ n ↔ r ≤ ↑n

@[simp]

theorem ENat.floor_lt {r : ENNReal} {n : ℕ∞} :

⌊r⌋ₑ < n ↔ r < ↑n

@[simp]

theorem ENat.lt_ceil {r : ENNReal} {n : ℕ∞} :

n < ⌈r⌉ₑ ↔ ↑n < r

GaloisConnection toENNReal floor

theorem ENat.gc_toENNReal_floor :

GaloisConnection ceil toENNReal

theorem ENat.gc_ceil_toENNReal :

theorem ENat.floor_le_self {r : ENNReal} :

↑⌊r⌋ₑ ≤ r

theorem ENat.le_ceil_self {r : ENNReal} :

r ≤ ↑⌈r⌉ₑ

@[simp]

theorem ENat.floor_le {r : ENNReal} {n : ℕ∞} (hn : n ≠ ⊤) :

⌊r⌋ₑ ≤ n ↔ r < ↑n + 1

@[simp]

theorem ENat.le_ceil {r : ENNReal} {n : ℕ∞} (hn₀ : n ≠ 0) (hn : n ≠ ⊤) :

n ≤ ⌈r⌉ₑ ↔ ↑n - 1 < r

@[simp]

theorem ENat.lt_floor {r : ENNReal} {n : ℕ∞} (hn : n ≠ ⊤) :

n < ⌊r⌋ₑ ↔ ↑n + 1 ≤ r

@[simp]

theorem ENat.ceil_lt {r : ENNReal} {n : ℕ∞} (hn₀ : n ≠ 0) (hn : n ≠ ⊤) :

⌈r⌉ₑ < n ↔ r ≤ ↑n - 1

theorem ENat.floor_mono :

Monotone floor

theorem ENat.ceil_mono :

Monotone ceil

theorem ENat.floor_le_floor {r s : ENNReal} (hrs : r ≤ s) :

⌊r⌋ₑ ≤ ⌊s⌋ₑ

theorem ENat.ceil_le_ceil {r s : ENNReal} (hrs : r ≤ s) :

⌈r⌉ₑ ≤ ⌈s⌉ₑ

@[simp]

theorem ENat.floor_natCast (n : ℕ∞) :

⌊↑n⌋ₑ = n

@[simp]

theorem ENat.ceil_natCast (n : ℕ∞) :

⌈↑n⌉ₑ = n

@[simp]

theorem ENat.floor_zero :

⌊0⌋ₑ = 0

@[simp]

theorem ENat.ceil_zero :

⌈0⌉ₑ = 0

@[simp]

theorem ENat.floor_one :

⌊1⌋ₑ = 1

@[simp]

theorem ENat.ceil_one :

⌈1⌉ₑ = 1

@[simp]

theorem ENat.floor_ofNat (n : ℕ) [n.AtLeastTwo] :

⌊OfNat.ofNat n⌋ₑ = OfNat.ofNat n

@[simp]

theorem ENat.ceil_ofNat (n : ℕ) [n.AtLeastTwo] :

⌈OfNat.ofNat n⌉ₑ = OfNat.ofNat n

theorem ENat.floor_pos {r : ENNReal} :

0 < ⌊r⌋ₑ ↔ 1 ≤ r

theorem ENat.ceil_pos {r : ENNReal} :

0 < ⌈r⌉ₑ ↔ 0 < r

@[simp]

theorem ENat.floor_eq_zero {r : ENNReal} :

⌊r⌋ₑ = 0 ↔ r < 1

@[simp]

theorem ENat.ceil_eq_zero {r : ENNReal} :

⌈r⌉ₑ = 0 ↔ r = 0

theorem ENat.floor_le_ceil {r : ENNReal} :

⌊r⌋ₑ ≤ ⌈r⌉ₑ

theorem ENat.ceil_le_floor_add_one (r : ENNReal) :

⌈r⌉ₑ ≤ ⌊r⌋ₑ + 1

theorem ENat.floor_lt_ceil {r s : ENNReal} (hrs : r < s) :

⌊r⌋ₑ < ⌈s⌉ₑ

theorem ENat.floor_congr {r s : ENNReal} (h : ∀ (n : ℕ∞), ↑n ≤ r ↔ ↑n ≤ s) :

⌊r⌋ₑ = ⌊s⌋ₑ

theorem ENat.ceil_congr {r s : ENNReal} (h : ∀ (n : ℕ∞), r ≤ ↑n ↔ s ≤ ↑n) :

⌈r⌉ₑ = ⌈s⌉ₑ

@[simp]

theorem ENat.floor_add_toENNReal (r : ENNReal) (n : ℕ∞) :

⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + n

@[simp]

theorem ENat.ceil_add_toENNReal (r : ENNReal) (n : ℕ∞) :

⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + n

@[simp]

theorem ENat.floor_toENNReal_add (r : ENNReal) (n : ℕ∞) :

⌊↑n + r⌋ₑ = n + ⌊r⌋ₑ

@[simp]

theorem ENat.ceil_toENNReal_add (r : ENNReal) (n : ℕ∞) :

⌈↑n + r⌉ₑ = n + ⌈r⌉ₑ

@[simp]

theorem ENat.floor_add_natCast (r : ENNReal) (n : ℕ) :

⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + ↑n

@[simp]

theorem ENat.ceil_add_natCast (r : ENNReal) (n : ℕ) :

⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + ↑n

@[simp]

theorem ENat.floor_natCast_add (r : ENNReal) (n : ℕ) :

⌊↑n + r⌋ₑ = ↑n + ⌊r⌋ₑ

@[simp]

theorem ENat.ceil_natCast_add (r : ENNReal) (n : ℕ) :

⌈↑n + r⌉ₑ = ↑n + ⌈r⌉ₑ

@[simp]

theorem ENat.floor_add_one (r : ENNReal) :

⌊r + 1⌋ₑ = ⌊r⌋ₑ + 1

@[simp]

theorem ENat.ceil_add_one (r : ENNReal) :

⌈r + 1⌉ₑ = ⌈r⌉ₑ + 1

@[simp]

theorem ENat.floor_add_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌊r + OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ + OfNat.ofNat n

@[simp]

theorem ENat.ceil_add_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌈r + OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ + OfNat.ofNat n

@[simp]

theorem ENat.floor_sub_toENNReal (r : ENNReal) (n : ℕ∞) :

⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - n

@[simp]

theorem ENat.ceil_sub_toENNReal (r : ENNReal) (n : ℕ∞) :

⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - n

@[simp]

theorem ENat.floor_sub_natCast (r : ENNReal) (n : ℕ) :

⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - ↑n

@[simp]

theorem ENat.ceil_sub_natCast (r : ENNReal) (n : ℕ) :

⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - ↑n

@[simp]

theorem ENat.floor_sub_one (r : ENNReal) :

⌊r - 1⌋ₑ = ⌊r⌋ₑ - 1

@[simp]

theorem ENat.ceil_sub_one (r : ENNReal) :

⌈r - 1⌉ₑ = ⌈r⌉ₑ - 1

@[simp]

theorem ENat.floor_sub_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌊r - OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ - OfNat.ofNat n

@[simp]

theorem ENat.ceil_sub_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌈r - OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ - OfNat.ofNat n

theorem ENat.ceil_lt_add_one {r : ENNReal} (hr : r ≠ ⊤) :

↑⌈r⌉ₑ < r + 1

theorem ENat.ceil_add_le (r s : ENNReal) :

⌈r + s⌉ₑ ≤ ⌈r⌉ₑ + ⌈s⌉ₑ

@[simp]

theorem ENat.toENNReal_iSup {ι : Sort u_1} (f : ι → ℕ∞) :

↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

@[simp]

theorem ENat.toENNReal_iInf {ι : Sort u_1} (f : ι → ℕ∞) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

theorem Mathlib.Meta.Positivity.natCeil_pos {r : ENNReal} :

0 < r → 0 < ⌈r⌉ₑ

Alias of the reverse direction of ENat.ceil_pos.