of_denseRange — Mathlib

English

If there exists a dense range map u: ι → α from a countable index set ι, then α is separable.

Русский

Если существует отображение u: ι → α с плотным диапазоном, где ι счётно, то α сепарабельно.

LaTeX

$$$[Countable \\ ι] (u: ι \\to α)\\; DenseRange(u) \\Rightarrow \\text{SeparableSpace}(α)$$$

Lean4

/-- If `f` has a dense range and its domain is countable, then its codomain is a separable space.
See also `DenseRange.separableSpace`. -/
theorem of_denseRange {ι : Sort _} [Countable ι] (u : ι → α) (hu : DenseRange u) : SeparableSpace α :=
  ⟨⟨range u, countable_range u, hu⟩⟩

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