of_continuous_surjective — Mathlib

English

A continuous image of a Lindelöf space under a surjective map is Lindelöf.

Русский

Пусть f : X → Y непрерывно, сюръективно, и X Линдельфово; тогда Y Линдельфово.

LaTeX

$$$\\text{If } f:X\\to Y\\text{ is continuous and surjective, and } X\\text{ is Lindelöf, then } Y\\text{ is Lindelöf}.$$$

Lean4

/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain. -/
theorem of_continuous_surjective {f : X → Y} [LindelofSpace X] (hf : Continuous f) (hsur : Function.Surjective f) :
    LindelofSpace Y where
  isLindelof_univ := by
    rw [← Set.image_univ_of_surjective hsur]
    exact IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf

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