of_regularSpace_secondCountableTopology

English

A regular space with second countable topology is metrizable (admits a pseudometric that generates the topology).

Русский

Регулярное пространство с второй счетной топологией метризуемо (существует псевдометрическая функция, которая порождает топологию).

LaTeX

$$$\\forall X [\\text{RegularSpace}(X)] [\\text{SecondCountableTopology}(X)],\\; \\text{PseudoMetrizableSpace}(X)$$$

Lean4

/-- *Urysohn's metrization theorem* (Tychonoff's version):
a regular topological space with second countable topology `X` is metrizable,
i.e., there exists a pseudometric space structure that generates the same topology. -/
instance (priority := 90) of_regularSpace_secondCountableTopology : PseudoMetrizableSpace X :=
  let ⟨_, hf⟩ := exists_isInducing_l_infty X
  hf.pseudoMetrizableSpace

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