DenseEmbedding.inj
theorem DenseEmbedding.inj :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
DenseEmbedding e → Function.Injective e
The theorem states that for any given types `α` and `β`, both equipped with a topological space structure (denoted as `TopologicalSpace α` and `TopologicalSpace β`), if a function `e : α → β` is a dense embedding, then this function `e` is injective. In mathematical terms, this means that if `e` is a function such that the image of `e` is dense in `β` and `e` preserves the topological structure, then `e` has the property that for any two elements `a₁` and `a₂` in `α`, if `e(a₁)` equals `e(a₂)`, then `a₁` must be equal to `a₂`.
More concisely: If `e : α → β` is a dense embedding of topological spaces `α` and `β`, then `e` is injective.
|
DenseInducing.tendsto_comap_nhds_nhds
theorem DenseInducing.tendsto_comap_nhds_nhds :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α]
[inst_1 : TopologicalSpace β] {i : α → β} [inst_2 : TopologicalSpace δ] {f : γ → α} {g : γ → δ} {h : δ → β}
{d : δ} {a : α},
DenseInducing i →
Filter.Tendsto h (nhds d) (nhds (i a)) → h ∘ g = i ∘ f → Filter.Tendsto f (Filter.comap g (nhds d)) (nhds a)
This theorem states that for given topological spaces `α`, `β`, `δ`, `γ`, and specific functions `f: γ → α`, `g: γ → δ`, `h: δ → β` and `i: α → β`, if the function `i` is dense-inducing and the function `h` tends to map neighborhoods of `d` in `δ` to neighborhoods of `i(a)` in `β`, and if `h` composed with `g` equals `i` composed with `f`, then `f` tends to map the preimage of `d`'s neighborhoods under `g` (from the neighborhood filter of `d` in `δ`) to neighborhoods of `a` in `α`.
More concisely: If `i` is dense-inducing, `h(g(U)) = i(f(U))` for all neighborhoods `U` of `d` in `γ`, and `h` maps neighborhoods of `d` in `δ` to neighborhoods of `i(a)` in `β`, then `f` maps the preimage of neighborhoods of `d` under `g` in `α` to neighborhoods of `a`.
|
DenseInducing.separableSpace
theorem DenseInducing.separableSpace :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
DenseInducing i → ∀ [inst : TopologicalSpace.SeparableSpace α], TopologicalSpace.SeparableSpace β
This theorem states that if we have a map `i` that is `DenseInducing` from a topological space `α` to another topological space `β`, and if `α` is a separable space, then `β` is also a separable space. In other words, the property of being a separable space, which means that there exists a countable, dense subset, is preserved under a `DenseInducing` map.
More concisely: If `α` is a separable topological space and `i : α → β` is a `DenseInducing` map, then `β` is a separable topological space.
|
DenseInducing.extend_eq
theorem DenseInducing.extend_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
(di : DenseInducing i) [inst_2 : TopologicalSpace γ] [inst_3 : T2Space γ] {f : α → γ},
Continuous f → ∀ (a : α), di.extend f (i a) = f a
This theorem states that for any types `α`, `β`, and `γ` with `α`, `β`, and `γ` being topological spaces and `γ` also being a T2 space (Hausdorff space), for any function `i` from `α` to `β` which is a dense inducing function, and any continuous function `f` from `α` to `γ`, the value of the extension of `f` by `i` at `i(a)` is equal to `f(a)` for each `a` in `α`. Essentially, if you have a continuous function `f` and a dense inducing function `i`, you can extend `f` using `i` without changing its values.
More concisely: For any dense inducing function `i` from a topological space `α` to another topological space `β`, and any continuous function `f` from `α` to a Hausdorff space `γ`, the extension of `f` by `i` equals `f` on the domain of `i`.
|
DenseInducing.nhds_eq_comap
theorem DenseInducing.nhds_eq_comap :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
DenseInducing i → ∀ (a : α), nhds a = Filter.comap i (nhds (i a))
This theorem states that for any types `α` and `β`, each equipped with a topological space structure, if `i` is a function from `α` to `β` that induces a dense topology, then the neighborhood filter of any element `a` in `α` is equal to the filter obtained by the pre-image (or `comap`) of the function `i` applied to the neighborhood filter of `i(a)` in `β`. In mathematical notation, this is saying that for a densely inducing function `i`, the filter of neighborhoods around a point `a` is exactly the pullback of the filter of neighborhoods around `i(a)` via the function `i`.
More concisely: For a densely inducing function between topological spaces, the filter of neighborhoods of a point is equal to the pullback of the filter of neighborhoods of its image under the function.
|
isClosed_property
theorem isClosed_property :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → Prop},
DenseRange e → IsClosed {x | p x} → (∀ (a : α), p (e a)) → ∀ (b : β), p b
The theorem `isClosed_property` states that for any types `α` and `β` and any topological space over `β`, given a function `e` from `α` to `β`, a predicate `p` over `β`, if `e` has a dense range, and the set of `β` satisfying `p` is closed, and `p` holds for every element in the image of `e`, then `p` holds for all `b` in `β`. In other words, if we have a function whose range densely covers a topological space and a property that holds for all points in the dense range and that defines a closed set, then that property must hold throughout the entire space.
More concisely: If a function with a dense range maps a closed set to a property, then the property holds for all elements in the target space.
|
DenseEmbedding.prod
theorem DenseEmbedding.prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {e₁ : α → β}
{e₂ : γ → δ}, DenseEmbedding e₁ → DenseEmbedding e₂ → DenseEmbedding fun p => (e₁ p.1, e₂ p.2)
This theorem states that the product of two dense embeddings creates another dense embedding. More precisely, if we have two types `α` and `γ` with respective topologies and two dense embeddings `e₁ : α → β` and `e₂ : γ → δ`, then the function that maps a pair `(a, c)` to the pair `(e₁ a, e₂ c)` is also a dense embedding. Here, `DenseEmbedding` refers to a function between two topological spaces that has a dense image and is a homeomorphism onto its image.
More concisely: If `e₁ : α → β` and `e₂ : γ → δ` are dense embeddings, then the function `(a, c) ↦ (e₁ a, e₂ c)` is a dense embedding from `α × γ` to `β × δ`.
|
DenseInducing.extend_eq'
theorem DenseInducing.extend_eq' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
[inst_2 : TopologicalSpace γ] [inst_3 : T2Space γ] {f : α → γ} (di : DenseInducing i),
(∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) → ∀ (a : α), di.extend f (i a) = f a
This theorem, `DenseInducing.extend_eq'`, states that for any types `α`, `β` and `γ` with `α` and `β` being topological spaces and `γ` being a T2 space, and any function `i : α → β` that induces a dense set, if for every `b : β` there exists a `c` such that the function `f : α → γ` tends to `nhds c` when mapped along the filter `comap i (nhds b)`, then for every `a : α`, the function `di.extend f (i a)` is equal to `f a`. In simple terms, it says that under certain conditions, the extension of a function `f` through a dense inducing function `i` is equal to `f` itself. This theorem is a stronger version of continuity for `f` and can be useful to avoid proving the same conditions twice in certain cases.
More concisely: If `i : α → β` is a dense function between topological spaces `α` and `β`, and `γ` is a T2 space, such that the function `f : α → γ` tends to the neighborhood filter of each point `b ∈ β` when mapped along `comap i`, then `di.extend f (i a) = f a` for all `a ∈ α`.
|
DenseInducing.extend_eq_at
theorem DenseInducing.extend_eq_at :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
(di : DenseInducing i) [inst_2 : TopologicalSpace γ] [inst_3 : T2Space γ] {f : α → γ} {a : α},
ContinuousAt f a → di.extend f (i a) = f a
This theorem states that for all types `α`, `β`, and `γ`, given the topological space structures on them, a function `i : α → β` that induces a dense embedding, and a function `f : α → γ`, if `f` is continuous at a point `a` in type `α`, then the extension of `f` by the dense inducing function `i` evaluated at `i a` is equal to `f a`. Here, a `DenseInducing` function `i` means that the image of any open set in `α` under `i` is dense in `β`, and `ContinuousAt f a` means that the function `f` is continuous at the point `a`. The condition `[inst_3 : T2Space γ]` refers to `γ` being a Hausdorff space (or T2 space), meaning that any two distinct points in `γ` can be separated by disjoint open sets.
More concisely: Given a dense inducing function `i` from type `α` to type `β`, a continuous function `f` from `α` to Hausdorff space `γ` at a point `a` in `α`, the extension of `f` by `i` at `i(a)` equals `f(a)`.
|
DenseRange.equalizer
theorem DenseRange.equalizer :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
[inst_2 : T2Space γ] {f : α → β},
DenseRange f → ∀ {g h : β → γ}, Continuous g → Continuous h → g ∘ f = h ∘ f → g = h
This theorem states that for any three types `α`, `β`, and `γ`, given that `β` and `γ` are topological spaces and `γ` is a T2 space (also known as a Hausdorff space), and given a function `f` from `α` to `β` that has a dense range, for any two continuous functions `g` and `h` from `β` to `γ`, if `g` and `h` agree on the image of `f` (meaning, `g ∘ f = h ∘ f`), then `g` and `h` must be the same function. This captures the intuition that in a Hausdorff space, points can be separated by neighborhoods, so if two continuous functions agree on a dense subset, they must agree everywhere.
More concisely: If `β` and `γ` are topological spaces with `γ` being Hausdorff, and `f: α → β` has a dense range, then any two continuous functions `g, h: β → γ` that agree on the image of `f` (`g ∘ f = h ∘ f`) are equal.
|
DenseEmbedding.separableSpace
theorem DenseEmbedding.separableSpace :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
DenseEmbedding e → ∀ [inst : TopologicalSpace.SeparableSpace α], TopologicalSpace.SeparableSpace β
This theorem states that if a function 'e' is a dense embedding from one topological space into another, and if the domain of this function is a separable space (i.e., it contains a countable dense subset), then the codomain of the function is also a separable space. In other words, under these conditions, the property of separability is preserved under dense embeddings.
More concisely: If a separable topological space is densely embedded into a Hausdorff space, then the codomain is also separable.
|
DenseInducing.interior_compact_eq_empty
theorem DenseInducing.interior_compact_eq_empty :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
[inst_2 : T2Space β], DenseInducing i → Dense (Set.range i)ᶜ → ∀ {s : Set α}, IsCompact s → interior s = ∅
The theorem `DenseInducing.interior_compact_eq_empty` states that given two topological spaces `α` and `β`, and a function `i : α → β` that exhibits a dense inducing, if the complement of the range of `i` is also dense, then for any compact set `s` in `α`, the interior of `s` is empty. Here, a function is called dense inducing if the closure of the image of the function equals the entire codomain and the function is inducing, meaning the topology on the domain can be recovered from the topology on the codomain and the function itself. The theorem, in essence, establishes a connection between dense inducing functions and compact sets, stating that such functions can lead to compact sets having an empty interior under certain conditions.
More concisely: Given topological spaces α and β, a dense inducing function i : α → β with dense complement, implies that the interior of any compact set in α is empty.
|
DenseInducing.continuous
theorem DenseInducing.continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
DenseInducing i → Continuous i
This theorem states that for any two types `α` and `β`, given that `α` and `β` are topological spaces, if a function `i` from `α` to `β` is dense inducing, then `i` is continuous. Here, dense inducing refers to a function that has the property of being both dense and inducing – the image of the function is a dense subset of the codomain, and the function induces the topology of the codomain on the domain. Hence, the theorem essentially establishes the continuity of any dense inducing function in a topological context.
More concisely: If `α` and `β` are topological spaces, and `i : α → β` is a dense and inducing function, then `i` is continuous.
|
DenseInducing.prod
theorem DenseInducing.prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {e₁ : α → β}
{e₂ : γ → δ}, DenseInducing e₁ → DenseInducing e₂ → DenseInducing fun p => (e₁ p.1, e₂ p.2)
This theorem states that the Cartesian product of two dense inducing functions results in another dense inducing function. In the context of topology, given two topological spaces `α` and `γ` mapped onto `β` and `δ` respectively by dense inducing functions `e₁` and `e₂`, the function that maps a pair `(a,c)` from `α × γ` to `(e₁ a, e₂ c)` in `β × δ` is also dense inducing.
More concisely: If `e₁:` `α` → `β` and `e₂:` `γ` → `δ` are dense functions, then the function `(e₁, e₂): α × γ` → `β × δ` given by `(a, c)` ↦ `(e₁ a, e₂ c)` is also a dense function.
|
DenseInducing.extend_eq_of_tendsto
theorem DenseInducing.extend_eq_of_tendsto :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
(di : DenseInducing i) [inst_2 : TopologicalSpace γ] [inst_3 : T2Space γ] {b : β} {c : γ} {f : α → γ},
Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c) → di.extend f b = c
The theorem `DenseInducing.extend_eq_of_tendsto` states that for all types `α`, `β` and `γ` with their respective topological spaces, and given a function `i : α → β` that induces a dense subset, another function `f : α → γ`, and elements `b : β`, `c : γ`, if `f` tends to `c` at the preimage of the neighborhood of `b` under `i`, then the extension of `f` with respect to the dense inducing function `i` at point `b` is equal to `c`. The space `γ` also needs to be a Hausdorff space (`T2Space`), which means any two distinct points in `γ` can be separated by neighbourhoods.
More concisely: Given a dense function `i : α → β` between Hausdorff spaces `α`, `β`, and `γ`, if `f : α → γ` tends to `c` at the preimages of neighborhoods of `b ∈ β`, then `f`'s extension at `b` is equal to `c`.
|
DenseInducing.dense
theorem DenseInducing.dense :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
DenseInducing i → DenseRange i
This theorem states that for any two types `α` and `β`, each with its own topological space structure, if we have a map `i` from `α` to `β` that is dense inducing, then the range of this map `i` is a dense set in `β`. In mathematical terms, given a map `i: α → β`, if `i` is dense inducing, then the image of `α` under `i` is a dense subset of `β`.
More concisely: If `i: α → β` is a dense-inducing map between topological spaces `α` and `β`, then the image of `α` under `i` is a dense subset of `β`.
|
DenseRange.induction_on
theorem DenseRange.induction_on :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β},
DenseRange e → ∀ {p : β → Prop} (b₀ : β), IsClosed {b | p b} → (∀ (a : α), p (e a)) → p b₀
This theorem states that for any two types `α` and `β`, with `β` having a topological space structure, and any function `e` from `α` to `β` whose range is dense in `β`, for any property `p` of elements in `β` and any element `b₀` in `β`, if the set of elements in `β` that satisfy the property `p` is a closed set, and if all the images of elements in `α` under the function `e` satisfy the property `p`, then the element `b₀` also satisfies the property `p`.
More concisely: If `e: α → β` is a dense function from type `α` to a topological space `β` with property `p` holding for all images `e(a)` in `β` for `a` in `α`, and the set of elements in `β` satisfying `p` is closed, then `b₀` satisfies `p` for any `b�!_0` in `β`.
|