PartialHomeomorph.IsImage.of_symm_preimage_eq
theorem PartialHomeomorph.IsImage.of_symm_preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t
This theorem states that for any two types `X` and `Y`, both of which are topological spaces, given a partial homeomorphism `e` between `X` and `Y`, and sets `s` of type `X` and `t` of type `Y`, if the intersection of `e`'s target and the preimage of `s` under `e.symm` (the inverse of `e`) equals the intersection of `e`'s target and `t`, then `e` is an image of `s` and `t`. In other words, it says that if two sets appear to have the same "shape" under the partial homeomorphism `e` and its inverse, then `e` maps `s` onto `t`.
More concisely: If `e` is a partial homeomorphism between topological spaces `X` and `Y`, and the inverse images of sets `s` in `X` and `t` in `Y` intersect `e(X)` identically, then `s` is the image of `t` under `e`.
|
PartialHomeomorph.isOpen_image_of_subset_source
theorem PartialHomeomorph.isOpen_image_of_subset_source :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {s : Set X}, IsOpen s → s ⊆ e.source → IsOpen (↑e '' s)
The theorem `PartialHomeomorph.isOpen_image_of_subset_source` states that a partial homeomorphism is an open mapping on its source set. More specifically, it means that for any types `X` and `Y` equipped with topological spaces, given a partial homeomorphism `e` from `X` to `Y` and a set `s` in `X` that is open and is a subset of the source of `e`, the image of `s` under `e` (denoted as `e '' s`) is also an open set. Thus, it assures the preservation of open sets under partial homeomorphisms, which is a key property in topology.
More concisely: Given a partial homeomorphism between topological spaces, the image of any open and subset of its source set is an open set.
|
PartialHomeomorph.toPartialEquiv_injective
theorem PartialHomeomorph.toPartialEquiv_injective :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Function.Injective PartialHomeomorph.toPartialEquiv
This theorem states that for any two types `X` and `Y` that are both topological spaces, the function `PartialHomeomorph.toPartialEquiv` is injective. In other words, for any two partial homeomorphisms between `X` and `Y`, if they are equal when mapped to partial equivalences via `PartialHomeomorph.toPartialEquiv`, then they were originally equal as partial homeomorphisms. This emphasizes that the `PartialHomeomorph.toPartialEquiv` function preserves the distinctness of partial homeomorphisms when converting them to partial equivalences.
More concisely: The function `PartialHomeomorph.toPartialEquiv` maps equal partial homeomorphisms between topological spaces `X` and `Y` to equal partial equivalences.
|
PartialHomeomorph.isOpen_image_symm_of_subset_target
theorem PartialHomeomorph.isOpen_image_symm_of_subset_target :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {t : Set Y}, IsOpen t → t ⊆ e.target → IsOpen (↑e.symm '' t)
The theorem `PartialHomeomorph.isOpen_image_symm_of_subset_target` states that for any given types `X` and `Y` along with their respective topological spaces and a partial homeomorphism `e` from `X` to `Y`, if there is a set `t` in `Y` that is open and is a subset of the target of `e`, then the image of `t` under the inverse of `e` is an open set in `X`. In other words, the inverse of a partial homeomorphism acts as an open map from its target to its source.
More concisely: Let `e` be a partial homeomorphism from topological spaces `X` and `Y`, if `t` is an open subset of `Y` that is contained in the target of `e`, then the inverse image of `t` under `e` is an open subset of `X`.
|
PartialHomeomorph.EqOnSource.target_eq
theorem PartialHomeomorph.EqOnSource.target_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → e.target = e'.target
This theorem states that if two partial homeomorphisms (which are functions between topological spaces that have a continuous inverse) are equivalent, then they have the same target space. It applies to any two partial homeomorphisms `e` and `e'` between any topological spaces `X` and `Y`. In the language of mathematics, if `e` and `e'` are partial homeomorphisms from `X` to `Y` and `e` is equivalent to `e'`, then the target of `e` is the same as the target of `e'`.
More concisely: If two partial homeomorphisms between topological spaces are equivalent, they have the same target space.
|
PartialHomeomorph.IsImage.symm
theorem PartialHomeomorph.IsImage.symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.symm.IsImage t s
This theorem states that for any given topological spaces `X` and `Y`, a partial homeomorphism `e` from `X` to `Y`, and two sets `s` in `X` and `t` in `Y`, if `t` is an image of `s` under the partial homeomorphism `e` (formally, `PartialHomeomorph.IsImage e s t` holds), then `s` is also an image of `t` under the inverse of the partial homeomorphism `e` (formally, `PartialHomeomorph.IsImage (PartialHomeomorph.symm e) t s` holds). This means that the property of being an image under a partial homeomorphism is symmetric with respect to the homeomorphism and its inverse.
More concisely: If a set is an image of another under a partial homeomorphism, then the other set is an image of the first under the partial homeomorphism's inverse.
|
PartialHomeomorph.IsImage.iff_symm_preimage_eq'
theorem PartialHomeomorph.IsImage.iff_symm_preimage_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y},
e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
This theorem states that for any partial homeomorphism `e` between two topological spaces `X` and `Y`, and for any two sets `s` in `X` and `t` in `Y`, the set `t` is an image of the set `s` under the partial homeomorphism `e` if and only if the intersection of the target of `e` with the preimage under the inverse of `e` of the intersection of the source of `e` and `s` is equal to the intersection of the target of `e` and `t`. This theorem provides a convenient condition in terms of set operations and inverse images for verifying when a set is an image of another set under a partial homeomorphism.
More concisely: For a partial homeomorphism between topological spaces, a set is the image of another set if and only if their intersections with the respective preimages under the inverse map have equal intersections.
|
PartialHomeomorph.restr_source
theorem PartialHomeomorph.restr_source :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) (s : Set X), (e.restr s).source = e.source ∩ interior s
This theorem states that for any types `X` and `Y`, which are equipped with respective topological spaces, a partial homeomorphism `e` from `X` to `Y`, and a set `s` of type `X`, the source of the restriction of `e` to `s` is equal to the intersection of the source of `e` and the interior of `s`. Here, a partial homeomorphism is a homeomorphism between a subset of `X` and a subset of `Y`, restriction of `e` to `s` means we are considering `e` only on the set `s`, and the interior of a set `s` in topology is the largest open subset of `s`.
More concisely: Given types `X` and `Y` with topological spaces, a partial homeomorphism `e` from `X` to `Y`, and a subset `s` of `X`, the restriction of `e` to `s` is equal to the restriction of `e` to the interior of `s`. (Note: "restriction of `e` to `s`" refers to the homeomorphism from `s` to `e(s)`.)
|
PartialHomeomorph.preimage_interior
theorem PartialHomeomorph.preimage_interior :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) (s : Set Y), e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑e ⁻¹' s)
The theorem `PartialHomeomorph.preimage_interior` states that for any partial homeomorphism `e` from a space `X` to a space `Y` and a set `s` of `Y`, the intersection of the source of `e` and the preimage of the interior of `s` under `e` is equal to the intersection of the source of `e` and the interior of the preimage of `s` under `e`. In other words, when a partial homeomorphism is restricted to its source, taking the preimage of the interior of a set and taking the interior of the preimage of a set are equivalent operations.
More concisely: For any partial homeomorphism between topological spaces and any set, the preimage of the interior of that set is equal to the interior of the preimage under the partial homeomorphism.
|
PartialHomeomorph.symm_mapsTo
theorem PartialHomeomorph.symm_mapsTo :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), Set.MapsTo (↑e.symm) e.target e.source
This theorem states that for any given partial homeomorphism `e` between two topological spaces `X` and `Y`, the inverse of `e` maps the target of `e` into its source. In other words, if `e` is a partial homeomorphism function from a subset of `X` to a subset of `Y`, then the inverse function of `e`, denoted as `e^-1` or `PartialHomeomorph.symm e`, maps any point in the target subset of `Y` back to the original subset in `X`. This is a property usually expected from the concept of inverse functions.
More concisely: If `e` is a partial homeomorphism from a subset of `X` to a subset of `Y`, then `e^-1` (or `PartialHomeomorph.symm e`) maps the target of `e` back to its source in `X`.
|
PartialHomeomorph.continuousOn_iff_continuousOn_comp_right
theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_right :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Y → Z} {s : Set Y},
s ⊆ e.target → (ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s))
The theorem `PartialHomeomorph.continuousOn_iff_continuousOn_comp_right` states that for all topological spaces `X`, `Y`, and `Z`, a given partial homeomorphism `e` from `X` to `Y`, a function `f` from `Y` to `Z`, and a set `s` in `Y` that is a subset of the target of `e`, the function `f` is continuous on `s` if and only if the composition of `f` with the inclusion of `e` is continuous on the intersection of the source of `e` with the preimage of `s` under `e`. In other words, the continuity of a function on a set is equivalent to the continuity of its composition with a partial homeomorphism on the corresponding set.
More concisely: For a partial homeomorphism \(e: X \rightarrow Y\) and functions \(f: Y \rightarrow Z\) and \(g: \text{dom}(e) \rightarrow Y\) the inclusion of \(e\), the continuity of \(f\) on \(g^{-1}(s)\) is equivalent to the continuity of \(f \circ e\) on \(e^{-1}(s)\), where \(s \subseteq \text{rge}(e)\).
|
PartialHomeomorph.image_source_inter_eq'
theorem PartialHomeomorph.image_source_inter_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
The theorem `PartialHomeomorph.image_source_inter_eq'` states that for any given partial homeomorphism `e` from a set `X` to a set `Y`, where both `X` and `Y` are equipped with a topological structure, and for any subset `s` of `X`, the image of the intersection of `e.source` and `s` under the mapping `e` is equal to the intersection of `e.target` and the preimage of `s` under the inverse of the partial homeomorphism `e`. Here, `e.source` refers to the domain of definition of the partial homeomorphism `e` and `e.target` refers to the set `Y`. This theorem connects the concepts of image, preimage, intersection, and inverses in the context of partial homeomorphisms between topological spaces.
More concisely: For any partial homeomorphism between topological spaces, the image of the intersection of its domain and a subset is equal to the intersection of its range and the preimage of that subset under its inverse.
|
PartialHomeomorph.EqOnSource.source_eq
theorem PartialHomeomorph.EqOnSource.source_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → e.source = e'.source
This theorem states that if two partial homeomorphisms, denoted as `e` and `e'`, are equivalent in a topological space context, then their sources must be the same. Here, `X` and `Y` are types representing the spaces, each equipped with a topological space structure. A partial homeomorphism is a homeomorphism (continuous, bijective map with a continuous inverse) defined on a subset of the space. The equivalence of two partial homeomorphisms here implies that they are defined on the same subset of the space and coincide on that subset.
More concisely: If two partial homeomorphisms `e` and `e'` are equivalent on a topological space `(X, top)`, then their domains (sets on which they are defined) are equal.
|
PartialHomeomorph.EqOnSource.eqOn
theorem PartialHomeomorph.EqOnSource.eqOn :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → Set.EqOn (↑e) (↑e') e.source
The theorem `PartialHomeomorph.EqOnSource.eqOn` states that for any two partial homeomorphisms `e` and `e'` between two topological spaces `X` and `Y`, if `e` and `e'` are equivalent, then the functions `e` and `e'` (denoted as `↑e` and `↑e'`) are equal on the source set of `e`. In other words, for all elements in the source set of `e`, the output of function `e` and function `e'` is the same. This assumes that the types `X` and `Y` are topological spaces.
More concisely: If two partial homeomorphisms between topological spaces have equivalent relations, then their underlying functions agree on the source set of the first partial homeomorphism.
|
PartialHomeomorph.isOpen_image_source_inter
theorem PartialHomeomorph.isOpen_image_source_inter :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {s : Set X}, IsOpen s → IsOpen (↑e '' (e.source ∩ s))
This theorem states that, given any two types `X` and `Y` equipped with topological spaces, and a partial homeomorphism `e` from `X` to `Y`, for any open set `s` in `X`, the image of the restriction of `s` to the source of `e` is also an open set in `Y`. In other words, if we restrict an open set `s` to only include points that are in the source of `e` and then apply `e` to this restricted set, the resulting set is open in `Y`. This theorem is a property of topological spaces and homeomorphisms - it illustrates how homeomorphisms preserve the topological structure.
More concisely: Given a topological space `(X, τX)`, a topological space `(Y, τY)`, and a partial homeomorphism `e : X ↠ Y`, if `s ∈ τX` then `e''(s) ∈ τY`, where `e''(s)` denotes the image of `s` under `e`.
|
OpenEmbedding.toPartialHomeomorph_target
theorem OpenEmbedding.toPartialHomeomorph_target :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
(h : OpenEmbedding f) [inst_2 : Nonempty X], (OpenEmbedding.toPartialHomeomorph f h).target = Set.range f
This theorem states that for any two types `X` and `Y` equipped with topological spaces, and a function `f` from `X` to `Y`, if `f` is an open embedding and `X` is nonempty, then the target of the partial homeomorphism obtained from this open embedding via `OpenEmbedding.toPartialHomeomorph` is equal to the range of `f`. In other words, the set of points in `Y` that are the image of the partial homeomorphism are exactly the set of points in `Y` that are mapped by `f` from some point in `X`.
More concisely: If `f` is an open embedding from a nonempty topological space `X` to `Y`, then the range of `f` equals the image of the partial homeomorphism obtained from `f`.
|
PartialHomeomorph.image_source_eq_target
theorem PartialHomeomorph.image_source_eq_target :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), ↑e '' e.source = e.target
This theorem states that for any given partial homeomorphism `e` between two topological spaces `X` and `Y`, the image of the source set of `e` under the function `e` is equal to the target set of `e`. In other words, if you apply the partial homeomorphism `e` to every point in its source set, you'll get exactly the target set. This is a fundamental property that reflects the idea of a homeomorphism being a bijective correspondence between two topological spaces that preserves the structure of the spaces.
More concisely: For any partial homeomorphism between topological spaces, the image of its domain is equal to the range.
|
PartialHomeomorph.continuousAt_symm
theorem PartialHomeomorph.continuousAt_symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : Y}, x ∈ e.target → ContinuousAt (↑e.symm) x
The theorem `PartialHomeomorph.continuousAt_symm` states that for any two topological spaces `X` and `Y`, and for any partial homeomorphism `e` from `X` to `Y`, the inverse of `e` is continuous at any point `x` that belongs to the target of `e`. In other words, if we have a partial homeomorphism between two topological spaces, then the inverse function of this homeomorphism is always continuous at the points in its target set.
More concisely: Given any partial homeomorphism `e: X ↫ Y` between topological spaces, the inverse `e⁻¹` is continuous at every point `x ∈ e(X)`.
|
PartialHomeomorph.right_inv
theorem PartialHomeomorph.right_inv :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : Y}, x ∈ e.target → ↑e (↑e.symm x) = x
The theorem `PartialHomeomorph.right_inv` states that for any two topological spaces `X` and `Y`, along with a partial homeomorphism `e` from `X` to `Y`, if a point `x` belongs to the target set of `e`, then applying `e` to the inverse of `x` under the symmetry operation of `e` (denoted by `PartialHomeomorph.symm e`) will give back `x`. In other words, the partial homeomorphism `e` and its inverse `PartialHomeomorph.symm e` cancel each other on the target set of `e`, acting as the right inverse of each other.
More concisely: For any partial homeomorphisms $e: X \rightarrow Y$ and $x \in \operatorname{rge}(e)$, we have $e(\operatorname{symm}_e(x)) = x$, where $\operatorname{symm}_e(x)$ denotes the symmetry of $x$ with respect to $e$.
|
PartialHomeomorph.mapsTo
theorem PartialHomeomorph.mapsTo :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), Set.MapsTo (↑e) e.source e.target
The theorem `PartialHomeomorph.mapsTo` states that for all types `X` and `Y`, which are equipped with a topological space structure, and any partial homeomorphism `e` from `X` to `Y`, the function `e` maps its source set into its target set. In other words, if an element belongs to the source set of `e`, its image under `e` belongs to the target set of `e`.
More concisely: For any partial homeomorphism between topological spaces `e : X ↫ Y`, the domain of `e` is a subset of the range of `e`.
|
PartialHomeomorph.continuousOn_symm
theorem PartialHomeomorph.continuousOn_symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), ContinuousOn (↑e.symm) e.target
The theorem `PartialHomeomorph.continuousOn_symm` states that for any two types `X` and `Y` both equipped with a topological space structure, and given a partial homeomorphism `e` from `X` to `Y`, the inverse function (or the symmetry) of the given partial homeomorphism is continuous on the target set of the original partial homeomorphism.
In mathematical terms, if we have a partial homeomorphism `e : X → Y`, then the inverse function `e^-1` is continuous on the image of `e`.
More concisely: If `e : X → Y` is a partial homeomorphism, then the inverse function `e^-1` is continuous on the image of `e`.
|
PartialHomeomorph.IsImage.toPartialEquiv
theorem PartialHomeomorph.IsImage.toPartialEquiv :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage s t
This theorem states that for any two topological spaces X and Y, a partial homeomorphism `e` from X to Y, and sets `s` of X and `t` of Y, if `t` is an image of `s` under the partial homeomorphism `e` (i.e., `PartialHomeomorph.IsImage e s t` holds), then `t` is also an image of `s` under the partial equivalence formed by the partial homeomorphism `e` (i.e., `PartialEquiv.IsImage e.toPartialEquiv s t` holds). In other words, the image relationship of a set under a partial homeomorphism is preserved when the homeomorphism is considered as a partial equivalence.
More concisely: If `e` is a partial homeomorphism from topological spaces X to Y, and s subset of X is the image of t subset of Y under `e` (PartialHomeomorph.IsImage e s t), then t is the image of s under the partial equivalence formed by `e` (PartialEquiv.IsImage e.toPartialEquiv s t).
|
PartialHomeomorph.map_nhds_eq
theorem PartialHomeomorph.map_nhds_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → Filter.map (↑e) (nhds x) = nhds (↑e x)
This theorem, `PartialHomeomorph.map_nhds_eq`, asserts that for any two types `X` and `Y` equipped with topological space structures, and for a partial homeomorphism `e` from `X` to `Y`, if a point `x` belongs to the source of `e`, then the forward map of the filter of neighborhood of `x` under `e` is equal to the neighborhood of the image of `x` under `e`. In other words, a partial homeomorphism maps the neighborhood filter of a point in its source to the neighborhood filter of its image. This is a property that we would expect from any structure preserving map between topological spaces.
More concisely: Given types equipped with topological structures `X` and `Y`, and a partial homeomorphism `e` from `X` to `Y`, if `x` is in the domain of `e`, then the filter of neighborhoods of `x` in `X` is mapped to the filter of neighborhoods of `e(x)` in `Y` under `e`.
|
PartialHomeomorph.symm_trans_self
theorem PartialHomeomorph.symm_trans_self :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), e.symm.trans e ≈ PartialHomeomorph.ofSet e.target ⋯
This theorem states that for any partial homeomorphism `e` from a topological space `X` to another topological space `Y`, the composition of the inverse of `e` (as given by `PartialHomeomorph.symm e`) followed by `e` itself is equivalent to the identity partial homeomorphism on the set `e.target`. This identity partial homeomorphism is given by `PartialHomeomorph.ofSet e.target`, where `e.target` is the target set of the partial homeomorphism `e`. In essence, this theorem highlights an important property of partial homeomorphisms: namely, that they preserve the topological structure when inverted and then composed with the original homeomorphism.
More concisely: For any partial homeomorphism `e` from topological space `X` to `Y`, `PartialHomeomorph.symm e ∘ e = PartialHomeomorph.ofSet e.target`.
|
PartialHomeomorph.IsImage.closure
theorem PartialHomeomorph.IsImage.closure :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage (closure s) (closure t)
The theorem `PartialHomeomorph.IsImage.closure` states that for any two topological spaces `X` and `Y`, and any partial homeomorphism `e` from `X` to `Y`, if a set `t` in `Y` is an image of a set `s` in `X` under the partial homeomorphism `e`, then the closure of `t` is also an image of the closure of `s` under the same partial homeomorphism. In other words, the closure of the image of a set under a partial homeomorphism is the image of the closure of that set under the same partial homeomorphism. The closure of a set is the smallest closed set containing it, and a partial homeomorphism is a bijection between subsets of the topological spaces that is continuous with a continuous inverse.
More concisely: For any topological spaces X and Y, and a partial homeomorphism e from X to Y, the image under e of the closure of a set in X is equal to the closure of the image of that set in Y.
|
PartialHomeomorph.IsImage.of_preimage_eq
theorem PartialHomeomorph.IsImage.of_preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t
This theorem, which is an alias of the reverse direction of `PartialHomeomorph.IsImage.iff_preimage_eq`, states that for any types `X` and `Y` with an associated topological space, for any partial homeomorphism `e` from `X` to `Y`, and for any sets `s` of `X` and `t` of `Y`, if the intersection of the source of `e` and the preimage of `t` under `e` equals the intersection of the source of `e` and `s`, then `t` is an image of `s` under the partial homeomorphism `e`. In other words, given specific conditions on the source of the homeomorphism and the sets, we can conclude that the set `t` can be obtained by mapping the set `s` under the homeomorphism `e`.
More concisely: If the source of a partial homeomorphism from X to Y and the preimage of a set t under this homeomorphism intersect equally with a given set s from the source, then t is the image of s under the homeomorphism.
|
PartialHomeomorph.continuous_iff_continuous_comp_left
theorem PartialHomeomorph.continuous_iff_continuous_comp_left :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Z → X},
f ⁻¹' e.source = Set.univ → (Continuous f ↔ Continuous (↑e ∘ f))
The theorem states that for all types `X`, `Y`, and `Z`, each with a topological space structure, and given a partial homeomorphism `e` from `X` to `Y` and a function `f` from `Z` to `X`, if the preimage of the source of `e` under `f` is the universal set, then `f` is continuous if and only if the composition of `e` and `f` is continuous. This theorem bridges the gap between the continuity of a function and the continuity of its composition with a partial homeomorphism.
More concisely: Given types `X`, `Y`, `Z` with topological spaces structures, a partial homeomorphism `e` from `X` to `Y`, and a function `f` from `Z` to `X`, if `e ∘ f` is continuous and the preimage of the domain of `e` under `f` is the universal set, then `f` is continuous.
|
PartialHomeomorph.injOn
theorem PartialHomeomorph.injOn :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), Set.InjOn (↑e) e.source
The theorem `PartialHomeomorph.injOn` states that for any two topological spaces `X` and `Y`, any partial homeomorphism `e` from `X` to `Y` is injective on its source set. This means that if `x₁` and `x₂` are any two elements in the source set where `x₁` is not equal to `x₂`, then their images under the partial homeomorphism `e`, i.e., `e(x₁)` is not equal to `e(x₂)`.
More concisely: For any partial homeomorphism between topological spaces, its source set elements map distinctly to their images.
|
PartialHomeomorph.IsImage.preimage_eq
theorem PartialHomeomorph.IsImage.preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s
This theorem, named `PartialHomeomorph.IsImage.preimage_eq`, states the following:
For any types `X` and `Y` equipped with topological spaces, a partial homeomorphism `e` from `X` to `Y`, and sets `s` of `X` and `t` of `Y`, if `t` is an image of `s` under the partial homeomorphism `e`, then the intersection of the source of `e` with the preimage of `t` under `e` is equal to the intersection of the source of `e` with `s`.
Simply put, it means that when set `t` is formed by applying the partial homeomorphism `e` on set `s`, the elements of `s` that are mapped by `e` match exactly with those elements of `t` that are associated with the source of `e` through the inverse mapping of `e`.
More concisely: If `e: X ↪ Y` is a partial homeomorphism, `s ⊆ X`, and `t = e''(s)`, then `s ∩ e^(-1)(t) = s`.
|
PartialHomeomorph.IsImage.symm_preimage_eq
theorem PartialHomeomorph.IsImage.symm_preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
The theorem `PartialHomeomorph.IsImage.symm_preimage_eq` states that for any two types `X` and `Y` which are topological spaces, given a partial homeomorphism `e` from `X` to `Y`, and two sets `s` of type `X` and `t` of type `Y`, if `s` is an image of `t` under the partial homeomorphism `e`, then the intersection of the target of `e` and the preimage of `s` under the inverse of `e` is equal to the intersection of the target of `e` and `t`. Here, the preimage of a set under a function is the set of all elements that map to that set under the given function.
More concisely: If `e: X ↪ Y` is a partial homeomorphism, `s ⊆ X` is the image of `t ⊆ Y` under `e`, then `e.symm '' t ∩ e `(X) = s ∩ e `(X)`.
|
PartialHomeomorph.IsImage.symm_preimage_eq'
theorem PartialHomeomorph.IsImage.symm_preimage_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y},
e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
This theorem, which is an alias of the forward direction of `PartialHomeomorph.IsImage.iff_symm_preimage_eq'`, states that for any two types `X` and `Y` equipped with topological space structures, any partial homeomorphism `e` from `X` to `Y`, and any sets `s` of `X` and `t` of `Y`, if `s` is the image of `t` under `e`, then the intersection of the target of `e` and the preimage of the intersection of the source of `e` and `s` under the inverse of `e`, is equal to the intersection of the target of `e` and `t`. This can be seen as a property about the interaction between partial homeomorphisms and the sets they map, specifically their sources, targets, and images.
More concisely: For any partial homeomorphism between topological spaces and any sets, the preimage of the intersection of the source and the image under the inverse, equals the intersection of the image and the preimage.
|
PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right
theorem PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Y → Z} {s : Set Y} {x : Y},
x ∈ e.target → (ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x))
This theorem states that for any three topological spaces X, Y and Z, a partial homeomorphism from X to Y, a function from Y to Z, a set of elements from Y, and a point in Y that lies in the target of the partial homeomorphism, the function is continuous within the set at the point if and only if the function composed with the inverse of the partial homeomorphism is continuous within the preimage of the set under the partial homeomorphism at the point mapped by the inverse of the partial homeomorphism. This allows us to understand the continuity of the function within a set at a point via the continuity of its composition with a local homeomorphism.
More concisely: For any partial homeomorphisms f: X → Y and g: Y → Z, sets S ⊆ Y, and points x ∈ X with f(x) ∈ S, g is continuous at f(x) with respect to S if and only if g ∘ f^(-1) is continuous at x with respect to f^(-1)[S].
|
PartialHomeomorph.tendsto_symm
theorem PartialHomeomorph.tendsto_symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → Filter.Tendsto (↑e.symm) (nhds (↑e x)) (nhds x)
This theorem states that for any two types `X` and `Y` that are equipped with topological spaces, given a partial homeomorphism `e` from `X` to `Y` and any element `x` from `X` that belongs to the source of `e`, the inverse function of `e` tends to the limit from the filter neighborhood of the image of `x` under `e` to the filter neighborhood of `x`. In other words, for any neighborhood of `x`, the pre-image under the inverse function of `e` of that neighborhood is a neighborhood of the image of `x` under `e`. This is a property of continuous functions in topological spaces.
More concisely: Given a continuous partial homeomorphism `e` between topological spaces `X` and `Y`, for every `x` in `X` and every neighborhood `V` of `e(x)` in `Y`, there exists a neighborhood `U` of `x` in `X` such that `e(U)` is a subset of `V` and `e⁻¹(V)` is a neighborhood of `x` in `X`.
|
Mathlib.Topology.PartialHomeomorph._auxLemma.20
theorem Mathlib.Topology.PartialHomeomorph._auxLemma.20 :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
Continuous f = ContinuousOn f Set.univ
This theorem states that for any types `α` and `β` with respective topological spaces, and for any function `f` from `α` to `β`, the function `f` is continuous if and only if it is continuous on the universal set `Set.univ`. Here, the universal set `Set.univ` is simply the set containing all elements of `α`. In other words, in the context of topology, a function is continuous throughout its domain if it is continuous at every point within the domain.
More concisely: A function between topological spaces is continuous if and only if it is continuous on their universal sets.
|
PartialHomeomorph.continuousAt_iff_continuousAt_comp_left
theorem PartialHomeomorph.continuousAt_iff_continuousAt_comp_left :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Z → X} {x : Z},
f ⁻¹' e.source ∈ nhds x → (ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x)
The theorem states that for any given types `X`, `Y`, and `Z` with their respective topological space instances, a partial homeomorphism `e` from `X` to `Y`, a function `f` from `Z` to `X`, and a point `x` in `Z`, if the preimage of `e`'s source under `f` belongs to the neighborhood of `x`, then `f` is continuous at `x` if and only if the composition of `e` and `f` (represented as `↑e ∘ f`) is continuous at `x`. This theorem essentially shows that the property of continuity at a point is preserved when we consider the left composition of the function with a partial homeomorphism, under the condition that a neighborhood of the initial point maps to the source of the partial homeomorphism.
More concisely: Given types `X`, `Y`, `Z` with topological spaces, a partial homeomorphism `e` from `X` to `Y`, a function `f` from `Z` to `X`, and a point `x` in `Z`, if `f''(x)` is in the neighborhood of `e(x)`, then `f` is continuous at `x` if and only if `↑e ∘ f` is continuous at `x`.
|
PartialHomeomorph.map_nhdsWithin_eq
theorem PartialHomeomorph.map_nhdsWithin_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X},
x ∈ e.source → ∀ (s : Set X), Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) (↑e '' (e.source ∩ s))
This theorem states that for any given partial homeomorphism `e` from a type `X` to a type `Y`, both endowed with a topological structure, and for any point `x` from `X` that belongs to the source of `e`, the image under `e` of the "neighborhood within" filter around `x` in any set `s` is equal to the "neighborhood within" filter around the image of `x` under `e` in the image under `e` of the intersection of `s` and the source of `e`.
In other words, the forward map of a filter behaves well under partial homeomorphisms when it comes to "neighborhood within" filters. This means that the topological properties of the neighborhoods of `x` in `X` are preserved when we move to `Y` using the partial homeomorphism `e`.
More concisely: For any partial homeomorphism between topological spaces and any point in the domain, the forward image of the neighborhood filter of that point is equal to the neighborhood filter of its image under the partial homeomorphism in the image space.
|
PartialHomeomorph.continuousOn
theorem PartialHomeomorph.continuousOn :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), ContinuousOn (↑e) e.source
The theorem `PartialHomeomorph.continuousOn` states that for any partial homeomorphism `e` from a topological space `X` to another topological space `Y`, the function represented by `e` is continuous on the source set of `e`. In other words, for every point in the source set of `e`, the function `e` is continuous at that point within the source set.
More concisely: A partial homeomorphism from a topological space to another preserves the continuity of functions on the domain, that is, it is continuous on the source set.
|
PartialHomeomorph.map_source
theorem PartialHomeomorph.map_source :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → ↑e x ∈ e.target
This theorem, `PartialHomeomorph.map_source`, states that for any partial homeomorphism `e` from a topological space `X` to another topological space `Y`, if an element `x` from `X` belongs to the source of `e`, then the image of `x` under `e` will belong to the target of `e`. The theorem is applicable to all types `X` and `Y` that have a topological space structure.
More concisely: For any partial homeomorphism between topological spaces, the image of a source element maps to the target.
|
PartialHomeomorph.ext
theorem PartialHomeomorph.ext :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e e' : PartialHomeomorph X Y),
(∀ (x : X), ↑e x = ↑e' x) → (∀ (x : Y), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'
This theorem states that two partial homeomorphisms, namely `e` and `e'` between two topological spaces `X` and `Y`, are equal if and only if their mapping functions `toFun`, their inverse functions `invFun`, and their `source` sets are equal. It is necessary to specify equality of both `toFun` and `invFun` since only specifying `toFun` and `source` only determines `invFun` on the target set, which is a weaker notion of equality termed `EqOnSource`.
More concisely: Two partial homeomorphisms `e` and `e'` between topological spaces `X` and `Y` are equal if and only if their mapping functions `toFun` and inverse functions `invFun` are equal.
|
PartialHomeomorph.IsImage.frontier
theorem PartialHomeomorph.IsImage.frontier :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage (frontier s) (frontier t)
The theorem `PartialHomeomorph.IsImage.frontier` states that for any two topological spaces `X` and `Y`, and any partial homeomorphism `e` from `X` to `Y`, if a set `t` in `Y` is the image of a set `s` in `X` under the partial homeomorphism `e`, then the frontier of `t` (the set of points between the closure and interior of `t`) is the image of the frontier of `s` (the set of points between the closure and interior of `s`) under the same partial homeomorphism `e`.
This theorem expresses a property of partial homeomorphisms, showing that they preserve not only the structure of sets, but also the structure of their frontiers, which can be considered as the "boundaries" of the sets.
More concisely: For any partial homeomorphism between topological spaces, the image of the frontier of a set under the partial homeomorphism is equal to the frontier of the image of that set.
|
PartialHomeomorph.EqOnSource.symm_eqOn_target
theorem PartialHomeomorph.EqOnSource.symm_eqOn_target :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → Set.EqOn (↑e.symm) (↑e'.symm) e.target
This theorem states that for any two partial homeomorphisms 'e' and 'e'' between two topological spaces 'X' and 'Y', if 'e' and 'e'' are equivalent, then the inverse functions of 'e' and 'e'' coincide on the target set of 'e'. In other words, for all elements in the target set of 'e', the inverse function of 'e' applied to an element is equal to the inverse function of 'e'' applied to the same element.
More concisely: If partial homeomorphisms e and e' between topological spaces X and Y are equivalent, then e^(-1) restricted to the target set of e is equal to e''^(-1) restricted to the same set.
|
PartialHomeomorph.EqOnSource.restr
theorem PartialHomeomorph.EqOnSource.restr :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → ∀ (s : Set X), e.restr s ≈ e'.restr s
The theorem `PartialHomeomorph.EqOnSource.restr` states that for any two types `X` and `Y` equipped with a topological space structure, and any two partial homeomorphisms `e` and `e'` between these types, if `e` is equivalent to `e'`, then the restriction of `e` to a given set `s` of type `X` is equivalent to the restriction of `e'` to the same set `s`. In other words, the process of restricting a partial homeomorphism to a subset respects the equivalence relation between partial homeomorphisms.
More concisely: If partial homeomorphisms `e` and `e'` between topological spaces `X` and `Y` are equivalent, then the restriction of `e` to a subset `s` of `X` is equivalent to the restriction of `e'` to `s`.
|
PartialHomeomorph.symm_symm
theorem PartialHomeomorph.symm_symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), e.symm.symm = e
The theorem `PartialHomeomorph.symm_symm` asserts that for any Partial Homeomorphism `e` from a topological space `X` to another topological space `Y`, applying the `symm` operation twice (taking the inverse of the inverse) returns the original Partial Homeomorphism `e`. This essentially states that taking the inverse of the inverse of a Partial Homeomorphism is an identity operation.
More concisely: For any Partial Homeomorphism `e` from topological space `X` to `Y`, `e.symm.symm = e`.
|
PartialHomeomorph.eventually_left_inverse
theorem PartialHomeomorph.eventually_left_inverse :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y
The theorem `PartialHomeomorph.eventually_left_inverse` states that for any partial homeomorphism `e` between two topological spaces `X` and `Y`, and any point `x` in the source of `e`, there is a neighborhood around `x` (in the neighborhood filter `nhds x`) such that for all points `y` in this neighborhood, applying the inverse of `e` to the image of `y` under `e` gives back `y`. In other words, within this neighborhood, the partial homeomorphism `e` and its inverse effectively cancel each other out when composed in succession.
More concisely: For any partial homeomorphism between topological spaces and any point in its domain, there exists a neighborhood such that applying the inverse and then the homeomorphism maps any point in the neighborhood back to the original point.
|
PartialHomeomorph.continuousOn_iff_continuousOn_comp_left
theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_left :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Z → X} {s : Set Z},
s ⊆ f ⁻¹' e.source → (ContinuousOn f s ↔ ContinuousOn (↑e ∘ f) s)
This theorem states that, given three topological spaces `X`, `Y`, and `Z`, a partial homeomorphism `e` from `X` to `Y`, a function `f` from `Z` to `X`, and a set `s` of elements from `Z`, if `s` is a subset of the preimage of the source of `e` under `f`, then `f` is continuous on `s` if and only if the composition of `e` and `f`, `(↑e ∘ f)`, is continuous on `s`. In other words, a function's continuity on a set is preserved when it is composed on the left with a partial homeomorphism.
More concisely: Given a partial homeomorphism `e` between topological spaces `X` and `Y`, a function `f` from `Z` to `X`, and a subset `s` of `Z` such that the image of `s` under `f` is contained in the domain of `e`, then `f` is continuous on `s` if and only if the composition `(↑e ∘ f)` is continuous on `s`.
|
PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left
theorem PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Z → X} {s : Set Z} {x : Z},
f x ∈ e.source → f ⁻¹' e.source ∈ nhdsWithin x s → (ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x)
This theorem states that for any partial homeomorphism `e` between two topological spaces `X` and `Y`, a function `f` from a third topological space `Z` to `X`, a set `s` of elements of `Z`, and a point `x` in `Z`, if the point `f(x)` is in the source of `e` and the preimage of `e.source` under `f` is in the neighborhood within `s` at `x`, then the continuity of `f` within `s` at `x` is equivalent to the continuity of the composition of `e` and `f` within `s` at `x`. In other words, the continuity of a function at a point within a set can be checked after applying a local homeomorphism, provided a neighborhood of the point is mapped into the source of the homeomorphism.
More concisely: Given a partial homeomorphism `e` between topological spaces `X` and `Y`, a function `f` from a topological space `Z` to `X`, a set `s` of elements of `Z`, and a point `x` in `s`, if `f(x)` is in the domain of `e` and `e.^1(f(x))` is in the neighborhood of `e.source` at `x`, then `f` is continuous at `x` if and only if the composition `e ∘ f` is continuous at `x`.
|
PartialHomeomorph.map_target
theorem PartialHomeomorph.map_target :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : Y}, x ∈ e.target → ↑e.symm x ∈ e.source
The theorem `PartialHomeomorph.map_target` states that for any types `X` and `Y` equipped with topological space structures, given a partial homeomorphism `e` from `X` to `Y`, for any element `x` of `Y` in the target set of `e`, the application of the inverse of `e` to `x` is an element of the source set of `e`. In simpler terms, it says that if `x` is in the target of a partial homeomorphism, its preimage under the inverse homeomorphism is in the source of the original homeomorphism.
More concisely: Given a partial homeomorphism from a topological space `X` to a topological space `Y`, if `x` is in the image of `X` under `f` and `g` is the inverse of `f`, then `g(x)` is in the domain of `f`.
|
PartialHomeomorph.image_source_inter_eq
theorem PartialHomeomorph.image_source_inter_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
The theorem `PartialHomeomorph.image_source_inter_eq` states that for any partial homeomorphism `e` between two topological spaces `X` and `Y`, and for any set `s` of elements in `X`, the image under `e` of the intersection of `e.source` and `s` is equal to the intersection of `e.target` and the preimage under the inverse of `e` of the intersection of `e.source` and `s`. In simpler terms, this theorem is about the relationship between a set in the domain of a partial homeomorphism, its image under the homeomorphism, and its corresponding preimage under the inverse of the homeomorphism.
More concisely: For any partial homeomorphism between topological spaces, the image of the intersection of its source domain and its domain, under the homeomorphism, equals the intersection of its target space and the preimage of that intersection under the inverse of the homeomorphism.
|
PartialHomeomorph.map_source''
theorem PartialHomeomorph.map_source'' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), ↑e '' e.source ⊆ e.target
This theorem, `PartialHomeomorph.map_source''`, is a variant of the `map_source` and states that for any given partial homeomorphism `e` from one topological space `X` to another topological space `Y`, the image of the source of `e` under `e` is a subset of the target of `e`. In other words, if we take any subset of `source` and map it using `e`, all the resulting elements will belong to `target`.
More concisely: For any partial homeomorphism `e` from topological space `X` to `Y`, `e` maps the source of `e` to a subset of the target of `e`: `source e ⊆ target e`.
|
PartialHomeomorph.left_inv
theorem PartialHomeomorph.left_inv :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → ↑e.symm (↑e x) = x
This theorem states that for any partial homeomorphism `e` from a type `X` to a type `Y`, both endowed with a topological space structure, if an element `x` of type `X` lies within the source of `e`, then applying the homeomorphism `e` to `x` and then the inverse of the homeomorphism (denoted by `PartialHomeomorph.symm e`) to the result, will give back the original element `x`. Essentially, it is a statement about the left-inverse property of the partial homeomorphism `e`.
More concisely: For any partial homeomorphism `e` between topological spaces `X` and `Y`, if `x ∈ X` lies in the domain of `e`, then `e (x) = e.symm (e x)`.
|
PartialHomeomorph.IsImage.iff_symm_preimage_eq
theorem PartialHomeomorph.IsImage.iff_symm_preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
This theorem states that for any given topological spaces `X` and `Y`, a partial homeomorphism `e` from `X` to `Y`, and two sets `s` of `X` and `t` of `Y`, the set `t` is an image of the set `s` under the partial homeomorphism `e` if and only if the intersection of the target of `e` and the preimage of the set `s` under the inverse of `e` equals the intersection of the target of `e` and the set `t`.
More concisely: For any topological spaces X and Y, a partial homeomorphism e from X to Y, and sets s in X and t in Y, s is the image of t under e if and only if e(s^-1) ∩ t = e(s^-1) ∩ e(s).
|
PartialHomeomorph.self_trans_symm
theorem PartialHomeomorph.self_trans_symm :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), e.trans e.symm ≈ PartialHomeomorph.ofSet e.source ⋯
The theorem `PartialHomeomorph.self_trans_symm` states that for any two topological spaces `X` and `Y`, and any partial homeomorphism `e` from `X` to `Y`, the composition of `e` and its inverse is equivalent to the restriction of the identity to the source set of `e`. In other words, if we apply `e` and then its inverse, we get the equivalent of applying the identity function restricted to the set where `e` is defined. This captures the intuition that a homeomorphism is a sort of "reversible continuous transformation" between topological spaces.
More concisely: For any partial homeomorphism `e` between topological spaces `X` and `Y`, `e ∘ e⁻¹` equals the restriction of the identity function on `X` to the domain of `e`.
|
PartialHomeomorph.IsImage.of_symm_preimage_eq'
theorem PartialHomeomorph.IsImage.of_symm_preimage_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y},
e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t → e.IsImage s t
This theorem, called `PartialHomeomorph.IsImage.of_symm_preimage_eq'`, states that for any two types `X` and `Y`, both equipped with a topological space structure, given a partial homeomorphism `e` from `X` to `Y`, and two sets `s` of `X` and `t` of `Y`, if the intersection of the target of the partial homeomorphism `e` and the preimage under the inverse of `e` of the intersection of the source of `e` and the set `s` equals the intersection of the target of `e` and the set `t`, then the partial homeomorphism `e` forms an image of the set `s` onto the set `t`. This is essentially a condition that relates the properties of the partial homeomorphism and the two sets under consideration.
More concisely: If for a partial homeomorphism between topological spaces and sets, the target's intersection with the preimage under the inverse equals the source's intersection with one set, then the partial homeomorphism maps the other set onto that set.
|
PartialHomeomorph.nhdsWithin_target_inter
theorem PartialHomeomorph.nhdsWithin_target_inter :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : Y}, x ∈ e.target → ∀ (s : Set Y), nhdsWithin x (e.target ∩ s) = nhdsWithin x s
This theorem states that for any given partial homeomorphism `e` between two topological spaces `X` and `Y`, and for any point `x` in the target of `e`, the neighborhood within `x` of the intersection between the target of `e` and any set `s` is equal to the neighborhood within `x` of `s`. In other words, when considering the topology near `x`, we can disregard the parts of `s` that lie outside the target of `e`. This is a property of continuity in topology and is specific to partial homeomorphisms, which are homeomorphisms between subsets of topological spaces.
More concisely: For any partial homeomorphism $e$ between topological spaces $X$ and $Y$ and any point $x$ in the target of $e$, the neighborhood filter of $x$ in the intersection of the target of $e$ and any set $s$ equals the neighborhood filter of $x$ in $s$.
|
PartialHomeomorph.IsImage.preimage_eq'
theorem PartialHomeomorph.IsImage.preimage_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y},
e.IsImage s t → e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s
This theorem states that for any types `X` and `Y` that are topological spaces, for any partial homeomorphism `e` from `X` to `Y`, and for any sets `s` of type `X` and `t` of type `Y`, if `e` is an image of `s` under the map to `t`, then the intersection of the source of `e` with the preimage under `e` of the intersection of the target of `e` and `t`, is equal to the intersection of the source of `e` and `s`. This is an alias of the forward direction of the theorem `PartialHomeomorph.IsImage.iff_preimage_eq'`.
More concisely: For any topological spaces X and Y, partial homeomorphism e between X and Y, and sets s ∈ X and t ∈ Y, if the image of s under the map to Y induced by e is equal to t, then the intersection of e's domain and the preimage of t under e is equal to the intersection of s and e's domain.
|
PartialHomeomorph.trans_assoc
theorem PartialHomeomorph.trans_assoc :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z']
(e : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) (e'' : PartialHomeomorph Z Z'),
(e.trans e').trans e'' = e.trans (e'.trans e'')
This theorem states that for any three topological spaces X, Y, and Z, and a fourth space Z', the composition of partial homeomorphisms is associative. Specifically, given a partial homeomorphism `e` from X to Y, a partial homeomorphism `e'` from Y to Z, and a partial homeomorphism `e''` from Z to Z', the composition of `e` and `e'` followed by `e''` is the same as the composition of `e` with the composition of `e'` and `e''`.
More concisely: For any partial homeomorphisms `e: X ↔ Y`, `e': Y ↔ Z`, and `e'': Z ↔ Z'`, the composition `(e' ∘ e) ∘ e'' = e ∘ (e' ∘ e'')` holds in the category of topological spaces.
|
PartialHomeomorph.IsImage.of_preimage_eq'
theorem PartialHomeomorph.IsImage.of_preimage_eq' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y},
e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s → e.IsImage s t
This theorem, which is an alias of the reverse direction of `PartialHomeomorph.IsImage.iff_preimage_eq'`, states that for any types `X` and `Y` equipped with topological structures, a partial homeomorphism `e` from `X` to `Y`, and sets `s` of `X` and `t` of `Y`, if the intersection of the source of `e` and the preimage under `e` of the intersection of the target of `e` and `t` equals the intersection of the source of `e` and `s`, then `e` is an image of `s` onto `t`. In simpler terms, it means that if a certain condition about the intersections and preimages is satisfied, then the partial homeomorphism maps `s` onto `t`.
More concisely: If a partial homeomorphism maps the source intersections of sets equitably, then it maps one set onto the other.
|
PartialHomeomorph.continuousAt_iff_continuousAt_comp_right
theorem PartialHomeomorph.continuousAt_iff_continuousAt_comp_right :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (e : PartialHomeomorph X Y) {f : Y → Z} {x : Y},
x ∈ e.target → (ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x))
The theorem `PartialHomeomorph.continuousAt_iff_continuousAt_comp_right` states that for any three types `X`, `Y` and `Z`, each equipped with a topological space structure, given a partial homeomorphism `e` from `X` to `Y`, a function `f` from `Y` to `Z`, and a point `x` in `Y`, if `x` is in the target of `e`, then the function `f` is continuous at point `x` if and only if the function `f` composed with the inverse of `e` is continuous at the point where `x` is mapped to under the inverse of `e`. In other words, under these conditions, continuity of `f` at `x` can be checked via the composition of `f` and the inverse of `e`.
More concisely: Given a partial homeomorphism `e: X ↫ Y` between topological spaces `X`, `Y`, a function `f: Y ↫ Z` to another topological space `Z`, and a point `x ∈ Y` in the domain of `e`, the function `f` is continuous at `x` if and only if `f ∘ e⁻¹` is continuous at `e(x)`.
|
PartialHomeomorph.eventually_right_inverse
theorem PartialHomeomorph.eventually_right_inverse :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : Y}, x ∈ e.target → ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y
This theorem states that for any type `X` and `Y` equipped with their respective topological spaces and for any partial homeomorphism `e` from `X` to `Y`, if a point `x` belongs to the target of `e`, then almost all points `y` in the neighborhood of `x` will satisfy the condition that applying `e` to the inverse of `e` applied to `y` gives back `y`. Essentially, it states that the inverse of the partial homeomorphism `e`, when composed with `e` itself, acts as an identity on a neighborhood of any point `x` in the target of `e`.
More concisely: Given a partial homeomorphism `e` from topological spaces `X` to `Y`, if `x` is in the image of `e` and `y` is in a neighborhood of `x`, then `e(Inv(e(y))) = y`, where `Inv` denotes the inverse.
|
PartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter
theorem PartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z},
ContinuousWithinAt f s x →
x ∈ e.source →
t ∈ nhds (f x) → (nhds (↑e x)).EventuallyEq (↑e.symm ⁻¹' s) (e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t))
This theorem, useful in the manifold library when `e` is a chart, asserts that for any topological spaces `X`, `Y`, and `Z`, a partial homeomorphism `e` from `X` to `Y`, sets `s` in `X` and `t` in `Z`, an element `x` of `X`, and a function `f` from `X` to `Z` that is continuous at `x` within `s`, if `x` is in the source of `e` and `t` is in the neighborhood of `f(x)`, then the neighborhood of `e(x)` is eventually equal to the preimage under `e.symm` of `s`, which is the same as the intersection of the target of `e` and the preimage under `e.symm` of the intersection of `s` and the preimage of `t` under `f`. In other words, around `e(x)`, the set `e.symm ⁻¹' s` locally looks like the intersection of the target of `e` and some other neighborhood of `f(x)`.
More concisely: Given a partial homeomorphism `e` from topological spaces `X` to `Y`, if `x` is in the domain of `e`, `t` is in the neighborhood of `f(x) = e(x)` for some continuous function `f` from `X` to `Z`, then the neighborhood of `e(x)` is equal to the preimage under `e.symm` of the intersection of the domain of `e` and the preimage of `t` under `f`.
|
PartialHomeomorph.EqOnSource.symm'
theorem PartialHomeomorph.EqOnSource.symm' :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e e' : PartialHomeomorph X Y}, e ≈ e' → e.symm ≈ e'.symm
The theorem `PartialHomeomorph.EqOnSource.symm'` states the following: for any two types `X` and `Y` equipped with topological space structures, and any two partial homeomorphisms `e` and `e'` between `X` and `Y`, if `e` is equivalent to `e'`, then the inverse of `e` is equivalent to the inverse of `e'`. In other words, the equivalence of two partial homeomorphisms implies the equivalence of their inverses.
More concisely: If partial homeomorphisms `e` and `e'` between topological spaces `X` and `Y` are equivalent, then their inverses are equivalent.
|
PartialHomeomorph.EqOnSource.trans'
theorem PartialHomeomorph.EqOnSource.trans' :
∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {e e' : PartialHomeomorph X Y} {f f' : PartialHomeomorph Y Z},
e ≈ e' → f ≈ f' → e.trans f ≈ e'.trans f'
This theorem states that for any three topological spaces X, Y, and Z, if two partial homeomorphisms between X and Y, say `e` and `e'`, are equivalent, and two partial homeomorphisms between Y and Z, say `f` and `f'`, are equivalent, then the composition of `e` and `f` (denoted as `e.trans f`) is equivalent to the composition of `e'` and `f'` (denoted as `e'.trans f'`). In other words, equivalence of partial homeomorphisms respects composition.
More concisely: If partial homeomorphisms `e : X ↔* Y` and `e' : X ↔* Y` are equivalent, and `f : Y ↔* Z` and `f' : Y ↔* Z` are equivalent, then `e.trans f` is equivalent to `e'.trans f'`.
|
PartialHomeomorph.IsImage.symm_iff
theorem PartialHomeomorph.IsImage.symm_iff :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.symm.IsImage t s ↔ e.IsImage s t
This theorem states that for any given partial homeomorphism `e` between two topological spaces `X` and `Y`, and any two sets `s` in `X` and `t` in `Y`, the set `t` is an image of the set `s` under the inverse of the homeomorphism `e` if and only if the set `s` is an image of the set `t` under the homeomorphism `e`. Intuitively, this theorem provides a condition for when we can reverse the direction of mapping by a homeomorphism when considering images of sets.
More concisely: For any partial homeomorphism between topological spaces, the inverse image and image of two sets are equal if and only if the sets are each other's images under that homeomorphism.
|
PartialHomeomorph.image_eq_target_inter_inv_preimage
theorem PartialHomeomorph.image_eq_target_inter_inv_preimage :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {s : Set X}, s ⊆ e.source → ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
This theorem states that for any two types `X` and `Y` equipped with topological spaces, and for a partial homeomorphism `e` from `X` to `Y`, if we have a set `s` which is a subset of the source of `e`, then the image of `s` under the partial homeomorphism `e` is equal to the intersection of the target of `e` and the preimage of `s` under the inverse of the partial homeomorphism `e`. This theorem essentially describes how a subset of a source set maps under a partial homeomorphism and its inverse.
More concisely: For any partial homeomorphism between topological spaces `e : X ↪ Y`, and subset `s ⊆ X`, the image of `s` under `e` is equal to the intersection of `e(`X`)` and the preimage of `s` under the inverse of `e`. In symbols: `e(s) = e(X) ∩ e⁻¹(s)`.
|
PartialHomeomorph.to_openEmbedding
theorem PartialHomeomorph.to_openEmbedding :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), e.source = Set.univ → OpenEmbedding ↑e
This theorem states that for any two types `X` and `Y` each equipped with a topological space structure, a partial homeomorphism `e` from `X` to `Y`, whose source covers the entire set `X`, defines an open embedding from `X` to `Y`. In other words, the partial homeomorphism `e` preserves the open sets structure under the condition that its source is the universal set of `X`. The converse of this statement is also true and can be seen from the theorem `OpenEmbedding.toPartialHomeomorph`.
More concisely: A partial homeomorphism from one topological space to another that maps the entire domain to open sets is an open embedding.
|
PartialHomeomorph.IsImage.iff_preimage_eq
theorem PartialHomeomorph.IsImage.iff_preimage_eq :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{e : PartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
This theorem states that for any given types `X` and `Y`, both equipped with a topology (i.e., they are topological spaces), a partial homeomorphism `e` from `X` to `Y`, and sets `s` of `X` and `t` of `Y`, the set `t` is an image of the set `s` under the partial homeomorphism `e` if and only if the intersection of the source of `e` with the preimage of `t` under `e` equals the intersection of the source of `e` with `s`. Essentially, this theorem establishes an equivalence between the definition of an image set under a partial homeomorphism and a particular condition involving set intersection and preimage.
More concisely: For topological spaces X and Y, a partial homeomorphism e from X to Y maps set s to set t if and only if e⁁⁻¹(t) ∩ source(e) = s ∩ source(e).
|
PartialHomeomorph.leftInvOn
theorem PartialHomeomorph.leftInvOn :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), Set.LeftInvOn (↑e.symm) (↑e) e.source
The theorem `PartialHomeomorph.leftInvOn` states that for any two given types `X` and `Y`, which have their respective topological space structures, and given a partial homeomorphism `e` from `X` to `Y`, the function `e` restricted to its source set has a left inverse given by the inverse of `e`. In other words, applying the inverse of `e` after `e` to any element in the source of `e` will get you back the original element.
More concisely: Given a partial homeomorphism `e` from topological spaces `X` and `Y`, the restriction of `e` on its source set has a left inverse equal to the inverse of `e`.
|
PartialHomeomorph.continuousAt
theorem PartialHomeomorph.continuousAt :
∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y) {x : X}, x ∈ e.source → ContinuousAt (↑e) x
This theorem states that a partial homeomorphism is continuous at any point in its source. More specifically, for all topological spaces `X` and `Y`, and for any partial homeomorphism `e` from `X` to `Y`, if a point `x` is in the source of `e`, then `e` is continuous at `x`. In mathematical terms, this means that when `x` tends to `x₀`, `e(x)` will tend to `e(x₀)`, where `x₀` is any point from the source of `e`.
More concisely: A partial homeomorphism from topological space X to Y is continuous at any point x in X if x is in the domain of the function.
|