sSup_iUnion_Iic — Mathlib

English

The supremum of the union of all intervals [f(i), ∞) equals the supremum of the values f(i): sSup(⋃i Iic(f(i))) = ⨆ i f(i).

Русский

Супремум объединения всех интервалов [f(i), ∞) равен супремуму значений f(i): sSup(⋃i Iic(f(i))) = ⨆ i f(i).

LaTeX

$$$ \operatorname{sSup} \big(\bigcup_{i} \mathrm{Iic}(f(i))\big) = \big\lVert \big( \sum_i f(i) \big\rVert \big) $$$

Lean4

theorem sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i, f i :=
  by
  apply csSup_eq_csSup_of_forall_exists_le
  · rintro x ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨f i, mem_range_self _, hi⟩
  · rintro x ⟨i, rfl⟩
    exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

Похожие утверждения