secondCountableTopology — Mathlib

English

Let X be a pseudo-metrizable space; if s ⊆ X is separable, then s has a second countable topology.

Русский

Пусть X псевдометризуемо; если s ⊆ X сепарабельно, то топология на s является второй счетной.

LaTeX

$$$[\text{PseudoMetrizableSpace } X] \Rightarrow [\text{SecondCountableTopology } s]$ with separable subset s.$$

Lean4

theorem secondCountableTopology [PseudoMetrizableSpace X] {s : Set X} (hs : IsSeparable s) :
    SecondCountableTopology s := by
  letI := pseudoMetrizableSpacePseudoMetric X
  have := hs.separableSpace
  exact UniformSpace.secondCountable_of_separable s

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