image — Mathlib

English

If s is Lindelöf in X and f is continuous on X, then the image f[s] is Lindelöf in Y.

Русский

Если s — множество Линдельёфа в X и f: X → Y непрерывна, то образ f[s] является Линдельёфовым во Y.

LaTeX

$$$IsLindelof(s) \to (Continuous f) \to IsLindelof(f[ s ])$$$

Lean4

/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain. -/
theorem image {f : X → Y} (hs : IsLindelof s) (hf : Continuous f) : IsLindelof (f '' s) :=
  hs.image_of_continuousOn hf.continuousOn

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