Documentation

Mathlib.Topology.Metrizable.Basic

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.

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

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

    Equations
    Instances For

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

      @[instance 100]

      Every pseudo-metrizable space is first countable.

      Equations
      • =
      instance TopologicalSpace.pseudoMetrizableSpace_pi {ι : Type u_1} {π : ιType u_4} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (π i)] :
      Equations
      • =

      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.

      • exists_metric : ∃ (m : MetricSpace X), UniformSpace.toTopologicalSpace = t
      Instances
        theorem TopologicalSpace.MetrizableSpace.exists_metric {X : Type u_5} {t : TopologicalSpace X} [self : TopologicalSpace.MetrizableSpace X] :
        ∃ (m : MetricSpace X), UniformSpace.toTopologicalSpace = t
        @[instance 100]
        Equations
        • =

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

        Equations
        Instances For

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

          instance TopologicalSpace.metrizableSpace_pi {ι : Type u_1} {π : ιType u_4} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TopologicalSpace.MetrizableSpace (π i)] :
          Equations
          • =