Theorems · Definition · general topology

TopCat.GlueData.fromOpenSubsetsGlue

{α : Type u} →
  [inst : TopologicalSpace α] →
    {J : Type u} → (U : J → TopologicalSpace.Opens α) → (TopCat.GlueData.ofOpenSubsets U).glued ⟶ TopCat.of α

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).

Defined in

Mathlib.Topology.Gluing

Cited by

6 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace