instMetrizableSpaceOnePointNat — Mathlib

English

The space OnePoint(ℕ) is metrizable because natUnionInftyEmbedding is a closed embedding; hence the topology is metrizable.

Русский

Пространство OnePoint(ℕ) метризуемо, поскольку natUnionInftyEmbedding является замкнутым вложением, следовательно, топология метризуема.

LaTeX

$$$\operatorname{MetrizableSpace}(\mathrm{OnePoint}(\mathbb{N}))$$$

Lean4

instance : MetrizableSpace (OnePoint ℕ) :=
  isClosedEmbedding_natUnionInftyEmbedding.metrizableSpace

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