continuous_toCloseds — Mathlib

English

If α is second countable, then NonemptyCompacts α is second countable.

Русский

Если пространство α вторично счётно, то NonemptyCompacts α также вторично счётно.

LaTeX

$$$[\\text{SecondCountableTopology }\\alpha] \\Rightarrow \\text{SecondCountableTopology}(\\text{NonemptyCompacts }\\alpha).$$$

Lean4

/-- `NonemptyCompacts.toCloseds` is continuous (as it is an isometry) -/
@[fun_prop]
theorem continuous_toCloseds : Continuous (@NonemptyCompacts.toCloseds α _ _) :=
  isometry_toCloseds.continuous

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