iUnion_Ici_eq_Ioi_iInf — Mathlib

English

For a complete linear order R and a family f: ι → R with no least element in range, the union of all rays [f(i), ∞) equals the ray (inf_i f(i), ∞).

Русский

Для полного линейного порядка R и семейства f: ι → R с условием, что инфimum по i не лежит в диапазоне f, объединение всех лучей [f(i), ∞) равно лучу (inf_i f(i), ∞).

LaTeX

$$$$\bigcup_i [f(i), \infty) = (\inf_i f(i), \infty)$$$$

Lean4

theorem iUnion_Ici_eq_Ioi_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R} (no_least_elem : ⨅ i, f i ∉ range f) :
    ⋃ i : ι, Ici (f i) = Ioi (⨅ i, f i) := by
  simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range, iUnion_exists,
    iUnion_iUnion_eq']

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