English
The projections satisfy the universal property that composing ι_i with fromOpenSubsetsGlue yields the canonical inclusion mapping for U_i.
Русский
Проекции удовлетворяют универсальной свойству, что композиция ι_i с fromOpenSubsetsGlue даёт каноническое включение для U_i.
LaTeX
$$ι_i^{fromOpenSubsetsGlue} ; fromOpenSubsetsGlue = inclusion'$$
Lean4
/-- The canonical map from the glue of a family of open subsets `α` into `α`.
This map is an open embedding (`fromOpenSubsetsGlue_isOpenEmbedding`),
and its range is `⋃ i, (U i : Set α)` (`range_fromOpenSubsetsGlue`).
-/
def fromOpenSubsetsGlue : (ofOpenSubsets U).toGlueData.glued ⟶ TopCat.of α :=
Multicoequalizer.desc _ _ (fun _ => Opens.inclusion' _) (by rintro ⟨i, j⟩; ext x; rfl)
