Documentation

Mathlib.Data.ENat.Lattice

Extended natural numbers form a complete linear order #

This instance is not in Data.ENat.Basic to avoid dependency on Finsets.

We also restate some lemmas about WithTop for ENat to have versions that use Nat.cast instead of WithTop.some.

noncomputable instance instCompleteLinearOrderENat :

CompleteLinearOrder ℕ∞

Equations

instCompleteLinearOrderENat = inferInstanceAs (CompleteLinearOrder (WithTop ℕ))

noncomputable instance instCompleteLinearOrderWithBotENat :

CompleteLinearOrder (WithBot ℕ∞)

Equations

instCompleteLinearOrderWithBotENat = inferInstanceAs (CompleteLinearOrder (WithBot (WithTop ℕ)))

theorem ENat.iSup_coe_eq_top {ι : Sort u_1} {f : ι → ℕ} :

⨆ (i : ι), ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)

theorem ENat.iSup_coe_ne_top {ι : Sort u_1} {f : ι → ℕ} :

⨆ (i : ι), ↑(f i) ≠ ⊤ ↔ BddAbove (Set.range f)

theorem ENat.iSup_coe_lt_top {ι : Sort u_1} {f : ι → ℕ} :

⨆ (i : ι), ↑(f i) < ⊤ ↔ BddAbove (Set.range f)

theorem ENat.iInf_coe_eq_top {ι : Sort u_1} {f : ι → ℕ} :

⨅ (i : ι), ↑(f i) = ⊤ ↔ IsEmpty ι

theorem ENat.iInf_coe_ne_top {ι : Sort u_1} {f : ι → ℕ} :

⨅ (i : ι), ↑(f i) ≠ ⊤ ↔ Nonempty ι

theorem ENat.iInf_coe_lt_top {ι : Sort u_1} {f : ι → ℕ} :

⨅ (i : ι), ↑(f i) < ⊤ ↔ Nonempty ι

theorem ENat.coe_sSup {s : Set ℕ} :

BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a

theorem ENat.coe_sInf {s : Set ℕ} (hs : s.Nonempty) :

↑(sInf s) = ⨅ a ∈ s, ↑a

theorem ENat.coe_iSup {ι : Sort u_1} {f : ι → ℕ} :

BddAbove (Set.range f) → ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

theorem ENat.coe_iInf {ι : Sort u_1} {f : ι → ℕ} [Nonempty ι] :

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

@[simp]

theorem ENat.iInf_eq_top_of_isEmpty {ι : Sort u_1} {f : ι → ℕ} [IsEmpty ι] :

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

theorem ENat.iInf_toNat {ι : Sort u_1} {f : ι → ℕ} :

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

theorem ENat.iInf_eq_zero {ι : Sort u_1} {f : ι → ℕ} :

⨅ (i : ι), ↑(f i) = 0 ↔ ∃ (i : ι), f i = 0

theorem ENat.sSup_eq_zero {s : Set ℕ∞} :

sSup s = 0 ↔ ∀ a ∈ s, a = 0

theorem ENat.sInf_eq_zero {s : Set ℕ∞} :

sInf s = 0 ↔ 0 ∈ s

theorem ENat.sSup_eq_zero' {s : Set ℕ∞} :

sSup s = 0 ↔ s = ∅ ∨ s = {0}

theorem ENat.iSup_eq_zero {ι : Sort u_1} {f : ι → ℕ∞} :

iSup f = 0 ↔ ∀ (i : ι), f i = 0

theorem ENat.sSup_eq_top_of_infinite {s : Set ℕ∞} (h : s.Infinite) :

theorem ENat.finite_of_sSup_lt_top {s : Set ℕ∞} (h : sSup s < ⊤) :

s.Finite

theorem ENat.sSup_mem_of_Nonempty_of_lt_top {s : Set ℕ∞} [Nonempty ↑s] (hs' : sSup s < ⊤) :

theorem ENat.exists_eq_iSup_of_lt_top {ι : Sort u_1} {f : ι → ℕ∞} [Nonempty ι] (h : ⨆ (i : ι), f i < ⊤) :

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

theorem ENat.exists_eq_iSup₂_of_lt_top {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁ → ι₂ → ℕ∞} [Nonempty ι₁] [Nonempty ι₂] (h : ⨆ (i : ι₁), ⨆ (j : ι₂), f i j < ⊤) :

∃ (i : ι₁) (j : ι₂), f i j = ⨆ (i : ι₁), ⨆ (j : ι₂), f i j