biUnion_Ici_eq_Ioi — Mathlib

English

If s has GLB a and a ∉ s, then the union over x ∈ s of Ici x equals Ici a.

Русский

Если s имеет наименьшую нижнюю границу a и a ∉ s, то ⋃_{x∈s} Ici x = Ici a.

LaTeX

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

Lean4

theorem biUnion_Ici_eq_Ioi (a_glb : IsGLB s a) (a_notMem : a ∉ s) : ⋃ x ∈ s, Ici x = Ioi a :=
  by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_notMem) hx)
  · rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
    rw [mem_iUnion₂]
    exact ⟨y, hys, hyx.le⟩

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