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
    • One or more equations did not get rendered due to their size.
    Instances For

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

      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

        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

          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