separableSpace — Mathlib

English

If f is an embedding into a second countable space β, then α is a separable space.

Русский

Если f — вложение в пространство β с второй счётностью, то пространство α сепарабельно.

LaTeX

$$$IsEmbedding f \rightarrow SecondCountableTopology \beta \rightarrow TopologicalSpace.SeparableSpace \alpha$$$

Lean4

protected theorem separableSpace [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) :
    TopologicalSpace.SeparableSpace α := by
  have := hf.secondCountableTopology
  exact SecondCountableTopology.to_separableSpace

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