Inducing.continuous
theorem Inducing.continuous :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → Continuous f
This theorem states that for any two types `X` and `Y`, and any function `f` from `X` to `Y`, if `f` induces the topology of `Y` on `X` (i.e., the topology on `X` is the coarsest one that makes `f` continuous), then `f` is a continuous function. This holds under the condition that `X` and `Y` are both equipped with a topological space structure. This is a foundational result in topology, linking the concepts of induced topology and continuous functions.
More concisely: If a function between topological spaces is the identification of the topology on the domain, then it is continuous.
|
Inducing.isOpenMap
theorem Inducing.isOpenMap :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → IsOpen (Set.range f) → IsOpenMap f
The theorem `Inducing.isOpenMap` states that for any two types `X` and `Y` (which can be considered as spaces), if `f` is a function from `X` to `Y`, and both `X` and `Y` have topological space structures, then if `f` is an inducing function (i.e., the topology on `X` is the one induced by `f` from `Y`), and the range of `f` (the set of all possible output values of `f`) is an open set in `Y`, then `f` is an open map. In other words, for any open set in `X`, its image under `f` is an open set in `Y`.
More concisely: If `f` is an inducing function from a topological space `(X, τX)` to another topological space `(Y, τY)` with open range, then `f` is an open map, that is, for every open set `U` in `X`, `f(U)` is an open set in `Y`.
|
IsOpenMap.to_quotientMap
theorem IsOpenMap.to_quotientMap :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → Continuous f → Function.Surjective f → QuotientMap f
This theorem states that for any two types `X` and `Y` with a function `f` mapping from `X` to `Y`, if both `X` and `Y` possess a topological structure and `f` is an open map, continuous, and surjective, then `f` is a quotient map. In mathematical terms, this theorem asserts that a continuous function that is both surjective and takes open sets to open sets (an open map) is a quotient map, where a quotient map is a surjective function that preserves the open sets of the domain in the codomain.
More concisely: A continuous, surjective open map between topological spaces is a quotient map.
|
OpenEmbedding.comp
theorem OpenEmbedding.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
OpenEmbedding g → OpenEmbedding f → OpenEmbedding (g ∘ f)
This theorem states that for all types X, Y, and Z, and for all functions f from X to Y and g from Y to Z, if they are equipped with topological spaces, then if g is an open embedding and f is also an open embedding, the composition of g and f (i.e., g ∘ f) is also an open embedding. In the context of topology, an open embedding is a function between two topological spaces that is an embedding (i.e., injective and homeomorphic to its image) and its image is an open subset.
More concisely: If two open embeddings between topological spaces compose them, the result is an open embedding.
|
IsClosedMap.closure_image_subset
theorem IsClosedMap.closure_image_subset :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsClosedMap f → ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s
The theorem `IsClosedMap.closure_image_subset` states that for any two types `X` and `Y`, if `f` is a closed map from `X` to `Y` and `s` is a set of elements of type `X`, then the closure of the image of set `s` under the function `f` is a subset of the image of the closure of `s` under function `f`. In other words, taking the closure after the function `f` is applied is contained within applying the function `f` after taking the closure.
More concisely: For any closed map `f` between topological spaces `X` and `Y`, and any set `s` in `X`, the closure of `f(s)` is contained in `f(Closure(s))`.
|
IsOpenMap.image_interior_subset
theorem IsOpenMap.image_interior_subset :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
This theorem states that for any two types `X` and `Y`, and any function `f` from `X` to `Y`, given that both `X` and `Y` are topological spaces and `f` is an open map, for any set `s` of type `X`, the image under `f` of the interior of `s` is a subset of the interior of the image of `s` under `f`. In simpler terms, applying `f` to the interior of a set doesn't produce values outside of the interior of the set's image under `f`.
More concisely: Given topological spaces X and Y and an open map f from X to Y, the image under f of the interior of any set in X is a subset of the interior of the image of that set under f.
|
embedding_id
theorem embedding_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Embedding id
This theorem states that for every type `X` that is equipped with a topology (a `TopologicalSpace`), the identity function on `X` is an embedding. In the context of topology, an embedding refers to a function which is one-to-one, continuous, and its inverse function is also continuous when restricted to the image of the original function. So, this theorem is essentially saying that the identity function satisfies these properties in any topological space.
More concisely: The identity function on any topological space is a continuous, injective (one-to-one) homeomorphism.
|
Embedding.discreteTopology
theorem Embedding.discreteTopology :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : DiscreteTopology Y], Embedding f → DiscreteTopology X
This theorem states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, if `Y` is a discrete topological space, and if `f` is an embedding (i.e., a function that is injective and has its image being a topologically identical subset of `Y`), then `X` must also be a discrete topological space. This is also related to `DiscreteTopology.of_continuous_injective`, another theorem in the context of discrete topologies.
More concisely: If `X` is a type, `Y` is a discrete topological space, and `f : X → Y` is an injective function whose image is a topologically identical subset of `Y`, then `X` is a discrete topological space.
|
IsOpenMap.comp
theorem IsOpenMap.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], IsOpenMap g → IsOpenMap f → IsOpenMap (g ∘ f)
The theorem `IsOpenMap.comp` states that for any three types `X`, `Y` and `Z` with respective topological spaces, if `f` is a function from `X` to `Y` and `g` is a function from `Y` to `Z`, then the composition of `g` and `f` is also an open map if `f` and `g` are both open maps. In mathematical terms, if the image of any open set `U` under `f` or `g` is open, then the image of `U` under the composition of `f` and `g` (i.e., `g ∘ f`) is also open.
More concisely: If `f: X ⟹ Y` and `g: Y ⟹ Z` are open maps, then their composition `g ∘ f: X ⟹ Z` is also an open map.
|
IsClosedMap.comp
theorem IsClosedMap.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
IsClosedMap g → IsClosedMap f → IsClosedMap (g ∘ f)
The theorem `IsClosedMap.comp` states that for any three types `X`, `Y`, and `Z` with associated topological spaces, if `f` is a closed map from `X` to `Y` and `g` is a closed map from `Y` to `Z`, then the composition of `g` and `f` (denoted by `g ∘ f`) is also a closed map from `X` to `Z`. In other words, the property of being a closed map is preserved under function composition in topological spaces.
More concisely: If `f` is a closed map from `X` to `Y` and `g` is a closed map from `Y` to `Z`, then the composition `g ∘ f` is a closed map from `X` to `Z` in topological spaces.
|
OpenEmbedding.map_nhds_eq
theorem OpenEmbedding.map_nhds_eq :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
OpenEmbedding f → ∀ (x : X), Filter.map f (nhds x) = nhds (f x)
This theorem states that for any two types `X` and `Y`, along with a function `f` from `X` to `Y`, if `X` and `Y` are equipped with topological space structures and `f` is an open embedding, then for any element `x` of `X`, the forward map of the neighborhood filter at `x` under `f` is equal to the neighborhood filter at `f(x)` in `Y`. In other words, applying `f` to each set in the neighborhood filter of `x` results in the neighborhood filter of `f(x)`. This is an important property that relates the concept of continuity in topology with the operation of filters.
More concisely: Given types `X` and `Y`, a function `f : X ↝ Y` between topological spaces, and an open embedding `f`, for all `x : X`, the forward image of the neighborhood filter of `x` under `f` equals the neighborhood filter of `f(x)` in `Y`.
|
QuotientMap.continuous
theorem QuotientMap.continuous :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
QuotientMap f → Continuous f
This theorem states that for any two types `X` and `Y` with respective topological spaces, and any function `f` from `X` to `Y`, if `f` is a quotient map, then `f` is continuous. In the context of topology, a function is continuous if the preimage of every open set is open, and a function is a quotient map if it is surjective and the topology on the codomain is the coinduced topology from the domain through the function.
More concisely: A surjective quotient map between topological spaces is a continuous function.
|
ClosedEmbedding.isClosedMap
theorem ClosedEmbedding.isClosedMap :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
ClosedEmbedding f → IsClosedMap f
The theorem states that for any types `X` and `Y`, and any function `f` from `X` to `Y`, given that `X` and `Y` have a topological space structure, if `f` is a closed embedding (meaning it's an embedding and its image is a closed set in `Y`), then `f` is a closed map. In other words, if a function `f` is such that it embeds `X` into `Y` and the image of `f` is closed in `Y`, it will also have the property that the image of any closed set in `X` under `f` is a closed set in `Y`.
More concisely: If `f` is a closed embedding of topological spaces `X` into `Y`, then `f` is a closed map.
|
OpenEmbedding.continuousAt_iff
theorem OpenEmbedding.continuousAt_iff :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
OpenEmbedding f → ∀ {x : X}, ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
This theorem states that for all topological spaces `X`, `Y`, and `Z`, and for all functions `f : X → Y` and `g : Y → Z`, if `f` is an open embedding, then the composition of `g` and `f` is continuous at a point `x` in `X` if and only if `g` is continuous at the point `f(x)` in `Y`. An open embedding is a function that is both injective and open, meaning that it bijectively maps open sets to open sets. Continuity of a function at a point refers to the property that the value of the function at that point is close to the values of the function at nearby points.
More concisely: For all topological spaces X, Y, Z, functions f : X → Y and g : Y → Z, if f is an open embedding then g ∘ f is continuous at x ∈ X if and only if g is continuous at f(x) ∈ Y.
|
IsOpenMap.preimage_closure_eq_closure_preimage
theorem IsOpenMap.preimage_closure_eq_closure_preimage :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' closure s = closure (f ⁻¹' s)
This theorem states that, for any types `X` and `Y` and any function `f` from `X` to `Y`, given that `X` and `Y` are topological spaces, if `f` is an open map and continuous, then for any set `s` of type `Y`, the preimage of the closure of `s` under `f` is equal to the closure of the preimage of `s` under `f`. In mathematical terms, if $f : X \rightarrow Y$ is an open and continuous function between two topological spaces, then for any subset $s$ of $Y$, we have $f^{-1}(cl(s)) = cl(f^{-1}(s))$, where $cl(s)$ denotes the closure of the set $s$.
More concisely: For any open and continuous function $f$ between topological spaces $X$ and $Y$, the preimages of closed sets under $f$ are equal: $f^{-1}(cl(s)) = cl(f^{-1}(s))$.
|
IsOpenMap.preimage_frontier_eq_frontier_preimage
theorem IsOpenMap.preimage_frontier_eq_frontier_preimage :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' frontier s = frontier (f ⁻¹' s)
This theorem states that for any types `X` and `Y`, and any function `f` from `X` to `Y`, if `f` is an open map and is continuous, then for any set `s` of type `Y`, the preimage of the frontier of `s` under `f` is equal to the frontier of the preimage of `s` under `f`. In simpler terms, if a function sends open sets to open sets and is continuous, then the "boundary" of the preimage of a set is the same as the preimage of the "boundary" of the set. Here, "boundary" refers to the frontier of a set, which is the set of points between the closure and interior of the set.
More concisely: If `f : X → Y` is a continuous and open function between topological spaces `X` and `Y`, then for any set `s ⊆ Y`, the frontier of `f⁻¹(s)` equals `f⁻¹(frontier(s))`.
|
Inducing.nhds_eq_comap
theorem Inducing.nhds_eq_comap :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → ∀ (x : X), nhds x = Filter.comap f (nhds (f x))
The theorem `Inducing.nhds_eq_comap` states that for any types `X` and `Y` with their corresponding topological spaces, and any function `f` from `X` to `Y` that induces the topology of `Y` from `X`, the neighborhood filter of any point `x` in `X` is equal to the pullback (also known as the inverse image under `f` or the `comap`) of the neighborhood filter of `f(x)` in `Y`. In simpler terms, the theorem is basically saying that the neighborhoods of point `x` in `X` correspond exactly to the pre-images under `f` of the neighborhoods of `f(x)` in `Y`, whenever `f` is a topology-inducing function.
More concisely: For any topological spaces (X,τ\_X) and (Y,τ\_Y), and a topology-inducing function f : X -> Y, the neighborhood filter of x in X is equal to the pullback of the neighborhood filter of f(x) in Y.
|
Inducing.closure_eq_preimage_closure_image
theorem Inducing.closure_eq_preimage_closure_image :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → ∀ (s : Set X), closure s = f ⁻¹' closure (f '' s)
This theorem states that for any two types `X` and `Y`, and any function `f` from `X` to `Y`, given that the topological structures of `X` and `Y` exist and the function `f` is inducing, for any set `s` of `X`, the closure of `s` is equal to the preimage under `f` of the closure of the image of `s` under `f`. In simpler terms, it says that the closure of a set in the domain of an inducing function is the same as the preimage of the closure of the image of that set under the function. This is a property of inducing functions in topology which helps in studying the topological structure of sets and spaces.
More concisely: For any inducing function between topological spaces `f` from `X` to `Y`, the closure of `f`'s image of a set `s` in `X` equals the preimage of the closure of that image in `Y`.
|
Inducing.tendsto_nhds_iff
theorem Inducing.tendsto_nhds_iff :
∀ {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z]
{f : ι → Y} {l : Filter ι} {y : Y},
Inducing g → (Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)))
The theorem `Inducing.tendsto_nhds_iff` states that for any types `Y`, `Z`, `ι`, a function `g` from `Y` to `Z`, a topological space over `Y` and `Z`, a function `f` from `ι` to `Y`, a filter `l` over `ι`, and an element `y` of `Y`, if `g` is an inducing function (i.e., the topology on `Y` is the initial topology with respect to `g`), then the function `f` tends to the neighborhood filter of `y` (in the sense of the Filter.Tendsto predicate) if and only if the composition of `g` and `f` tends to the neighborhood filter of `g(y)`. In simpler terms, the function `f` approaches `y` as its inputs approach the elements of the filter `l` if and only if `g(f)` approaches `g(y)` in the same manner.
More concisely: For a function `g` inducing the topology on `Y` from `Z`, `f` tends to the neighborhood filter of `y` in `Y` if and only if `g ∘ f` tends to the neighborhood filter of `g(y)` in `Z`.
|
IsOpenMap.preimage_interior_eq_interior_preimage
theorem IsOpenMap.preimage_interior_eq_interior_preimage :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' interior s = interior (f ⁻¹' s)
This theorem states that for any function `f` mapping elements from a topological space `X` to another topological space `Y`, if `f` is an open map and is continuous, then for any set `s` in `Y`, the preimage of the interior of `s` under `f` is equal to the interior of the preimage of `s` under `f`. In mathematical terms, it says that for all open maps `f : X → Y` that are continuous, the preimage of the interior of a set is the same as the interior of the preimage of the set, i.e., `f⁻¹(interior(s)) = interior(f⁻¹(s))`.
More concisely: If `f : X → Y` is a continuous open map between topological spaces, then for any open set `s` in `Y`, the preimage `f⁻¹(s)` is the interior of its preimage, i.e., `interior(f⁻¹(s)) = f⁻¹(interior(s))`.
|
inducing_id
theorem inducing_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Inducing id
This theorem states that for any type `X` with a given topology (represented by `TopologicalSpace X`), the identity mapping (represented by `id`) is an inducing map. In terms of mathematics, it is saying that the identity function is always a topological embedding, thus it induces the same topology on the underlying set `X`.
More concisely: The identity function is a topological embedding for any topological space `X`.
|
embedding_of_embedding_compose
theorem embedding_of_embedding_compose :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
Continuous f → Continuous g → Embedding (g ∘ f) → Embedding f
This theorem states that for all types `X`, `Y`, and `Z`, given functions `f: X → Y` and `g: Y → Z` and considering `X`, `Y` and `Z` are topological spaces, if both `f` and `g` are continuous and the composition of `g` and `f` (i.e., `g ∘ f`) is an embedding, then `f` is also an embedding. In topology, an embedding is a function that is both injective (i.e., maps distinct points in the domain to distinct points in the codomain) and continuous, with its image being a topologically meaningful copy of its domain.
More concisely: If `f: X → Y` and `g: Y → Z` are continuous functions between topological spaces `X`, `Y`, and `Z` with `g ∘ f` being an embedding, then `f` is an embedding.
|
inducing_of_inducing_compose
theorem inducing_of_inducing_compose :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
Continuous f → Continuous g → Inducing (g ∘ f) → Inducing f
This theorem states that for any three types `X`, `Y`, and `Z`, and for any two functions `f`: from `X` to `Y` and `g`: from `Y` to `Z`, given that `X`, `Y`, and `Z` each have a topology, if both `f` and `g` are continuous and the composition `g ∘ f` is an inducing function, then `f` is also an inducing function. In mathematical terms, if `g` and `f` are continuous maps between topological spaces such that the composition `g ∘ f` induces the topology of `Z` onto `X`, then `f` alone induces the topology of `Y` onto `X`.
More concisely: If `X`, `Y`, and `Z` are topological spaces, `f: X → Y` and `g: Y → Z` are continuous functions with `g ∘ f` being an inducing function from `X` to `Z`, then `f` is an inducing function from `X` to `Y`.
|
quotientMap_iff
theorem quotientMap_iff :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
QuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsOpen s ↔ IsOpen (f ⁻¹' s)
This theorem states that for all topological spaces `X` and `Y` and a function `f` from `X` to `Y`, `f` is a quotient map if and only if `f` is surjective and for every subset `s` of `Y`, `s` is an open set in `Y` if and only if the preimage of `s` under `f` is an open set in `X`. In other words, a function between topological spaces is a quotient map precisely when it is surjective and the preimage of any open set remains an open set.
Here, surjectivity means that for every element in `Y`, there exists an element in `X` such that the function `f` maps this element in `X` to that element in `Y`. A set `s` is said to be open if it is an open set in the given topological space. The preimage of a set under a function is the set of all elements that the function maps to any element of the original set.
More concisely: A function between topological spaces is a quotient map if and only if it is surjective and preserves open sets.
|
isOpenMap_iff_nhds_le
theorem isOpenMap_iff_nhds_le :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f ↔ ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
The theorem `isOpenMap_iff_nhds_le` establishes an equivalence between two conditions for a map `f` from a topological space `X` to another topological space `Y`. The first condition is that `f` is an open map, which means that the image of any open set in `X` under `f` is open in `Y`. The second condition is a property of the neighborhood filters at each point `x` in `X`: for all `x` in `X`, the neighborhood filter at `f(x)` in `Y` is smaller than or equal to the filter obtained by applying `f` to the neighborhood filter at `x` in `X`. The "smaller than or equal to" relation here is in the sense of filter inclusion, meaning that every set in the neighborhood filter at `f(x)` is also in the image of the neighborhood filter at `x` under `f`.
More concisely: A continuous function \(f : X \to Y\) between topological spaces is open if and only if for all \(x \in X\), the neighborhood filter of \(f(x)\) in \(Y\) is contained in the filter generated by \(f(\text{N}_{\delta}(x))\), where \(\text{N}_{\delta}(x)\) denotes the open neighborhood of \(x\) in \(X\) with respect to the given topology.
|
Inducing.mapClusterPt_iff
theorem Inducing.mapClusterPt_iff :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → ∀ {x : X} {l : Filter X}, MapClusterPt (f x) l f ↔ ClusterPt x l
The theorem `Inducing.mapClusterPt_iff` states that for any two topological spaces `X` and `Y`, and a function `f` from `X` to `Y` that induces the topology on `Y` from `X`, a point `x` in `X` is a cluster point of a filter `l` if and only if the image of `x` under `f` is a cluster point of the filter `l` mapped through `f`. This theorem provides a way to check if a point is a cluster point using its image under an inducing function.
More concisely: For any function `f` inducing the topology on `Y` from `X`, a point `x` in `X` is a cluster point of a filter `l` if and only if the image of `x` under `f` is a cluster point of the filtered set `f""l` in `Y`.
|
Embedding.closure_eq_preimage_closure_image
theorem Embedding.closure_eq_preimage_closure_image :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Embedding f → ∀ (s : Set X), closure s = f ⁻¹' closure (f '' s)
The theorem `Embedding.closure_eq_preimage_closure_image` states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, given that `f` is an Embedding and both `X` and `Y` are topological spaces, for any set `s` of type `X`, the closure of `s` is equal to the preimage under `f` of the closure of the image of `s` under `f`. In less formal terms, this means that the closure of a set in the original space and the closure of its image in the target space are closely related: the closure of the original set is exactly the set of points that get mapped to the closure of the image.
More concisely: Given an Embedding `f` between topological spaces `X` and `Y`, the closure of `f`(S) is equal to `f`(Closure S), where S is a subset of X.
|
IsOpenMap.image_mem_nhds
theorem IsOpenMap.image_mem_nhds :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → ∀ {x : X} {s : Set X}, s ∈ nhds x → f '' s ∈ nhds (f x)
This theorem states that for any types `X` and `Y`, and a function `f` mapping `X` to `Y`, given that `X` and `Y` are topological spaces and `f` is an open map, for any point `x` in `X` and any set `s` that is a neighborhood of `x`, the image of `s` under `f` is a neighborhood of the image of `x` under `f`. In simpler terms, if `s` is close to `x`, then `f(s)` is close to `f(x)`, assuming `f` is an open mapping between the topological spaces.
More concisely: Given topological spaces X and Y and an open map f from X to Y, for all x in X and every neighborhood s of x, the image f(s) is a neighborhood of f(x).
|
Embedding.tendsto_nhds_iff
theorem Embedding.tendsto_nhds_iff :
∀ {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z]
{f : ι → Y} {l : Filter ι} {y : Y},
Embedding g → (Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)))
The theorem `Embedding.tendsto_nhds_iff` states that, given two types `Y` and `Z` along with an indexing type `ι`, a function `g` from `Y` to `Z`, both `Y` and `Z` having topological space structures, a function `f` from `ι` to `Y`, a filter `l` on `ι`, and an element `y` of `Y`, if `g` is an embedding, then the function `f` tends towards the neighborhood of `y` under the filter `l` if and only if the composition of `g` and `f` (denoted `g ∘ f`) tends towards the neighborhood of `g(y)` under the filter `l`. In simpler terms, it shows the preservation of limit properties under an embedding.
More concisely: Given an embedding `g` between topological spaces `Y` and `Z`, if a filter `l` on the indexing type `ι` causes `f` from `ι` to `Y` to tend towards the neighborhood of `y` in `Y`, then it causes `g ∘ f` to tend towards the neighborhood of `g(y)` in `Z`.
|
Inducing.map_nhds_eq
theorem Inducing.map_nhds_eq :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → ∀ (x : X), Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
The theorem `Inducing.map_nhds_eq` states that for any types `X` and `Y`, a function `f: X → Y`, and any point `x` in `X`, under the conditions that `f` induces the topological structure on `Y` from `X`, the forward map of the neighborhood filter at `x` under `f` is equal to the neighborhood within filter at `f(x)` in the range of `f`. Essentially, it confirms that the induced topology correctly transforms local properties of `X` under `f` to `Y`.
More concisely: For any functions `f: X -> Y` inducing the topology on `Y` from `X`, the neighborhood filter at `x` in `X` is equal to the neighborhood filter at `f(x)` in `Y`.
|
Inducing.continuous_iff
theorem Inducing.continuous_iff :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], Inducing g → (Continuous f ↔ Continuous (g ∘ f))
The theorem `Inducing.continuous_iff` states that for any three types `X`, `Y`, and `Z`, given functions `f` from `X` to `Y` and `g` from `Y` to `Z`, with each of them having a topological space structure, if `g` is inducing, then `f` is continuous if and only if the composition of `g` and `f` (`g ∘ f`) is continuous. This theorem essentially establishes a condition under which the continuity of a function `f` can be deduced from the continuity of the composition `g ∘ f`.
More concisely: Given functions `f : X → Y` and `g : Y → Z` between topological spaces with `g` inducing and continuous, then `f` is continuous if and only if their composition `g ∘ f` is continuous.
|
ClosedEmbedding.continuous
theorem ClosedEmbedding.continuous :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
ClosedEmbedding f → Continuous f
This theorem states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, given that `X` and `Y` are topological spaces, if `f` is a closed embedding, then `f` is also continuous. In other words, a closed embedding between topological spaces always preserves continuity.
More concisely: If `f : X → Y` is a closed embedding between topological spaces `X` and `Y`, then `f` is continuous.
|
IsClosedMap.closed_range
theorem IsClosedMap.closed_range :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsClosedMap f → IsClosed (Set.range f)
The theorem `IsClosedMap.closed_range` states that for any function `f` mapping from type `X` to type `Y`, where `X` and `Y` are equipped with a topological space structure, if `f` is a closed map (meaning the image of any closed set in `X` under `f` is also a closed set in `Y`), then the range of `f` (which is the set of all the outputs `f` can produce) is a closed set in `Y`. In other words, if `f` preserves the property of being closed under mapping, then the entire set of possible outputs of `f` is also a closed set.
More concisely: If `f` is a closed map from a topological space `(X, τX)` to another topological space `(Y, τY)`, then the range of `f` is a closed set in `(Y, τY)`.
|
IsOpenMap.nhds_le
theorem IsOpenMap.nhds_le :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
The theorem `IsOpenMap.nhds_le` states that for any types `X` and `Y`, and any function `f` from `X` to `Y`, if `f` is an open map (i.e., the image of any open set in `X` under `f` is an open set in `Y`), then for any element `x` in `X`, the neighborhood filter of `f(x)` in `Y` is less than or equal to the filter obtained by mapping the neighborhood filter of `x` in `X` through the function `f`. This means that every neighborhood of `f(x)` contains the image under `f` of some neighborhood of `x`.
More concisely: For any open map f from X to Y and any x in X, the neighborhood filter of f(x) in Y is contained in the filter obtained by mapping neighborhoods of x in X through f.
|
openEmbedding_of_continuous_injective_open
theorem openEmbedding_of_continuous_injective_open :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Continuous f → Function.Injective f → IsOpenMap f → OpenEmbedding f
The theorem `openEmbedding_of_continuous_injective_open` states that for any two types `X` and `Y`, given a function `f` from `X` to `Y`, and instances of `TopologicalSpace` for `X` and `Y`, if the function `f` is continuous, injective, and is an open map (i.e., it maps open sets in `X` to open sets in `Y`), then `f` is an open embedding. An open embedding is a continuous, injective function that also maps open sets to open sets. Therefore, this theorem provides a sufficient condition for a function to be an open embedding in the context of topology.
More concisely: If a continuous, injective function between topological spaces maps open sets to open sets, then it is an open embedding.
|
Embedding.toOpenEmbedding_of_surjective
theorem Embedding.toOpenEmbedding_of_surjective :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Embedding f → Function.Surjective f → OpenEmbedding f
The theorem `Embedding.toOpenEmbedding_of_surjective` states that for any two types `X` and `Y` with their respective topological spaces, if a function `f` from `X` to `Y` is a surjective embedding, then `f` is an open embedding. Here, a surjective function is one where every element in `Y` is the image of at least one element in `X` under `f`, an embedding is a function that is injective (one-to-one) and continuous, and an open embedding is an embedding that additionally carries open sets to open sets. Thus, this theorem connects the notions of surjectivity, embeddings and open embeddings in topology.
More concisely: If `f` is a surjective embedding between topological spaces `X` and `Y`, then `f` is an open embedding.
|
Inducing.map_nhds_of_mem
theorem Inducing.map_nhds_of_mem :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f → ∀ (x : X), Set.range f ∈ nhds (f x) → Filter.map f (nhds x) = nhds (f x)
This theorem states that for any two types `X` and `Y`, a function `f` from `X` to `Y`, and points `x` in `X`, if the function `f` is inducing (i.e., the topology on `X` is the coarsest topology such that `f` is continuous) and the range of the function `f` is in the neighborhood of `f(x)`, then the forward map of the filter of `nhds x` under `f` is equal to the neighborhood of `f(x)`. In other words, mapping the neighborhood filter at `x` through `f` gives you the neighborhood filter at `f(x)` when `f` is inducing and the image of `f` lies within the neighborhood of `f(x)`.
More concisely: If function `f` from type `X` to `Y` is inducing and the range of `f` is in the neighborhood of `f(x)` for some `x` in `X`, then the image of the neighborhood filter of `x` under `f` equals the neighborhood filter of `f(x)`.
|
IsOpenMap.mapsTo_interior
theorem IsOpenMap.mapsTo_interior :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → ∀ {s : Set X} {t : Set Y}, Set.MapsTo f s t → Set.MapsTo f (interior s) (interior t)
The theorem `IsOpenMap.mapsTo_interior` states that for any given two types `X` and `Y`, along with their respective topological structures, and a function `f` from `X` to `Y` which is an open map, if `f` maps a set `s` from `X` to a set `t` in `Y`, then `f` also maps the interior of `s` (the largest open subset of `s`) to the interior of `t` (the largest open subset of `t`). This theorem is an important property in the study of open maps in topology.
More concisely: If `f: X �ึ� Y` is an open map between topological spaces `(X, τX)` and `(Y, τY)`, and `s ⊆ X` has an open interior `int(s)`, then `f(int(s)) = int(f(s))`.
|
closedEmbedding_of_continuous_injective_closed
theorem closedEmbedding_of_continuous_injective_closed :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Continuous f → Function.Injective f → IsClosedMap f → ClosedEmbedding f
The theorem `closedEmbedding_of_continuous_injective_closed` states that for any two types `X` and `Y`, along with a function `f` from `X` to `Y`, given that `X` and `Y` are topological spaces, if the function `f` is continuous, injective (that is, `f x = f y` implies `x = y`), and a closed map (that is, the image of any closed set of `X` is closed in `Y`), then `f` is a closed embedding. A closed embedding, in the context of topology, is a function that is injective, continuous, its image is a closed set, and the function induces a homeomorphism (bijective, continuous, and has continuous inverse) between the original space and the image space.
More concisely: If a continuous, injective, and closed function between topological spaces X and Y maps closed sets to closed sets, then it is a closed embedding.
|
Function.Injective.embedding_induced
theorem Function.Injective.embedding_induced :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [t : TopologicalSpace Y], Function.Injective f → Embedding f
This theorem states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, if `Y` is equipped with a topological space structure and the function `f` is injective (meaning that if `f x = f y`, then `x = y`), then `f` is an embedding. An embedding in this context is a function that induces a topology on `X` from the topology on `Y`, such that the function is continuous and its inverse function from its image to `X` is also continuous.
More concisely: If `f` is an injective function from type `X` to a topological space `Y`, then `f` is an embedding.
|
OpenEmbedding.isOpenMap
theorem OpenEmbedding.isOpenMap :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
OpenEmbedding f → IsOpenMap f
The theorem `OpenEmbedding.isOpenMap` states that for any given types `X` and `Y` and a function `f` from `X` to `Y`, if both `X` and `Y` have a `TopologicalSpace` instance, then if `f` is an open embedding, `f` is also an open map. In other words, if `f` is an open embedding, which means it is a function that is both injective and continuous, and the image of any open set in `X` is open in `Y`, then the image of any open set under `f` is still open in `Y`.
More concisely: If `f` is an open embedding from a topological space `X` to a topological space `Y`, then the image of every open set in `X` under `f` is an open set in `Y`.
|
OpenEmbedding.continuous
theorem OpenEmbedding.continuous :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
OpenEmbedding f → Continuous f
This theorem asserts that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, if `X` and `Y` are equipped with a topological space structure, then if `f` is an open embedding, it is also continuous. In terms of topology, this means that if `f` is a function that preserves the open set structure (i.e., the image of any open set in `X` under `f` is an open set in `Y`), then `f` also preserves the nearbyness relation (i.e., `f` is continuous). Thus, any open embedding between topological spaces is a continuous map.
More concisely: If `f` is an open embedding between topological spaces `X` and `Y`, then `f` is a continuous function.
|
QuotientMap.isClosed_preimage
theorem QuotientMap.isClosed_preimage :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
QuotientMap f → ∀ {s : Set Y}, IsClosed (f ⁻¹' s) ↔ IsClosed s
The theorem `QuotientMap.isClosed_preimage` states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, given that `f` is a quotient map (which is defined as a surjective function such that a set `s` in `Y` is open if and only if its preimage in `X` is an open set), then for any set `s` of type `Y`, the preimage of `s` under `f` is closed if and only if `s` is closed. In other words, a set in the codomain `Y` is closed if and only if its corresponding preimage in the domain `X` is closed, when the function mapping `X` to `Y` is a quotient map.
More concisely: For a surjective function `f` between types `X` and `Y` being a quotient map implies that the preimage of a closed set in `Y` under `f` is closed in `X`.
|
IsOpenMap.of_nhds_le
theorem IsOpenMap.of_nhds_le :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
(∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)) → IsOpenMap f
This theorem states that for any two topological spaces `X` and `Y`, and a function `f` from `X` to `Y`, if for every element `x` in `X`, the neighborhood filter of `f(x)` is less than or equal to the filter obtained by mapping `f` over the neighborhood filter of `x`, then `f` is an open map. An open map is a function where for any open set in `X`, its image under `f` is an open set in `Y`.
More concisely: If for every x in X, the neighborhood filter of f(x) is contained in the filter obtained by mapping f over the neighborhood filter of x, then f is an open map.
|
Inducing.continuousAt_iff
theorem Inducing.continuousAt_iff :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
Inducing g → ∀ {x : X}, ContinuousAt f x ↔ ContinuousAt (g ∘ f) x
The theorem `Inducing.continuousAt_iff` states that, for any three types `X`, `Y`, `Z` representing topological spaces, and for any two functions `f` from `X` to `Y` and `g` from `Y` to `Z`, if `g` is an inducing function, then the function `f` is continuous at a point `x` in `X` if and only if the composition of `g` and `f` (denoted as `(g ∘ f)`) is continuous at the same point `x`. Here, a function is said to be continuous at a point if the function's value at any point close to `x` gets close to the function's value at `x`. An inducing function is one that creates a coarser (or equal) topology on its domain when its codomain is considered with a given topology.
More concisely: A function `f : X → Y` is continuous at a point `x ∈ X` if and only if the composition `g ∘ f` is continuous at `x`, where `g : Y → Z` is an inducing function.
|
Embedding.continuous_iff
theorem Embedding.continuous_iff :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], Embedding g → (Continuous f ↔ Continuous (g ∘ f))
This theorem states that for any types `X`, `Y`, and `Z`, and any functions `f` from `X` to `Y` and `g` from `Y` to `Z`, assuming `X`, `Y`, `Z` are topological spaces, and `g` is an embedding, then `f` is continuous if and only if the composition of `g` and `f` (`g ∘ f`) is continuous. In mathematical terms, if `g` is an embedding from a topological space `Y` to `Z`, then a function `f` from `X` to `Y` is continuous if and only if the function obtained by composing `f` with `g` is continuous.
More concisely: If `g` is a topological space embedding from `Y` to `Z`, then a function `f` from `X` to `Y` is continuous if and only if the composition `g ∘ f` is continuous.
|
inducing_induced
theorem inducing_induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] (f : X → Y), Inducing f := by
sorry
This theorem states that for any two types `X` and `Y`, where `Y` has a topological space structure, and for any function `f` from `X` to `Y`, the function `f` is inducing. In the context of topology, an "inducing" function is one that makes the topology on the domain `X` the same as the topology on the image of `f`, when the image is considered as a subspace of `Y`.
More concisely: For any continuous function $f : X \rightarrow Y$ between topological spaces $X$ and $Y$, the topology on $X$ induced by $Y$'s topology is equal to the preimage topology on $X$ under $f$.
|
Embedding.continuous
theorem Embedding.continuous :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Embedding f → Continuous f
This theorem states that for any two types `X` and `Y`, given a function `f` from `X` to `Y`, and assuming that both `X` and `Y` have topological space structures, if `f` is an embedding (i.e., an injective (one-to-one) function that preserves the topology), then `f` is also continuous. In terms of topology, a function is continuous if the preimage of every open set in the codomain is an open set in the domain.
More concisely: If `X` and `Y` are topological spaces and `f : X → Y` is an injective function that preserves open sets, then `f` is continuous.
|
isClosedMap_iff_clusterPt
theorem isClosedMap_iff_clusterPt :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsClosedMap f ↔
∀ (s : Set X) (y : Y),
MapClusterPt y (Filter.principal s) f → ∃ x, f x = y ∧ ClusterPt x (Filter.principal s)
The theorem `isClosedMap_iff_clusterPt` states that a function `f` mapping from a topological space `X` to another topological space `Y`, is a closed map if and only if for every set `s` in `X`, any cluster point of the image of `s` under `f` is itself the image under `f` of some cluster point of `s`. This means that `f` sends cluster points of `s` to cluster points of the image of `s`. This concept is related to the notion of proper maps, which requires this condition for all filters (not just principal filters) and also requires that `f` is continuous.
More concisely: A function between topological spaces is closed if and only if it sends cluster points of every set to cluster points of their images.
|
IsOpenMap.isOpen_range
theorem IsOpenMap.isOpen_range :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → IsOpen (Set.range f)
The theorem `IsOpenMap.isOpen_range` states that for any two types `X` and `Y`, and for any function `f` from `X` to `Y`, if `f` is an open map (meaning that if a set `U` in `X` is open, then its image under `f` is open in `Y`), then the range of `f` (which is the set of all values `f(x)` where `x` is in `X`) is an open set in the topological space `Y`. This theorem is a property of open maps in the context of topology.
More concisely: If `f` is an open map from a topological space `X` to a topological space `Y`, then the range of `f` is an open set in `Y`.
|
openEmbedding_of_embedding_open
theorem openEmbedding_of_embedding_open :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Embedding f → IsOpenMap f → OpenEmbedding f
The theorem `openEmbedding_of_embedding_open` states that for any two types `X` and `Y` with associated topological spaces, and any function `f` from `X` to `Y`, if `f` is an embedding and an open map, then `f` is an open embedding. Here, an embedding is a function that is injective (one-to-one) and its image under `f` is homeomorphic to the preimage. An open map is a function where the image of any open set is still open. Finally, an open embedding is a function which is both an embedding and an open map.
More concisely: If a function between topological spaces is both an embedding and an open map, then it is an open embedding.
|
QuotientMap.isOpen_preimage
theorem QuotientMap.isOpen_preimage :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
QuotientMap f → ∀ {s : Set Y}, IsOpen (f ⁻¹' s) ↔ IsOpen s
This theorem states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, given that `X` and `Y` are both topological spaces and `f` is a quotient map, then for any set `s` of `Y`, `s` is an open set if and only if its preimage under `f` is an open set. In simpler terms, a set in the target space `Y` of the quotient map is open if and only if all the elements in the source space `X` that map into this set form an open set.
More concisely: Given two topological spaces X and Y and a quotient map f : X -> Y between them, the preimage under f of any open set in Y is open in X.
|
QuotientMap.continuous_iff
theorem QuotientMap.continuous_iff :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
QuotientMap f → (Continuous g ↔ Continuous (g ∘ f))
The theorem `QuotientMap.continuous_iff` states that for any three types `X`, `Y` and `Z`, which have topological space structures, and any two functions `f` from `X` to `Y` and `g` from `Y` to `Z`, if `f` is a quotient map, then the function `g` is continuous if and only if the composition of `g` and `f` (i.e., `g ∘ f`) is continuous. In mathematical terms, under the condition that the function `f: X → Y` is a quotient map, the continuity of the function `g: Y → Z` is equivalent to the continuity of the composed function `(g ∘ f): X → Z`.
More concisely: A quotient map's composability with a continuous function results in a continuous image function. In other words, if `f: X → Y` is a quotient map and `g: Y → Z` is continuous, then `g ∘ f: X → Z` is continuous.
|
inducing_iff_nhds
theorem inducing_iff_nhds :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Inducing f ↔ ∀ (x : X), nhds x = Filter.comap f (nhds (f x))
This theorem states that for any two types `X` and `Y`, and a function `f` from `X` to `Y`, if both `X` and `Y` have a topological space structure, then `f` is an inducing function if and only if, for every element `x` of `X`, the neighborhood filter of `x` in `X` is equivalent to the preimage under `f` of the neighborhood filter of `f(x)` in `Y`. In simpler terms, a function induces a topology on its domain if the neighborhoods of each point in the domain are exactly the preimages of the neighborhoods of their images in the codomain.
More concisely: A function between topological spaces induces the same neighborhood structure on each point if and only if the preimage of every neighborhood of its image under the function is the neighborhood of that point in the domain.
|
Inducing.comp
theorem Inducing.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], Inducing g → Inducing f → Inducing (g ∘ f)
This theorem states that for any three types `X`, `Y`, and `Z`, and two functions `f : X → Y` and `g : Y → Z`, given that the topological spaces on `X`, `Y`, and `Z` are defined, if `g` is an inducing function (preserves the topology) and `f` is also an inducing function, then the composition of `g` and `f` (denoted as `g ∘ f`) is also an inducing function. The theorem thus establishes the transitivity of inducing functions in a topological context.
More concisely: If functions `f : X → Y` and `g : Y → Z` are indising functions between topological spaces `X`, `Y`, and `Z` respectively, then their composition `g ∘ f` is also an inducing function between `X` and `Z`.
|
IsOpenMap.id
theorem IsOpenMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap id
This theorem states that for any type `X` with a topology (that is, `X` forms a topological space), the identity function on `X` is an open map. In terms of mathematics, the theorem says that for all open sets `U` in the topological space `X`, the image of `U` under the identity function is also an open set in `X`. This is expected because the identity function does not change any elements of the set it is applied to.
More concisely: For any topological space (X,τ), the identity function on X is an open map, that is, for all open sets U ∈ τ, the image of U under the identity function is also an open set in X.
|
QuotientMap.surjective
theorem QuotientMap.surjective :
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
QuotientMap f → Function.Surjective f
The theorem `QuotientMap.surjective` states that for any two types `X` and `Y` and a function `f` from `X` to `Y`, if the topological spaces `X` and `Y` exist, and if `f` is a quotient map, then `f` is a surjective function. In the context of mathematics, this means that for any given element in the codomain `Y`, there exists at least one element in the domain `X` that maps to it under `f`. This is a property of quotient maps in topology, which are defined as surjective (onto) functions between topological spaces that respect the structure of the spaces in the sense that a set in the codomain is open if and only if its preimage in the domain is open.
More concisely: If `f` is a quotient map between topological spaces `X` and `Y`, then `f` is surjective.
|
IsClosedMap.id
theorem IsClosedMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsClosedMap id
This theorem states that for any type `X` which has a topology `inst`, the identity function `id` is a closed map. In other words, if we consider any type `X` endowed with a topological structure, the identity function, which maps each element of `X` to itself, has the property that the image of any closed set under this function is also a closed set in `X`.
More concisely: For any topological space (type `X` with topology `inst`), the identity function is a continuous map and thus preserves closed sets.
|