Embedding.metrizableSpace
theorem Embedding.metrizableSpace :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace.MetrizableSpace Y] {f : X → Y}, Embedding f → TopologicalSpace.MetrizableSpace X
This theorem states that if you have a function that embeds a topological space 'X' into a metrizable space 'Y' (a space where you can define a metric or distance function), then the original topological space 'X' is also metrizable. In other words, if you can accurately and continuously map 'X' into 'Y' such that 'Y' can be measured with a metric, then 'X' can also be measured with a metric.
More concisely: If a topological space X admits a continuous embedding into a metrizable space Y, then X is metrizable.
|
Inducing.pseudoMetrizableSpace
theorem Inducing.pseudoMetrizableSpace :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y},
Inducing f → TopologicalSpace.PseudoMetrizableSpace X
This theorem states that for any types `X` and `Y`, given `X` and `Y` are topological spaces and `Y` is a pseudo metrizable space, if there is a function `f` from `X` to `Y` that induces the topology of `X` from `Y`, then `X` is also a pseudo metrizable space. In simpler terms, if we have a map that preserves the topological structure from a pseudo metrizable space to another space, then the latter space is also pseudo metrizable.
More concisely: If `X` and `Y` are topological spaces with `Y` being pseudo metrizable, and there exists a function `f: X → Y` inducing the topology of `X` from `Y`, then `X` is also pseudo metrizable.
|