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

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

    @[deprecated IsInducing.pseudoMetrizableSpace]

    Alias of IsInducing.pseudoMetrizableSpace.


    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

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

      @[deprecated IsEmbedding.metrizableSpace]

      Alias of IsEmbedding.metrizableSpace.


      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
      • =