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.

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.

source
noncomputable instance instCompleteLinearOrderENat :
CompleteLinearOrder ℕ∞
Equations
source
noncomputable instance instCompleteLinearOrderWithBotENat :
CompleteLinearOrder (WithBot ℕ∞)
Equations
source
theorem ENat.iSup_coe_eq_top {ι : Sort u_1} {f : ι → ℕ} :
⨆ (i : ι), ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
source
theorem ENat.iSup_coe_ne_top {ι : Sort u_1} {f : ι → ℕ} :
⨆ (i : ι), ↑(f i) ≠ ⊤ ↔ BddAbove (Set.range f)
source
theorem ENat.iSup_coe_lt_top {ι : Sort u_1} {f : ι → ℕ} :
⨆ (i : ι), ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
source
theorem ENat.iInf_coe_eq_top {ι : Sort u_1} {f : ι → ℕ} :
⨅ (i : ι), ↑(f i) = ⊤ ↔ IsEmpty ι
source
theorem ENat.iInf_coe_ne_top {ι : Sort u_1} {f : ι → ℕ} :
⨅ (i : ι), ↑(f i) ≠ ⊤ ↔ Nonempty ι
source
theorem ENat.iInf_coe_lt_top {ι : Sort u_1} {f : ι → ℕ} :
⨅ (i : ι), ↑(f i) < ⊤ ↔ Nonempty ι
source
theorem ENat.coe_sSup {s : Set ℕ} :
BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
source
theorem ENat.coe_sInf {s : Set ℕ} (hs : s.Nonempty) :
↑(sInf s) = ⨅ a ∈ s, ↑a
source
theorem ENat.coe_iSup {ι : Sort u_1} {f : ι → ℕ} :
BddAbove (Set.range f) → ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
source
theorem ENat.coe_iInf {ι : Sort u_1} {f : ι → ℕ} [Nonempty ι] :
↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
source
@[simp]
theorem ENat.iInf_eq_top_of_isEmpty {ι : Sort u_1} {f : ι → ℕ} [IsEmpty ι] :
⨅ (i : ι), ↑(f i) = ⊤
source
theorem ENat.iInf_toNat {ι : Sort u_1} {f : ι → ℕ} :
(⨅ (i : ι), ↑(f i)).toNat = ⨅ (i : ι), f i
source
@[simp]
theorem ENat.iInf_eq_zero {ι : Sort u_1} {f : ι → ℕ∞} :
⨅ (i : ι), f i = 0 ↔ ∃ (i : ι), f i = 0
source
theorem ENat.sSup_eq_zero {s : Set ℕ∞} :
sSup s = 0 ↔ ∀ a ∈ s, a = 0
source
theorem ENat.sInf_eq_zero {s : Set ℕ∞} :
sInf s = 0 ↔ 0 ∈ s
source
theorem ENat.sSup_eq_zero' {s : Set ℕ∞} :
sSup s = 0 ↔ s = ∅ ∨ s = {0}
source
@[simp]
theorem ENat.iSup_eq_zero {ι : Sort u_1} {f : ι → ℕ∞} :
iSup f = 0 ↔ ∀ (i : ι), f i = 0
source
@[simp]
theorem ENat.iSup_zero {ι : Sort u_1} :
⨆ (x : ι), 0 = 0
source
theorem ENat.exists_eq_iInf {ι : Sort u_1} [Nonempty ι] (f : ι → ℕ∞) :
∃ (a : ι), f a = ⨅ (x : ι), f x
source
theorem ENat.sSup_eq_top_of_infinite {s : Set ℕ∞} (h : s.Infinite) :
sSup s = ⊤
source
theorem ENat.finite_of_sSup_lt_top {s : Set ℕ∞} (h : sSup s < ⊤) :
s.Finite
source
theorem ENat.sSup_mem_of_nonempty_of_lt_top {s : Set ℕ∞} [Nonempty ↑s] (hs' : sSup s < ⊤) :
sSup s ∈ s
source
theorem ENat.exists_eq_iSup_of_lt_top {ι : Sort u_1} {f : ι → ℕ∞} [Nonempty ι] (h : ⨆ (i : ι), f i < ⊤) :
∃ (i : ι), f i = ⨆ (i : ι), f i
source
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
source
theorem ENat.iSup_natCast :
⨆ (n : ℕ), ↑n = ⊤
source
theorem ENat.mul_iSup {ι : Sort u_2} (a : ℕ∞) (f : ι → ℕ∞) :
a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
source
theorem ENat.iSup_mul {ι : Sort u_2} (f : ι → ℕ∞) (a : ℕ∞) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
source
theorem ENat.mul_sSup {s : Set ℕ∞} {a : ℕ∞} :
a * sSup s = ⨆ b ∈ s, a * b
source
theorem ENat.sSup_mul {s : Set ℕ∞} {a : ℕ∞} :
sSup s * a = ⨆ b ∈ s, b * a
source
theorem ENat.mul_iInf {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
source
theorem ENat.iInf_mul {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] :
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
source
theorem ENat.mul_iInf' {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} (h₀ : a = 0 → Nonempty ι) :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

A version of mul_iInf with a slightly more general hypothesis.

source
theorem ENat.iInf_mul' {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} (h₀ : a = 0 → Nonempty ι) :
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

A version of iInf_mul with a slightly more general hypothesis.

source
theorem ENat.mul_iInf_of_ne {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} (ha₀ : a ≠ 0) :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

If a ≠ 0, then right multiplication by a maps infimum to infimum. See also ENat.iInf_mul that assumes [Nonempty ι] but does not require a ≠ 0.

source
theorem ENat.iInf_mul_of_ne {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} (ha₀ : a ≠ 0) :
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

If a ≠ 0, then right multiplication by a maps infimum to infimum. See also ENat.iInf_mul that assumes [Nonempty ι] but does not require a ≠ 0.

source
theorem ENat.add_iSup {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞) :
a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
source
theorem ENat.iSup_add {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞) :
(⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a
source
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
source
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
source
theorem ENat.add_biSup {a : ℕ∞} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) :
a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i
source
theorem ENat.biSup_add {a : ℕ∞} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) :
(⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a
source
theorem ENat.add_sSup {s : Set ℕ∞} {a : ℕ∞} (hs : s.Nonempty) :
a + sSup s = ⨆ b ∈ s, a + b
source
theorem ENat.sSup_add {s : Set ℕ∞} {a : ℕ∞} (hs : s.Nonempty) :
sSup s + a = ⨆ b ∈ s, b + a
source
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
source
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
source
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
source
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
source
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
source
theorem ENat.sub_iSup {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] (ha : a ≠ ⊤) :
a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i