TopologicalSpace.exists_inducing_l_infty
theorem TopologicalSpace.exists_inducing_l_infty :
∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : RegularSpace X] [inst_2 : SecondCountableTopology X],
∃ f, Inducing f
This theorem states that for any type `X` that is a regular topological space with second countable topology, there exists a function `f` that is an inducing map to `l^∞ = ℕ →ᵇ ℝ` (the space of bounded real-valued sequences). In mathematical terms, it shows the existence of a function that preserves the topological structure of `X` when mapped to the space of bounded sequences, which demonstrates the property of regularity and second countability in the space `X`.
More concisely: For any regular topological space `X` with a second countable topology, there exists a continuous function `f : X → l^∞` preserving the topological structure.
|
TopologicalSpace.exists_embedding_l_infty
theorem TopologicalSpace.exists_embedding_l_infty :
∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : T3Space X] [inst_2 : SecondCountableTopology X],
∃ f, Embedding f
This theorem states that for any type `X` that has a T₃ topological space structure and a second countable topology, there exists a continuous, injective function `f` (an embedding) from `X` to the space of all bounded real-valued sequences, denoted by `ℕ →ᵇ ℝ`. In mathematical terms, a T₃ space, also known as a regular Hausdorff space, is a type of topological space that has certain separation properties, and a second countable topology is a topology that has a countable base. The theorem therefore asserts a specific property about the embeddability of such spaces into the space of bounded real sequences.
More concisely: Given a T₃ and second countable topological space X, there exists a continuous and injective function embedding X into the space of all bounded real-valued sequences.
|