Homeomorph.isClosedMap
theorem Homeomorph.isClosedMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
IsClosedMap ⇑h
The theorem `Homeomorph.isClosedMap` states that for any two topological spaces `X` and `Y`, and any homeomorphism `h` from `X` to `Y`, the function `h` is a closed map. In other words, if `U` is a closed set in `X`, then its image under `h`, i.e., `h(U)`, is a closed set in `Y`. This theorem holds for all topological spaces `X` and `Y`, and any homeomorphisms between them.
More concisely: Given any topological spaces X and Y and a homeomorphism h from X to Y, the image of any closed set in X under h is a closed set in Y.
|
Homeomorph.funSplitAt_symm_apply
theorem Homeomorph.funSplitAt_symm_apply :
∀ (Y : Type u_2) [inst : TopologicalSpace Y] {ι : Type u_6} [inst_1 : DecidableEq ι] (i : ι)
(f : (fun a => Y) i × ((j : { j // j ≠ i }) → (fun a => Y) ↑j)) (j : ι),
(Homeomorph.funSplitAt Y i).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
This theorem states that for any type `Y` that has a structure of a topological space, any type `ι` with decidable equality, and any index `i` of type `ι`, the inverse of the homeomorphism `funSplitAt` applied to a pair consisting of a point in `Y` and a function from the set of indices not equal to `i` to `Y`, evaluated at any index `j` of type `ι`, is equal to the first component of the pair if `j` is equal to `i`, and the second component of the pair evaluated at `j` otherwise. In other words, it undoes the splitting operation performed by `funSplitAt`.
More concisely: For any topological space `Y`, decidable type `ι`, and homeomorphism `f` of `Y × (ι → Y)` to `Y × ι` (denoted `funSplitAt`), `f.symm (f x (fun i => if h: i ≠ i then i := i, i := x.2 i)) = if h: i = i then x else x.2 i`.
|
Homeomorph.quotientMap
theorem Homeomorph.quotientMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
QuotientMap ⇑h
This theorem states that for any two types `X` and `Y`, each equipped with a topological space structure, if there exists a homeomorphism `h` from `X` to `Y`, then the function defined by the homeomorphism `h` is a quotient map. A quotient map is a function that is surjective and for any set `s` in `Y`, `s` is open if and only if its preimage under the function is an open set in `X`.
More concisely: If `h` is a homeomorphism between topological spaces `(X, txX)` and `(Y, tyY)`, then `h` is a quotient map, i.e., for any open set `s` in `Y`, `h⁻¹(s)` is an open set in `X`.
|
Homeomorph.map_nhds_eq
theorem Homeomorph.map_nhds_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
Filter.map (⇑h) (nhds x) = nhds (h x)
This theorem states that for any two types `X` and `Y`, which are equipped with topological space structures, given a homeomorphism `h` from `X` to `Y` and a point `x` in `X`, the application of the filter map to the neighborhood filter of `x` in `X` under the homeomorphism `h` is equal to the neighborhood filter of the image of `x` under `h` in `Y`. In mathematical terms, this can be understood as the property that homeomorphisms preserve the topology, in this case, specifically the neighborhood structure around a point.
More concisely: Given two topological spaces `(X,τX)` and `(Y,τY)`, a homeomorphism `h : X ↔ Y`, and a point `x ∈ X`, the neighborhood filters `filter.basic τX x` and `filter.basic τY (h x)` are equal.
|
Homeomorph.closedEmbedding
theorem Homeomorph.closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
ClosedEmbedding ⇑h
This theorem states that for any two types `X` and `Y` that are both topological spaces, if there exists a homeomorphism `h` between `X` and `Y`, then the function `h` is a closed embedding. In other words, `h` is a function that maps closed sets in `X` to closed sets in `Y` and it is injective and continuous, with its image being a homeomorph of the original space `X`.
More concisely: If `X` and `Y` are topological spaces with a homeomorphism `h` between them, then `h` is a closed, injective, and continuous function such that the image of every closed set in `X` is a closed set in `Y`.
|
Homeomorph.image_symm
theorem Homeomorph.image_symm :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Set.image ⇑h.symm = Set.preimage ⇑h
The theorem `Homeomorph.image_symm` states that for any homeomorphism `h` between two types `X` and `Y` that are endowed with topological spaces, the image of a set under the inverse homeomorphism `h⁻¹` is the same as the preimage of the set under the original homeomorphism `h`. In other words, if we take any set from `Y`, find its image in `X` using the inverse of `h`, it would be the same as taking the preimage of the set in `X` using `h`. This establishes a certain symmetry property of images and preimages under homeomorphisms.
More concisely: For any homeomorphism between topological spaces, the image of a set under its inverse is equal to the preimage of that set.
|
Homeomorph.apply_symm_apply
theorem Homeomorph.apply_symm_apply :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y),
h (h.symm y) = y
The theorem `Homeomorph.apply_symm_apply` states that for any homeomorphism `h` from a topological space `X` to another topological space `Y` and for any element `y` of `Y`, applying `h` to the inverse image of `y` under homeomorphism `h` will yield `y` itself. In other words, this theorem ensures that the inverse function of a homeomorphism truly behaves as an inverse, mapping each point in `Y` back to its original point in `X` after applying the homeomorphism `h`.
More concisely: For any homeomorphism $h$ and any $y$ in the codomain, $h(h^{-1}(y)) = y$.
|
Homeomorph.openEmbedding
theorem Homeomorph.openEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
OpenEmbedding ⇑h
This theorem states that for any two types `X` and `Y`, both equipped with a topological space structure, if `X` is homeomorphic to `Y` (denoted as `X ≃ₜ Y`), then the function that maps `X` to `Y` (the homeomorphism) is an open embedding. In other words, the homeomorphism preserves the open sets structure, meaning that an open set in `X` is mapped to an open set in `Y`.
More concisely: If two topological spaces `X` and `Y` are homeomorphic, then any open map between them is a homeomorphism and a topological embedding. (In other words, the homeomorphism preserves open sets and is an open function.)
|
Homeomorph.preimage_closure
theorem Homeomorph.preimage_closure :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y),
⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)
The theorem `Homeomorph.preimage_closure` states that for any two topological spaces `X` and `Y`, and for any homeomorphism `h` from `X` to `Y`, and for any set `s` in `Y`, the preimage of the closure of `s` under the homeomorphism `h` is equal to the closure of the preimage of `s` under `h`. In other words, if we first take the closure of a set and then apply the inverse of a homeomorphism, it's the same as if we first applied the inverse of the homeomorphism and then took the closure. This can be expressed mathematically as: for all `s`, `h⁻¹(closure(s)) = closure(h⁻¹(s))`.
More concisely: For any homeomorphism between topological spaces and any set, the preimages of each other's closures are equal: `h⁻¹(closure(s)) = closure(h⁻¹(s))`.
|
Homeomorph.image_closure
theorem Homeomorph.image_closure :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
⇑h '' closure s = closure (⇑h '' s)
The theorem `Homeomorph.image_closure` states that for any two types `X` and `Y`, each equipped with a topological space structure, a homeomorphism `h` from `X` to `Y`, and a set `s` of type `X`, the image of the closure of `s` under `h` is equal to the closure of the image of `s` under `h`. In mathematical terms, this means if `h` is a homeomorphism from topological space `X` to `Y` and `s` is a set in `X`, then the closure of `h(s)` in `Y` is the same as `h` of the closure of `s` in `X`.
More concisely: For any topological spaces X and Y, a homeomorphism h between them, and a set s in X, the closure of h(s) in Y equals h(closure(s) in X).
|
Homeomorph.inducing
theorem Homeomorph.inducing :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Inducing ⇑h
This theorem states that for any two types `X` and `Y` that are equipped with topological spaces, a homeomorphism `h` from `X` to `Y` is inducing. In the context of topology, an inducing function is one that, given the topology on `Y`, generates the same topology on `X` when we consider the preimage of every open set in `Y`. Thus, this theorem asserts that homeomorphisms preserve the topology under preimages.
More concisely: A homeomorphism between topological spaces preserves the topology, that is, the preimage of any open set under a homeomorphism is an open set.
|
Homeomorph.nhds_eq_comap
theorem Homeomorph.nhds_eq_comap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
nhds x = Filter.comap (⇑h) (nhds (h x))
The theorem `Homeomorph.nhds_eq_comap` states that for any two types `X` and `Y`, each with a defined topological space structure, and a homeomorphism `h` between them, the neighborhood filter at a point `x` in `X` is equal to the filter obtained by precomposing the function `h` with the neighborhood filter at the point `h(x)` in `Y`. In other words, the concept of "neighboring" is preserved in the homeomorphism.
More concisely: For any types `X` and `Y` with topological spaces structures and a homeomorphism `h` between them, the neighborhood filter of `x` in `X` is equal to the filter obtained by precomposing `h` with the neighborhood filter of `h(x)` in `Y`.
|
Homeomorph.isOpen_preimage
theorem Homeomorph.isOpen_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y},
IsOpen (⇑h ⁻¹' s) ↔ IsOpen s
The theorem `Homeomorph.isOpen_preimage` states that for any two types `X` and `Y` with their respective topological space instances, and for any homeomorphism `h` from `X` to `Y`, a set `s` in `Y` is open if and only if its preimage under `h` is open in `X`. Here, the preimage of `s` under `h` is the set of all elements in `X` that `h` maps to `s`. This theorem essentially characterizes one of the key properties of homeomorphisms in topology, which is that they preserve the open (and also closed) sets between the topological spaces.
More concisely: A homeomorphism preserves open sets between topological spaces: for any homeomorphism between topological spaces X and Y, and any open set s in Y, the preimage h⁻¹(s) in X is open.
|
Homeomorph.locallyConnectedSpace
theorem Homeomorph.locallyConnectedSpace :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[i : LocallyConnectedSpace Y], X ≃ₜ Y → LocallyConnectedSpace X
This theorem states that for any two types `X` and `Y` with defined topological spaces, if `Y` is a locally connected space and there is a homeomorphism (a bijective, continuous function with a continuous inverse) between `X` and `Y`, then `X` is also a locally connected space. In other words, the property of being a locally connected space is preserved under a homeomorphism.
More concisely: If `X` and `Y` are topological spaces with `X` homeomorphic to `Y`, and `Y` is locally connected, then `X` is also locally connected.
|
Homeomorph.preimage_symm
theorem Homeomorph.preimage_symm :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Set.preimage ⇑h.symm = Set.image ⇑h
This theorem states that for any two topological spaces `X` and `Y` and any homeomorphism `h` from `X` to `Y`, the preimage of a set under the inverse of `h` is the same as the image of the set under `h`. In simpler terms, if you take a set from `Y`, apply the inverse of `h` to it, and get a set in `X`, this is the same as taking the original set in `X`, applying `h` to it, and obtaining a set in `Y`. This theorem illustrates an important property of homeomorphisms, which are continuous functions with continuous inverses, in the field of topology.
More concisely: For any topological spaces `X`, `Y`, and a homeomorphism `h` from `X` to `Y`, the inverse image of a set under `h` equals the image of that set under `h`.
|
Homeomorph.symm_comp_self
theorem Homeomorph.symm_comp_self :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
⇑h.symm ∘ ⇑h = id
This theorem states that for every homeomorphism `h` from a topological space `X` to another topological space `Y`, the composition of `h` and its inverse (denoted by `Homeomorph.symm h`) is the identity function. In other words, applying the homeomorphism `h` and then its inverse always brings us back to where we started, as it should for a well-defined inverse. This is a fundamental property of homeomorphisms, reflecting their role as isomorphisms in the category of topological spaces.
More concisely: For every homeomorphism `h` between topological spaces `X` and `Y`, `h` and its inverse `Homeomorph.symm h` are mutually inverse functions, i.e., `h ∘ Homeomorph.symm h = idX` and `Homeomorph.symm h ∘ h = idY`, where `idX` and `idY` are the identity functions on `X` and `Y`, respectively.
|
Homeomorph.isCompact_preimage
theorem Homeomorph.isCompact_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
IsCompact (⇑h ⁻¹' s) ↔ IsCompact s
The theorem `Homeomorph.isCompact_preimage` states that for any given topological spaces `X` and `Y`, and a set `s` of type `Y`, if there is a homeomorphism `h` from `X` to `Y`, then the preimage of set `s` under `h` is compact if and only if `s` is compact. In other words, a homeomorphism preserves the property of compactness between the image and preimage of a set.
More concisely: A homeomorphism preserves the compactness of sets, that is, if there is a homeomorphism between topological spaces X and Y, then a set in X is compact if and only if its preimage under this homeomorphism is compact in Y.
|
Homeomorph.comp_continuous_iff'
theorem Homeomorph.comp_continuous_iff' :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z}, Continuous (f ∘ ⇑h) ↔ Continuous f
This theorem states that for any three types `X`, `Y`, and `Z`, each equipped with a topological space structure, and a homeomorphism `h` from `X` to `Y`, a function `f` from `Y` to `Z` is continuous if and only if the composition of `f` and `h` (`f ∘ ⇑h`) is continuous. In other words, the continuity of a function `f` from space `Y` to `Z` is preserved under pre-composition with a homeomorphism from `X` to `Y`.
More concisely: For any topological spaces `X`, `Y`, `Z`, a homeomorphism `h: X \to Y`, and a function `f: Y \to Z`, the continuity of `f` if and only if of `f �circ h`.
|
Homeomorph.surjective
theorem Homeomorph.surjective :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Function.Surjective ⇑h
The theorem `Homeomorph.surjective` states that for any two types `X` and `Y`, where `X` and `Y` are topological spaces (denoted by the instances `TopologicalSpace X` and `TopologicalSpace Y`), if `h` is a homeomorphism from `X` to `Y` (denoted by `X ≃ₜ Y`), then the function `h` is surjective. In other words, for every element `y` in `Y`, there exists an element `x` in `X` such that `h(x)` equals `y`. This implies that every point in the topological space `Y` is the image of some point in the topological space `X` under the homeomorphism `h`.
More concisely: If `X` and `Y` are topological spaces and `h : X ≃ₜ Y` is a homeomorphism, then `h` is a surjective function.
|
Homeomorph.isSigmaCompact_image
theorem Homeomorph.isSigmaCompact_image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
IsSigmaCompact (⇑h '' s) ↔ IsSigmaCompact s
The theorem `Homeomorph.isSigmaCompact_image` states that for any two types `X` and `Y` with their respective topological spaces, given a set `s` of type `X` and a homeomorphism `h` from `X` to `Y`, the image of `s` under `h` is σ-compact (i.e., is the union of countably many compact sets) if and only if `s` itself is σ-compact. In other words, the property of being σ-compact is preserved under a homeomorphism.
More concisely: A homeomorphism preserves the property of being σ-compact, that is, if a subset of a topological space is σ-compact, then its image under a homeomorphism is also σ-compact, and vice versa.
|
Homeomorph.embedding
theorem Homeomorph.embedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Embedding ⇑h
This theorem states that for every homeomorphism `h` between two types `X` and `Y`, where both `X` and `Y` are topological spaces, the function resulting from applying `h` is an embedding. In other words, homeomorphisms are always embeddings in the context of topological spaces.
More concisely: Every homeomorphism between topological spaces is an embedding.
|
Homeomorph.isClosed_image
theorem Homeomorph.isClosed_image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X},
IsClosed (⇑h '' s) ↔ IsClosed s
The theorem `Homeomorph.isClosed_image` states that for any two types `X` and `Y` with associated topological spaces, given a homeomorphism `h` from `X` to `Y` and a set `s` of type `X`, the image of `s` under `h` is closed if and only if `s` itself is closed. This theorem can be used to check whether a set is closed after being mapped by a homeomorphism, by checking the closedness of the original set.
More concisely: A homeomorphism preserves closed sets, that is, for any homeomorphism between topological spaces and any subset, the image of a closed set is closed.
|
Homeomorph.ext
theorem Homeomorph.ext :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {h h' : X ≃ₜ Y},
(∀ (x : X), h x = h' x) → h = h'
This theorem states that for any two types `X` and `Y`, each with an instance of a topological space, and given two homeomorphisms `h` and `h'` between `X` and `Y`, if for all `x` in `X`, the application of `h` and `h'` to `x` results in the same outcome, then `h` and `h'` are the same homeomorphism. In other words, two homeomorphisms between two topological spaces are identical if they map every point in the source space to the same point in the target space.
More concisely: Two homeomorphisms between topological spaces are equal if they map each point in the source space to the same point in the target space.
|
Homeomorph.image_interior
theorem Homeomorph.image_interior :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
⇑h '' interior s = interior (⇑h '' s)
This theorem states that for any two types `X` and `Y` equipped with respective topological spaces (`TopologicalSpace X` and `TopologicalSpace Y`), if there is a homeomorphism `h` between `X` and `Y`, then the image under `h` of the interior of a set `s` of type `X` (denoted `⇑h '' interior s`) is equal to the interior of the image of set `s` under the homeomorphism `h` (denoted `interior (⇑h '' s)`). In simpler terms, it asserts that a homeomorphism preserves the concept of "interior of a set" when mapping from one topological space to another.
More concisely: Given topological spaces `X` and `Y` with homeomorphism `h`, the interior of `h(s)` is equal to `h(interior s)` for any set `s` in `X`.
|
Homeomorph.isOpenMap
theorem Homeomorph.isOpenMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
IsOpenMap ⇑h
The theorem `Homeomorph.isOpenMap` states that for any two types `X` and `Y` equipped with topological spaces, if there exists a homeomorphism `h` from `X` to `Y`, then the function `h` is an open map. In other words, for any open set `U` in `X`, its image under `h` will also be an open set in `Y`. A homeomorphism is a bijective function that is continuous, and its inverse is also continuous. An open map, as defined in the preamble, is a function for which the image of any open set is also an open set.
More concisely: Given types equipped with topological spaces `X` and `Y`, if there exists a homeomorphism `h` from `X` to `Y`, then `h` maps open sets in `X` to open sets in `Y`.
|
Homeomorph.continuous
theorem Homeomorph.continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Continuous ⇑h
This theorem states that for any two types `X` and `Y`, given that both `X` and `Y` are topological spaces, if there is a homeomorphism between `X` and `Y`, then the application of this homeomorphism is a continuous function. In other words, it preserves the topological structures of `X` and `Y`, demonstrating one of the key properties of homeomorphisms in topology.
More concisely: Given topological spaces X and Y and a homeomorphism f : X ↔ Y, the function f is continuous.
|
Homeomorph.isSigmaCompact_preimage
theorem Homeomorph.isSigmaCompact_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s
The theorem `Homeomorph.isSigmaCompact_preimage` states that for any given topological spaces `X` and `Y`, and a set `s` of `Y`, if there is a homeomorphism `h` from `X` to `Y`, then the preimage of `s` under `h` (denoted as `h⁻¹(s)`) is σ-compact if and only if `s` is σ-compact. In other words, the property of σ-compactness is preserved under the inverse of a homeomorphism. Here, σ-compactness means that a set can be expressed as the union of countably many compact sets, and a homeomorphism is a continuous, bijective map between two topological spaces whose inverse is also continuous.
More concisely: If `h` is a homeomorphism between topological spaces `X` and `Y`, then `h⁻¹(σ-compact set `s`) is σ-compact if and only if `s` is σ-compact.
|
Homeomorph.continuous_invFun
theorem Homeomorph.continuous_invFun :
∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : X ≃ₜ Y),
Continuous self.invFun
This theorem states that for any homeomorphism between two topological spaces, X and Y, the inverse function of the homeomorphism is continuous. In other words, if you have a continuous function that forms a one-to-one correspondence (bijection) between every point in X and Y, and its inverse function maps every point in Y back to X, then this inverse function is also continuous. This property is essential in the study of topological spaces and forms the basis for the concept of a homeomorphism, a key component in topology.
More concisely: If X and Y are topological spaces and f : X ↔ Y is a homeomorphism, then the inverse function g : Y ↔ X of f is continuous.
|
Homeomorph.continuous_toFun
theorem Homeomorph.continuous_toFun :
∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : X ≃ₜ Y),
Continuous self.toFun
This theorem states that for any homeomorphism between two topological spaces X and Y, the forward map of the homeomorphism is a continuous function. In other words, given any two types X and Y with their respective topological spaces, and a homeomorphism `self` from X to Y, the function `self.toFun` that maps elements of X to Y is a continuous function.
More concisely: Given any topological spaces X and Y and a homeomorphism f : X -> Y, the function f is continuous.
|
Homeomorph.comap_nhds_eq
theorem Homeomorph.comap_nhds_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y),
Filter.comap (⇑h) (nhds y) = nhds (h.symm y)
The theorem `Homeomorph.comap_nhds_eq` states that for any topological spaces `X` and `Y`, and a homeomorphism `h` from `X` to `Y`, the result of applying the comap function to the neighborhood filter `nhds` at a point `y` in `Y` and the function defined by `h`, is equal to the neighborhood filter at the image of `y` under the inverse of `h`. In other words, precomposing the neighborhood filter of a point in `Y` with a homeomorphism gives the neighborhood filter of its preimage in `X`.
More concisely: For any topological spaces X and Y and a homeomorphism h: X -> Y, the preimage of the neighborhood filter of y in Y under h is equal to the neighborhood filter of h\*(y) in X.
|
Homeomorph.isCompact_image
theorem Homeomorph.isCompact_image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
IsCompact (⇑h '' s) ↔ IsCompact s
The theorem `Homeomorph.isCompact_image` states that for any homeomorphism `h` from a topological space `X` to another topological space `Y` and for any subset `s` of `X`, the image of `s` under `h` is compact if and only if `s` itself is compact. In other words, compactness is preserved under a homeomorphism.
More concisely: A homeomorphism preserves compact sets: for any homeomorphism h between topological spaces X and Y, and any compact subset s of X, the image h(s) is a compact subset of Y.
|
Homeomorph.symm_apply_apply
theorem Homeomorph.symm_apply_apply :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
h.symm (h x) = x
The theorem `Homeomorph.symm_apply_apply` states that for any two topological spaces `X` and `Y`, and a given homeomorphism `h` from `X` to `Y`, applying the homeomorphism `h` to a point `x` in `X` and then applying the inverse homeomorphism `Homeomorph.symm h` to the result, we recover the original point `x`. In mathematical terms, this theorem asserts that for any homeomorphism and its inverse, the composition of these two maps is the identity on `X`.
More concisely: For any homeomorphism $h$ between topological spaces $X$ and $Y$, $h \circ \text{Homeomorph.symm } h = \text{id}_X$, where $\text{id}_X$ is the identity map on $X$.
|
Homeomorph.self_comp_symm
theorem Homeomorph.self_comp_symm :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
⇑h ∘ ⇑h.symm = id
The theorem `Homeomorph.self_comp_symm` states that for any two topological spaces `X` and `Y`, if there is a homeomorphism `h` from `X` to `Y`, then composing `h` with its inverse (as given by the `Homeomorph.symm` function) yields the identity function. In other words, applying `h` followed by its inverse is equivalent to doing nothing, which is a fundamental property of homeomorphisms in topology.
More concisely: For any topological spaces X and Y with a homeomorphism h : X ↔ Y, h ∘ Homeomorph.symm h = id\_X and Homeomorph.symm h ∘ h = id\_Y, where id\_X and id\_Y are the identity functions on X and Y, respectively.
|