ClosedEmbedding.restrictPreimage
theorem ClosedEmbedding.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
ClosedEmbedding f → ClosedEmbedding (s.restrictPreimage f)
This theorem, referred to as `ClosedEmbedding.restrictPreimage`, asserts that for any two topological spaces `α` and `β`, a function `f` from `α` to `β`, and a set `s` in `β`, if `f` is a closed embedding, then the restriction of `f` to the preimage of `s` (denoted as `(s.restrictPreimage f)`) is also a closed embedding. A "closed embedding" is a function that satisfies certain properties in topology, particularly, it is injective (one-to-one) and the closure of the image of any closed set under the function coincides with the image under the function of the closure of the set.
More concisely: If `f` is a closed embedding from topological space `α` to `β`, then the restriction of `f` to the preimage of any set `s` in `β` is also a closed embedding.
|
OpenEmbedding.restrictPreimage
theorem OpenEmbedding.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
OpenEmbedding f → OpenEmbedding (s.restrictPreimage f)
This theorem, referred to as `OpenEmbedding.restrictPreimage`, states that for any two types `α` and `β` with associated topological spaces, a function `f` from `α` to `β`, and a set `s` of elements in `β`, if `f` is an open embedding (a function that is a homeomorphism onto its image and the image is an open set), then the restriction of the preimage of set `s` under `f` is also an open embedding. This theorem highlights the preservation of the open embedding property under the operation of restriction of preimages.
More concisely: If `f: α → β` is an open embedding and `s ⊆ β` is open, then `f⁁⁻¹(s)` is an open subset of `α` and is an open embedding.
|
Inducing.restrictPreimage
theorem Inducing.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
Inducing f → Inducing (s.restrictPreimage f)
This theorem, referred to as `Inducing.restrictPreimage`, states that for any two types `α` and `β` with topological space structures, a function `f : α → β`, and a set `s` of elements of type `β`, if `f` is an inducing function, then the restriction of the preimage of `f` to the set `s` is also an inducing function.
In more mathematical terms, an inducing function is one that, given the topology of the codomain, induces the topology of the domain. So, if `f` induces the topology of `α` from `β`, then the restriction of the preimage of `f` to `s` will also induce a topology.
More concisely: If `f : α → β` is an inducing function between topological spaces `α` and `β`, then the restriction of `f⁁⁻¹` to a subset `s` of `β` is also an inducing function from `s` to `α`.
|
Embedding.restrictPreimage
theorem Embedding.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
Embedding f → Embedding (s.restrictPreimage f)
The theorem `Embedding.restrictPreimage` asserts that for any two types `α` and `β` having topological space structures, and any function `f` from `α` to `β`, along with a set `s` of type `β`, if `f` is an embedding, then the restriction of the preimage of `f` to the set `s` is also an embedding. In other words, the function that maps each element of `α` to its preimage under `f` in `s` is an embedding if `f` is an embedding.
More concisely: If `f: α → β` is an embedding of topological spaces and `s ⊆ β`, then the restriction of `f⁻¹` to `s` is an embedding from `f⁻¹(s)` to `s`.
|