IsClosed.isClopenable
theorem IsClosed.isClopenable :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PolishSpace α] {s : Set α},
IsClosed s → PolishSpace.IsClopenable s
This theorem states that for any given closed set `s` in a Polish space (a completely separable, completely metrizable topological space), it is possible to construct a finer Polish topology in which the set `s` is both open and closed. In other words, given the type `α` with an existing topological space and a Polish space, and a subset `s` of `α` that is closed, there exists a refined Polish topology, under which the set `s` is clopen (both open and closed). This theorem provides a link between the concepts of closed sets and 'clopenable' sets in the context of Polish spaces.
More concisely: Given a closed subset `s` of a Polish space `α`, there exists a finer Polish topology on `α` making `s` clopen.
|
PolishSpace.exists_polishSpace_forall_le
theorem PolishSpace.exists_polishSpace_forall_le :
∀ {α : Type u_1} {ι : Type u_3} [inst : Countable ι] [t : TopologicalSpace α] [p : PolishSpace α]
(m : ι → TopologicalSpace α),
(∀ (n : ι), m n ≤ t) → (∀ (n : ι), PolishSpace α) → ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
This theorem states that given a Polish space (a separable completely metrizable topological space), and a countable array of finer Polish topologies on the same set, there exists another Polish topology which is finer than every topology in the given array and coarser than the original topology. Here, 'finer' means that every open set in the 'coarser' topology is also an open set in the 'finer' topology. This theorem shows that a Polish space provides the structure for a countable refinement of topologies that maintain the Polish property.
More concisely: Given a Polish space and a countable array of finer Polish topologies, there exists a Polish topology that is coarser than the original topology and finer than every topology in the array.
|
PolishSpace.exists_nat_nat_continuous_surjective
theorem PolishSpace.exists_nat_nat_continuous_surjective :
∀ (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : PolishSpace α] [inst_2 : Nonempty α],
∃ f, Continuous f ∧ Function.Surjective f
The theorem states that for any nonempty Polish space (a complete, separable, metric topological space), there exists a continuous function that is surjective (onto) from the topological space of sequences of natural numbers to this Polish space. In other words, any point in the Polish space can be mapped to from a sequence of natural numbers via a continuous function, effectively saying that the Polish space can be represented as a continuous image of the space of sequences of natural numbers.
More concisely: Every nonempty Polish space admits a surjective continuous function from the space of sequences of natural numbers.
|
IsOpen.polishSpace
theorem IsOpen.polishSpace :
∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : PolishSpace α] {s : Set α}, IsOpen s → PolishSpace ↑s := by
sorry
The theorem `IsOpen.polishSpace` states that for any type `α` with a topological space structure and a Polish space structure, if `s` is a subset of `α` that is open in the given topological space, then the subset `s` is also a Polish space. In other words, open subsets of a Polish space retain the property of being Polish. A Polish space is a separable completely metrizable topological space; that is, it is a space that can be parametrized by a complete metric and is countably dense.
More concisely: If a Polish space `α` has an open subset `s`, then `s` is also a Polish space.
|
Equiv.polishSpace_induced
theorem Equiv.polishSpace_induced :
∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] [inst : PolishSpace β] (f : α ≃ β), PolishSpace α := by
sorry
This theorem states that for any two types `α` and `β`, if `β` is equipped with a topological space structure and a Polish space structure (a completely metrizable, separable topological space), and there exists a bijection (an equivalence, represented by `α ≃ β`) from `α` to `β`, then the topology on `α` induced by this bijection also makes `α` a Polish space. Essentially, it's saying that the property of being a Polish space is preserved under bijections (or equivalences).
More concisely: Given types `α` and `β` with a bijection `α ≃ β`, if `β` is a Polish space, then `α` equipped with the induced topology is also a Polish space.
|
ClosedEmbedding.polishSpace
theorem ClosedEmbedding.polishSpace :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PolishSpace β]
{f : α → β}, ClosedEmbedding f → PolishSpace α
This theorem states that if a function `f` from a topological space `α` to another topological space `β` is a closed embedding and if `β` is a Polish space (a completely metrizable, separable topological space), then `α` is also a Polish space. In other words, the topology of `α` inherits the Polish space properties from `β` through the closed embedding `f`.
More concisely: If `f: α → β` is a closed embedding of a topological space `α` into a Polish space `β`, then `α` is a Polish space.
|
IsClosed.polishSpace
theorem IsClosed.polishSpace :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PolishSpace α] {s : Set α}, IsClosed s → PolishSpace ↑s := by
sorry
The theorem "IsClosed.polishSpace" states that for any given type 'α', which has a topological space structure and a Polish space structure, if 's' is a set of elements of type 'α' and 's' is a closed subset in the given topological space, then the topological subspace induced by 's' is also a Polish space. In other words, it asserts that a closed subset of a Polish space retains the property of being a Polish space.
More concisely: A closed subsets of a Polish space is a Polish space.
|