image — Mathlib

English

If s is σ-compact and f is continuous, f(s) is σ-compact.

Русский

Если s σ-компактно и f непрерывна, то f(s) σ-компактно.

LaTeX

$$$IsSigmaCompact(s) \\\\rightarrow Continuous f \\\\rightarrow IsSigmaCompact(f''s)$$$

Lean4

/-- If `s` is σ-compact and `f` continuous, `f(s)` is σ-compact. -/
theorem image {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsSigmaCompact s) : IsSigmaCompact (f '' s) :=
  hs.image_of_continuousOn hf.continuousOn

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