isClosed_iff_image_isClosed — Mathlib

English

For a closed embedding f, a set s is closed iff its image f''s is closed.

Русский

Для замкнутого вложения f множество s замкнуто тогда и только тогда, когда образ f''s замкнут.

LaTeX

$$$\mathrm{IsClosedEmbedding}(f) \rightarrow \forall s, \mathrm{IsClosed}(s) \leftrightarrow \mathrm{IsClosed}(f''s)$$$

Lean4

theorem isClosed_iff_image_isClosed (hf : IsClosedEmbedding f) {s : Set X} : IsClosed s ↔ IsClosed (f '' s) :=
  ⟨hf.isClosedMap s, fun h => by
    rw [← preimage_image_eq s hf.injective]
    exact h.preimage hf.continuous⟩

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