TopologicalSpace.Opens.opensHomHasCoeToFun.proof_1
theorem TopologicalSpace.Opens.opensHomHasCoeToFun.proof_1 :
∀ {X : TopCat} {U V : TopologicalSpace.Opens ↑X}, (U ⟶ V) → ∀ (x : ↥U), ↑x ∈ ↑V
The theorem `TopologicalSpace.Opens.opensHomHasCoeToFun.proof_1` states that for every topological space `X` in the category of topological spaces (`TopCat`), and for any two open sets `U` and `V` in `X`, any morphism (or continuous map) from `U` to `V` ensures that for any point `x` in `U`, `x` is also in `V`. In other words, if we have a continuous map from one open set to another in a given topological space, any point in the domain set is also a point in the codomain set.
More concisely: For any topological spaces X and open sets U, V in X, any continuous map from U to V implies that the inclusion of U into V is a subset inclusion.
|
TopologicalSpace.Opens.openEmbedding
theorem TopologicalSpace.Opens.openEmbedding :
∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), OpenEmbedding ⇑U.inclusion
This theorem asserts that for any topological space `X` (from the category `TopCat`) and any open subset `U` of `X`, the inclusion map from `U` to `X` (as denoted by `TopologicalSpace.Opens.inclusion U`) is an open embedding. In terms of topology, an open embedding is a continuous and injective function that also has the property that the image of any open set under this function is open. Therefore, the theorem essentially guarantees that the inclusion of an open subset into a topological space preserves the topological structure, specifically the open sets.
More concisely: The inclusion map of an open subset into a topological space is an open embedding.
|
TopologicalSpace.Opens.map_obj
theorem TopologicalSpace.Opens.map_obj :
∀ {X Y : TopCat} (f : X ⟶ Y) (U : Set ↑Y) (p : IsOpen U),
(TopologicalSpace.Opens.map f).obj { carrier := U, is_open' := p } = { carrier := ⇑f ⁻¹' U, is_open' := ⋯ }
The theorem `TopologicalSpace.Opens.map_obj` states that for any topological spaces `X` and `Y`, and for any continuous map `f` from `X` to `Y`, if `U` is an open set in `Y`, then the object of the functor `Opens.map f` applied to `U` is the set of preimages of `U` under `f` which is an open set in `X`. This essentially indicates that the preimage of an open set under a continuous map is also open, reflecting one of the key properties of continuous functions in topology.
More concisely: For any continuous function $f$ between topological spaces $X$ and $Y$, and any open set $U$ in $Y$, the preimage $f^{-1}(U)$ is an open set in $X$.
|
TopologicalSpace.Opens.openEmbedding_obj_top
theorem TopologicalSpace.Opens.openEmbedding_obj_top :
∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), ⋯.functor.obj ⊤ = U
This theorem states that for any topological space `X` in the category of topological spaces (`TopCat`) and for any open set `U` in that topological space, the object of the functor induced by an open map (defined by `IsOpenMap.functor`) applied to the top element (`⊤`) is equal to `U`. In other words, this theorem asserts that the functor produced by any open map maps the whole topological space `X` (represented by the top element `⊤`) onto any of its open subsets `U`.
More concisely: For any topological space X and open set U, the functor induced by an open map maps the top element ⊤ of X to U.
|