IsLocalHomeomorph.isTopologicalBasis
theorem IsLocalHomeomorph.isTopologicalBasis :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f →
TopologicalSpace.IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}
This theorem states that for any two types `X` and `Y` with defined topological spaces and a function `f` from `X` to `Y`, if the function `f` satisfies the property `IsLocalHomeomorph`, then the set of all `U` such that there exists an open set `V` and a section `s` with `f` composed with `s` equal to the underlying element of the subtype and the range of `s` equals `U`, forms a topological basis of the source space `X`. In simpler terms, the theorem tells us that the ranges of continuous local sections of a local homeomorphism form a topological basis of the source space. A topological basis is a set of open sets in a topological space that can be used to generate all other open sets in the space.
More concisely: For any local homeomorphism between topological spaces `X` and `Y`, the ranges of continuous local sections form a topological basis of `X`.
|
IsLocalHomeomorphOn.mk
theorem IsLocalHomeomorphOn.mk :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) (s : Set X),
(∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source) → IsLocalHomeomorphOn f s
This theorem, `IsLocalHomeomorphOn.mk`, proves that a function `f` satisfies the property `IsLocalHomeomorphOn f s`, given a certain condition. Here, `X` and `Y` are types equipped with topological spaces, `f` is a function from `X` to `Y`, and `s` is a set of elements of `X`. The condition needed to prove the theorem, denoted as `h`, is that for every element `x` in the set `s`, there exists a partial homeomorphism `e` from `X` to `Y` such that `x` is in the source of `e` and `f` agrees with `e` on `e`'s source. This condition `h` is weaker than the definition of `IsLocalHomeomorphOn f s` because it only requires `f` to agree with `e` on `e`'s source and not on the whole space `X`.
More concisely: Given types `X` and `Y` with topological spaces, a function `f: X → Y`, and a set `s ⊆ X`, if for each `x ∈ s`, there exists a partial homeomorphism `e` from `X` to `Y` with `x` in the source of `e` such that `f` agrees with `e` on `e`'s source, then `f` is a local homeomorphism on `s`.
|
IsLocalHomeomorph.mk
theorem IsLocalHomeomorph.mk :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
(∀ (x : X), ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source) → IsLocalHomeomorph f
The theorem `IsLocalHomeomorph.mk` establishes the condition under which a function `f` from a topological space `X` to another topological space `Y` satisfies the property `IsLocalHomeomorph f`. Specifically, for any point `x` in `X`, if there exists a partial homeomorphism `e` such that `x` is in the source of `e` and `f` and `e` agree on all points in the source of `e`, then `f` is a local homeomorphism. This condition is weaker than the definition of `IsLocalHomeomorph f`, as it does not require `f` and `e` to agree on all points in `X`, but only those in the source of `e`.
More concisely: If for each point `x` in a topological space `X` and for some partial homeomorphism `e` with `x` in the source, `f` agrees with `e` on the source points, then `f` is a local homeomorphism.
|
IsLocalHomeomorph.Homeomorph.isLocalHomeomorph
theorem IsLocalHomeomorph.Homeomorph.isLocalHomeomorph :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
IsLocalHomeomorph ⇑h
This theorem states that a homeomorphism is also a local homeomorphism. More explicitly, for any two types `X` and `Y` that are endowed with topological spaces, if there exists a homeomorphism `h` from `X` to `Y`, then the function `h` satisfies the property of being a local homeomorphism. In mathematical terms, that means that for each point `x` in `X`, there exists a partial homeomorphism `e` such that `x` is in the source of `e` and the function `h` equals the embedding of `e`.
More concisely: If `X` and `Y` are topological spaces and `h` is a homeomorphism from `X` to `Y`, then `h` is a local homeomorphism.
|
IsLocalHomeomorph.openEmbedding_of_comp
theorem IsLocalHomeomorph.openEmbedding_of_comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y},
IsLocalHomeomorph g → OpenEmbedding (g ∘ f) → Continuous f → OpenEmbedding f
The theorem `IsLocalHomeomorph.openEmbedding_of_comp` states that if `g` is a local homeomorphism (a function from type `Y` to `Z` such that for every point in `Y`, there exists a partial homeomorphism that matches `g` at that point), and the composition of `g` and another function `f` (from type `X` to `Y`) is an open embedding (a function that is both a homeomorphism onto its image and an embedding), and `f` is continuous, then `f` itself is also an open embedding. This theorem is applicable in the context where `X`, `Y`, and `Z` are topological spaces.
More concisely: If `g` is a local homeomorphism and the composition of continuous `f` and `g` is an open embedding, then `f` is an open embedding.
|
IsLocalHomeomorph.comp
theorem IsLocalHomeomorph.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y},
IsLocalHomeomorph g → IsLocalHomeomorph f → IsLocalHomeomorph (g ∘ f)
The theorem `IsLocalHomeomorph.comp` states that if we have two functions `f : X → Y` and `g : Y → Z`, where `X`, `Y` and `Z` are topological spaces, and `f` and `g` are both local homeomorphisms, then the composition of `g` and `f`, denoted by `g ∘ f`, is also a local homeomorphism. A function is a local homeomorphism if for every point in its domain, there exists a partial homeomorphism that has the point in its source and the function equals to the embedding of that partial homeomorphism.
More concisely: The composition of two local homeomorphisms between topological spaces is a local homeomorphism.
|
IsLocalHomeomorph.continuous
theorem IsLocalHomeomorph.continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f → Continuous f
The theorem states that a local homeomorphism is continuous. More specifically, for any types `X` and `Y`, and any topological spaces over `X` and `Y`, if a function `f` from `X` to `Y` is a local homeomorphism (i.e., for each point in `X`, there exists a partial homeomorphism `e` such that the point is in the source of `e` and `f` equals the function represented by `e`), then `f` is continuous.
More concisely: If a local homeomorphism between topological spaces is given, then it is continuous.
|
IsLocalHomeomorph.isOpenMap
theorem IsLocalHomeomorph.isOpenMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f → IsOpenMap f
The theorem `IsLocalHomeomorph.isOpenMap` states that for any two types `X` and `Y` with topological space structures, any function `f` from `X` to `Y` that is a local homeomorphism is also an open map. In other words, if for every point `x` in `X`, there is a partial homeomorphism `e` such that `x` is in the source of `e` and `f` is equivalent to `e`, then the image of any open set in `X` under `f` is an open set in `Y`.
More concisely: A local homeomorphism between topological spaces is an open map.
|
IsLocalHomeomorphOn.PartialHomeomorph.isLocalHomeomorphOn
theorem IsLocalHomeomorphOn.PartialHomeomorph.isLocalHomeomorphOn :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(e : PartialHomeomorph X Y), IsLocalHomeomorphOn (↑e) e.source
The theorem `IsLocalHomeomorphOn.PartialHomeomorph.isLocalHomeomorphOn` states that, for any given partial homeomorphism `e` from a type `X` to a type `Y`, both endowed with a topological structure, the function underlying `e` is a local homeomorphism on the source of `e`. In other words, for every point in the source of `e`, there's a partial homeomorphism whose source contains that point and whose associated function is the function underlying `e`.
More concisely: Given a partial homeomorphism `e` from a topological space `X` to a topological space `Y`, the underlying function is a local homeomorphism on `X`.
|
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ
theorem isLocalHomeomorph_iff_isLocalHomeomorphOn_univ :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ
This theorem states that for any function `f` from a type `X` to a type `Y`, where `X` and `Y` are equipped with some topological spaces, the function `f` is a local homeomorphism if and only if it is a local homeomorphism on the universal set in `X`. In other words, `f` is a local homeomorphism (meaning, every point in `X` is contained in the source of some partial homeomorphism that equals `f`) if and only if this condition holds when we restrict our attention to the universal set in `X` (which contains all elements of `X`).
More concisely: A function `f : X → Y` between topological spaces `X` and `Y` is a local homeomorphism if and only if it is a local homeomorphism on the universal set of `X`.
|
IsLocalHomeomorph.openEmbedding_of_injective
theorem IsLocalHomeomorph.openEmbedding_of_injective :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f → Function.Injective f → OpenEmbedding f
The theorem `IsLocalHomeomorph.openEmbedding_of_injective` states that for any types `X` and `Y`, which are topological spaces, and for any function `f` from `X` to `Y`, if `f` satisfies the property of being a local homeomorphism (i.e., for each point in `X`, there exists a partial homeomorphism enveloping the point such that it is equivalent to `f` in a neighborhood of the point) and `f` is injective (i.e., equal outputs imply equal inputs), then `f` is an open embedding. An open embedding is a function that is injective, continuous, and turns open sets in the original space into open sets in the target space.
More concisely: If `f : X → Y` is a local homeomorphism and an injective function between topological spaces `X` and `Y`, then `f` is an open embedding.
|
IsLocalHomeomorph.isLocallyInjective
theorem IsLocalHomeomorph.isLocallyInjective :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsLocalHomeomorph f → IsLocallyInjective f
The theorem `IsLocalHomeomorph.isLocallyInjective` asserts that for any function `f` from a topological space `X` to another topological space `Y`, if `f` satisfies the property `IsLocalHomeomorph`, i.e., each point in `X` is in the source of some partial homeomorphism with `f` equal to the inclusion of this partial homeomorphism, then `f` also satisfies the property `IsLocallyInjective`, i.e., around every point of `X`, there exists a neighborhood on which `f` is injective.
More concisely: If a function between topological spaces is a local homeomorphism, then it is locally injective.
|
IsLocalHomeomorph.isLocalHomeomorphOn
theorem IsLocalHomeomorph.isLocalHomeomorphOn :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
IsLocalHomeomorph f → IsLocalHomeomorphOn f s
This theorem states that for all topological spaces `X` and `Y`, all functions `f` from `X` to `Y`, and all sets `s` of `X`, if `f` satisfies the property `IsLocalHomeomorph`, then `f` also satisfies the property `IsLocalHomeomorphOn` for the set `s`. In other words, if every point in `X` is mapped by `f` in a way that is locally a homeomorphism, then every point in the particular set `s` of `X` is also mapped by `f` in a way that is locally a homeomorphism.
More concisely: If `f` is a local homeomorphism from a topological space `X` to `Y`, then `f` is locally a homeomorphism on every subset `s` of `X`.
|