English
If α is separable and f: α → β is a continuous map with dense range, then β is separable.
Русский
Если пространство α разделимо и имеется непрерывное отображение f: α → β с плотным диапазоном, то β также разделимо.
LaTeX
$$$[SeparableSpace\\;\\alpha] \\land \\text{Continuous}(f) \\land \\text{DenseRange}(f) \\Rightarrow \\text{SeparableSpace}(\\beta)$$$
Lean4
/-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
a separable space as well. E.g., the completion of a separable uniform space is separable. -/
protected theorem _root_.DenseRange.separableSpace [SeparableSpace α] [TopologicalSpace β] {f : α → β}
(h : DenseRange f) (h' : Continuous f) : SeparableSpace β :=
let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α
⟨⟨f '' s, Countable.image s_cnt f, h.dense_image h' s_dense⟩⟩
