biUnion_Ici_eq_Ici — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Ici x = Ici a :=
  by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
  · exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

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