range_fromOpenSubsetsGlue — Mathlib

English

The range of fromOpenSubsetsGlue is the union of the images of all Ui in α.

Русский

Область значения fromOpenSubsetsGlue есть объединение образов всех Ui в α.

LaTeX

$$Range(fromOpenSubsetsGlue) = ⋃ i, (U i : Set α)$$

Lean4

theorem range_fromOpenSubsetsGlue : Set.range (fromOpenSubsetsGlue U) = ⋃ i, (U i : Set α) :=
  by
  ext
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
    rw [ι_fromOpenSubsetsGlue_apply]
    exact Set.subset_iUnion _ i hx'
  · rintro ⟨_, ⟨i, rfl⟩, hx⟩
    rename_i x
    exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

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