instSecondCountableOpens — Mathlib

English

If α is a second-countable space, then every open subspace U of α is also second-countable.

Русский

Если пространство α вторично счетно, то любая открытая подпространство U ⊆ α тоже вторично счетно.

LaTeX

$$$[\text{SecondCountableTopology}(\alpha)] \Rightarrow \mathrm{SecondCountableTopology}(U) \text{ for all } U \in \mathrm{Opens}(\alpha).$$$

Lean4

instance instSecondCountableOpens [SecondCountableTopology α] (U : Opens α) : SecondCountableTopology U :=
  inferInstanceAs (SecondCountableTopology U.1)

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