sInf_iUnion_Ici — Mathlib

English

The infimum of the union of all intervals [f(i), ∞) equals the infimum of the f(i) values: sInf(⋃i Ici(f(i))) = ⨅ i f(i).

Русский

Infimum объединения всех интервалов [f(i), ∞) равен инфимума значений f(i).

LaTeX

$$$ \operatorname{sInf} (\bigcup_{i} \mathrm{Ici}(f(i))) = \big\wedge_i f(i) $$$

Lean4

theorem sInf_iUnion_Ici (f : ι → α) : sInf (⋃ (i : ι), Ici (f i)) = ⨅ i, f i :=
  sSup_iUnion_Iic (α := αᵒᵈ) f

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