isSigmaCompact_range — Mathlib

English

If X is σ-compact and f is continuous, then the range of f is σ-compact.

Русский

Если X σ-компактно и f непрерывна, то множество образа f имеет σ-компактность.

LaTeX

$$$Continuous f \\rightarrow (SigmaCompactSpace X \\Rightarrow IsSigmaCompact (range f))$$$

Lean4

/-- If `X` is σ-compact, `im f` is σ-compact. -/
theorem isSigmaCompact_range {f : X → Y} (hf : Continuous f) [SigmaCompactSpace X] : IsSigmaCompact (range f) :=
  image_univ ▸ isSigmaCompact_univ.image hf

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