isSeparable_range — Mathlib

English

The range of a continuous map from a separable space is separable.

Русский

Образ непрерывного отображения из сепарабельного пространства сепарабельно.

LaTeX

$$$IsSeparable(\operatorname{range} f)$, given [TopologicalSpace β] [SeparableSpace α] and f Continuous$$

Lean4

theorem isSeparable_range [TopologicalSpace β] [SeparableSpace α] {f : α → β} (hf : Continuous f) :
    IsSeparable (range f) :=
  image_univ (f := f) ▸ (isSeparable_univ_iff.2 ‹_›).image hf

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