biUnion_Ioi_eq — Mathlib

English

Let s be a set with GLB a. If a ∉ s, then the union over x ∈ s of the right-closed rays [x, ∞) equals the right ray starting at a, i.e., ⋃_{x∈s} [x, ∞) = [a, ∞) or equivalently Ici x over s equals Ioi a.

Русский

Пусть s имеет наименьшее нижнееBounds a. Если a ∉ s, то объединение по x ∈ s полулучей [x, ∞) даёт луч [a, ∞); т.е. ⋃_{x∈s} [x, ∞) = [a, ∞).

LaTeX

$$$$\bigcup_{x\in s} \mathrm{Ici}(x) = \mathrm{Ioi}(a)$$$$

Lean4

theorem biUnion_Ioi_eq (h : IsGLB s a) : ⋃ x ∈ s, Ioi x = Ioi a :=
  by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ioi_subset_Ioi (h.1 hx)
  · rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
    exact mem_biUnion hys hyx

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