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.

TODO

Currently (2024-Nov-12), shake does not check proof_wanted and insist that Mathlib.Algebra.Group.Action.Defs should not be imported. Once shake is fixed, please remove the corresponding noshake.json entry.

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}

@[simp]

theorem ENat.iSup_eq_zero {ι : Sort u_1} {f : ι → ℕ∞} : iSup f = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem ENat.iSup_zero {ι : Sort u_1} : ⨆ (x : ι), 0 = 0

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

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 < ⊤) : sSup s ∈ 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

theorem ENat.iSup_natCast : ⨆ (n : ℕ), ↑n = ⊤

theorem ENat.add_iSup {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞) : a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

theorem ENat.iSup_add {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞) : (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

theorem ENat.add_biSup' {ι : Sort u_2} {a : ℕ∞} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ℕ∞) : a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

theorem ENat.biSup_add' {ι : Sort u_2} {a : ℕ∞} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ℕ∞) : (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

theorem ENat.add_biSup {a : ℕ∞} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

theorem ENat.biSup_add {a : ℕ∞} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

theorem ENat.add_sSup {s : Set ℕ∞} {a : ℕ∞} (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

theorem ENat.sSup_add {s : Set ℕ∞} {a : ℕ∞} (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

theorem ENat.iSup_add_iSup_le {ι : Sort u_2} {κ : Sort u_3} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] [Nonempty κ] {g : κ → ℕ∞} (h : ∀ (i : ι) (j : κ), f i + g j ≤ a) : iSup f + iSup g ≤ a

theorem ENat.biSup_add_biSup_le' {ι : Sort u_2} {κ : Sort u_3} {f : ι → ℕ∞} {a : ℕ∞} {p : ι → Prop} {q : κ → Prop} (hp : ∃ (i : ι), p i) (hq : ∃ (j : κ), q j) {g : κ → ℕ∞} (h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a) : (⨆ (i : ι), ⨆ (_ : p i), f i) + ⨆ (j : κ), ⨆ (_ : q j), g j ≤ a

theorem ENat.biSup_add_biSup_le {ι : Type u_4} {κ : Type u_5} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ℕ∞} {g : κ → ℕ∞} {a : ℕ∞} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a

theorem ENat.iSup_add_iSup {ι : Sort u_2} {f g : ι → ℕ∞} (h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ (i : ι), f i + g i

theorem ENat.iSup_add_iSup_of_monotone {ι : Type u_4} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {f g : ι → ℕ∞} (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ (a : ι), f a + g a

theorem ENat.sub_iSup {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i