pseudoMetricSpace — Mathlib

English

There exists a canonical construction of a PseudoMetricSpace structure compatible with a given UniformSpace using a chosen basis.

Русский

Существует каноническая конструция псевдометрического пространство, совместимая с данным равномерным пространством, через базис.

LaTeX

$$$\\text{UniformSpace.metrizable_uniformity}$ yields a PseudoMetricSpace structure on X$$

Lean4

/-- A `PseudoMetricSpace` instance compatible with a given `UniformSpace` structure. -/
protected noncomputable def pseudoMetricSpace (X : Type*) [UniformSpace X] [IsCountablyGenerated (𝓤 X)] :
    PseudoMetricSpace X :=
  (UniformSpace.metrizable_uniformity X).choose.replaceUniformity <|
    congr_arg _ (UniformSpace.metrizable_uniformity X).choose_spec.symm

Похожие утверждения