isLindelof_preimage — Mathlib

English

The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.

Русский

При закрытом вложении предобраз Линдельфового множества также Линдельфово.

LaTeX

$$${f:X→Y}\ (hf: IsClosedEmbedding f) {K:Set Y}\ (hK:IsLindelof K) : IsLindelof (preimage f K)$$$

Lean4

/-- The preimage of a Lindelöf set under a closed embedding is a Lindelöf set. -/
theorem isLindelof_preimage {f : X → Y} (hf : IsClosedEmbedding f) {K : Set Y} (hK : IsLindelof K) :
    IsLindelof (f ⁻¹' K) :=
  hf.isInducing.isLindelof_preimage (hf.isClosed_range) hK

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