Documentation

Mathlib.Topology.MetricSpace.Metrizable

Metrizability of a T₃ topological space with second countable topology #

In this file we define metrizable topological spaces, i.e., topological spaces for which there exists a metric space structure that generates the same topology.

We also show that a T₃ topological space with second countable topology X is metrizable.

First we prove that X can be embedded into l^∞, then use this embedding to pull back the metric space structure.

source
class TopologicalSpace.PseudoMetrizableSpace (X : Type u_5) [t : TopologicalSpace X] :
Prop
  • exists_pseudo_metric : ∃ m, UniformSpace.toTopologicalSpace = t

A topological space is pseudo metrizable if there exists a pseudo metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X.

Instances
    source
    instance PseudoMetricSpace.toPseudoMetrizableSpace {X : Type u_5} [m : PseudoMetricSpace X] :
    TopologicalSpace.PseudoMetrizableSpace X
    Equations
    source
    noncomputable def TopologicalSpace.pseudoMetrizableSpacePseudoMetric (X : Type u_5) [TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X] :
    PseudoMetricSpace X

    Construct on a metrizable space a metric compatible with the topology.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance TopologicalSpace.pseudoMetrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace.PseudoMetrizableSpace Y] :
      TopologicalSpace.PseudoMetrizableSpace (X × Y)
      Equations
      source
      theorem Inducing.pseudoMetrizableSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y} (hf : Inducing f) :
      TopologicalSpace.PseudoMetrizableSpace X

      Given an inducing map of a topological space into a pseudo metrizable space, the source space is also pseudo metrizable.

      source
      instance TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology {X : Type u_2} [TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X] :
      TopologicalSpace.FirstCountableTopology X

      Every pseudo-metrizable space is first countable.

      Equations
      source
      instance TopologicalSpace.PseudoMetrizableSpace.subtype {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] (s : Set X) :
      TopologicalSpace.PseudoMetrizableSpace ↑s
      Equations
      source
      instance TopologicalSpace.pseudoMetrizableSpace_pi {ι : Type u_1} {π : ι → Type u_4} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (π i)] :
      TopologicalSpace.PseudoMetrizableSpace ((i : ι) → π i)
      Equations
      source
      class TopologicalSpace.MetrizableSpace (X : Type u_5) [t : TopologicalSpace X] :
      Prop
      • exists_metric : ∃ m, UniformSpace.toTopologicalSpace = t

      A topological space is metrizable if there exists a metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X.

      Instances
        source
        instance MetricSpace.toMetrizableSpace {X : Type u_5} [m : MetricSpace X] :
        TopologicalSpace.MetrizableSpace X
        Equations
        source
        instance TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace {X : Type u_2} [TopologicalSpace X] [h : TopologicalSpace.MetrizableSpace X] :
        TopologicalSpace.PseudoMetrizableSpace X
        Equations
        source
        noncomputable def TopologicalSpace.metrizableSpaceMetric (X : Type u_5) [TopologicalSpace X] [h : TopologicalSpace.MetrizableSpace X] :
        MetricSpace X

        Construct on a metrizable space a metric compatible with the topology.

        Equations
        Instances For
          source
          instance TopologicalSpace.t2Space_of_metrizableSpace {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] :
          T2Space X
          Equations
          source
          instance TopologicalSpace.metrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace X] [TopologicalSpace.MetrizableSpace Y] :
          TopologicalSpace.MetrizableSpace (X × Y)
          Equations
          source
          theorem Embedding.metrizableSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] {f : X → Y} (hf : Embedding f) :
          TopologicalSpace.MetrizableSpace X

          Given an embedding of a topological space into a metrizable space, the source space is also metrizable.

          source
          instance TopologicalSpace.MetrizableSpace.subtype {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] (s : Set X) :
          TopologicalSpace.MetrizableSpace ↑s
          Equations
          source
          instance TopologicalSpace.metrizableSpace_pi {ι : Type u_1} {π : ι → Type u_4} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TopologicalSpace.MetrizableSpace (π i)] :
          TopologicalSpace.MetrizableSpace ((i : ι) → π i)
          Equations
          source
          theorem TopologicalSpace.IsSeparable.secondCountableTopology {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X} (hs : TopologicalSpace.IsSeparable s) :
          TopologicalSpace.SecondCountableTopology ↑s
          source
          theorem TopologicalSpace.exists_embedding_l_infty (X : Type u_2) [TopologicalSpace X] [T3Space X] [TopologicalSpace.SecondCountableTopology X] :
          ∃ f, Embedding f

          A T₃ topological space with second countable topology can be embedded into l^∞ = ℕ →ᵇ ℝ.

          source
          theorem TopologicalSpace.metrizableSpace_of_t3_second_countable (X : Type u_2) [TopologicalSpace X] [T3Space X] [TopologicalSpace.SecondCountableTopology X] :
          TopologicalSpace.MetrizableSpace X

          Urysohn's metrization theorem (Tychonoff's version): a T₃ topological space with second countable topology X is metrizable, i.e., there exists a metric space structure that generates the same topology.

          source
          instance TopologicalSpace.instMetrizableSpaceENNRealInstTopologicalSpaceENNReal :
          TopologicalSpace.MetrizableSpace ENNReal
          Equations