secondCountableTopology — Mathlib

English

If α has a second-countable topology, then any subspace s ⊆ α, with the subspace topology, is also second-countable.

Русский

Если у пространства α есть вторая счетность, то любое подпространство s⊆α с подпоплотной топологией тоже имеет вторую счетность.

LaTeX

$$$\forall s \subseteq \alpha,\; SecondCountableTopology(s)$$$

Lean4

instance secondCountableTopology (s : Set α) [SecondCountableTopology α] : SecondCountableTopology s :=
  secondCountableTopology_induced s α (↑)

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