TopCat.GlueData.ι_injective

theorem TopCat.GlueData.ι_injective : ∀ (D : TopCat.GlueData) (i : D.J), Function.Injective ⇑(D.ι i)

The theorem `TopCat.GlueData.ι_injective` states that for any glued data structure `D` in the category of topological spaces (`TopCat.GlueData`), and any index `i` in the indexing set of `D`, the map `ι` from the `i`th component to the glued data (given by `CategoryTheory.GlueData.ι D.toGlueData i`) is injective. In other words, if applying this map to two different points in the `i`th component gives the same point in the glued data, then the two original points must have been the same.

More concisely: For any glued data structure in the category of topological spaces, the map from the indexing set to the glued data is injective.