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.

source
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.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_iInf {ι : Sort u_1} [Nonempty ι] (f : ι → ℕ∞) :
∃ (a : ι), f a = ⨅ (x : ι), f x
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.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