TopologicalSpace.OpenNhds.openEmbedding

theorem TopologicalSpace.OpenNhds.openEmbedding : ∀ {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x), OpenEmbedding ⇑U.obj.inclusion

This theorem states that for any topological space 'X' and any point 'x' in 'X', if 'U' is an open neighborhood of 'x' in 'X', then the function given by the inclusion of 'U' into 'X' is an open embedding. An open embedding is a function that is both an embedding and an open map, meaning it injectively maps 'U' into 'X' while preserving the topology, i.e., the open subsets of 'U' are mapped to open subsets of 'X'.

More concisely: Given any topological space 'X' and point 'x' in 'X', if 'U' is an open neighborhood of 'x', then the inclusion function from 'U' to 'X' is a topological embedding. (A topological embedding is an open and injective function that preserves the topology.)