isSeparable_image — Mathlib

English

If a map is continuous on a separable set, then its image of that set is separable.

Русский

Если отображение непрерывно на сепарабельном множества, изображение этого множества сепарабельно.

LaTeX

$$$\\text{ContinuousOn}(f,s) \\land \\text{IsSeparable}(s) \\Rightarrow \\text{IsSeparable}(f''s)$$$

Lean4

/-- If a map is continuous on a separable set `s`, then the image of `s` is also separable. -/
theorem isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ContinuousOn f s) (hs : IsSeparable s) :
    IsSeparable (f '' s) := by
  rw [image_eq_range, ← image_univ]
  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

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