metrizableSpace_of_t3_secondCountable

English

A T3 space with second-countable topology is metrizable (admits a metric generating the topology).

Русский

Т3-пространство с топологией второй счетности метризуемо; существует метрика, порождающая топологию.

LaTeX

$$$\\forall X [\\text{TopologicalSpace}(X)] [\\text{T3Space}(X)] [\\text{SecondCountableTopology}(X)],\\; \\text{MetrizableSpace}(X)$$$

Lean4

/-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second
countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
same topology. -/
instance (priority := 90) metrizableSpace_of_t3_secondCountable : MetrizableSpace X :=
  let ⟨_, hf⟩ := exists_embedding_l_infty X
  hf.metrizableSpace

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