Extended natural numbers form a complete linear order #

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 ι] [IsDirectedOrder ι] {f g : ι → ℕ∞} (hf : Monotone f) (hg : Monotone g) :

iSup f + iSup g = ⨆ (a : ι), f a + g a

source

theorem ENat.smul_iSup {ι : Sort u_2} {R : Type u_4} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) :

c • ⨆ (i : ι), f i = ⨆ (i : ι), c • f i

source

theorem ENat.smul_sSup {R : Type u_4} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R) :

c • sSup s = ⨆ a ∈ s, c • a

source

theorem ENat.sub_iSup {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] (ha : a ≠ ⊤) :

a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

source

theorem ENat.iInf_add {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} :

iInf f + a = ⨅ (i : ι), f i + a

source

theorem ENat.sub_iInf {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} :

a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

source

theorem ENat.sInf_add {a : ℕ∞} {s : Set ℕ∞} :

sInf s + a = ⨅ b ∈ s, b + a

source

theorem ENat.add_iInf {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} :

a + iInf f = ⨅ (b : ι), a + f b

source

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

iInf f + iInf g = ⨅ (a : ι), f a + g a

source

theorem ENat.iInf_add_iInf_of_monotone {ι : Type u_4} [Preorder ι] [IsCodirectedOrder ι] {f g : ι → ℕ∞} (hf : Monotone f) (hg : Monotone g) :

iInf f + iInf g = ⨅ (a : ι), f a + g a

source

theorem ENat.add_iInf₂ {ι : Sort u_2} {a : ℕ∞} {κ : ι → Sort u_4} (f : (i : ι) → κ i → ℕ∞) :

a + ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a + f i j

source

theorem ENat.iInf₂_add {ι : Sort u_2} {a : ℕ∞} {κ : ι → Sort u_4} (f : (i : ι) → κ i → ℕ∞) :

(⨅ (i : ι), ⨅ (j : κ i), f i j) + a = ⨅ (i : ι), ⨅ (j : κ i), f i j + a

source

theorem ENat.add_sInf {a : ℕ∞} {s : Set ℕ∞} :

a + sInf s = ⨅ b ∈ s, a + b

source

theorem ENat.le_iInf_add_iInf {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} {κ : Sort u_4} {g : κ → ℕ∞} (h : ∀ (i : ι) (j : κ), a ≤ f i + g j) :

a ≤ iInf f + iInf g

source

theorem ENat.le_iInf₂_add_iInf₂ {ι : Sort u_2} {a : ℕ∞} {κ : Sort u_4} {q₁ : ι → Sort u_5} {q₂ : κ → Sort u_6} {f : (i : ι) → q₁ i → ℕ∞} {g : (k : κ) → q₂ k → ℕ∞} (h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk) :

a ≤ (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) + ⨅ (k : κ), ⨅ (qk : q₂ k), g k qk

Documentation

Mathlib.Data.ENat.Lattice

Extended natural numbers form a complete linear order #