separableSpace — Mathlib

English

If α is separable and f: α → β is a quotient map, then β is separable.

Русский

Если α разделимо и f: α → β — плоская карта (окончательный отображатель), то β разделимо.

LaTeX

$$$[SeparableSpace \\;\\alpha] \\land \\text{IsQuotientMap}(f) \\Rightarrow \\text{SeparableSpace}(\\beta)$$$

Lean4

theorem _root_.Topology.IsQuotientMap.separableSpace [SeparableSpace α] [TopologicalSpace β] {f : α → β}
    (hf : IsQuotientMap f) : SeparableSpace β :=
  hf.surjective.denseRange.separableSpace hf.continuous

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