isClosed_image — Mathlib

English

Let h: X ≃ₜ Y be a homeomorphism. For every subset s of X, the image h''s is closed in Y if and only if s is closed in X.

Русский

Пусть h: X ≃ₜ Y — гомеоморфизм. Для любого подмножества s ⊆ X образ h''s замкнут в Y тогда и только тогда, когда s замкнуто в X.

LaTeX

$$$\forall s \subseteq X, \ IsClosed(s) \iff IsClosed(h''s).$$$

Lean4

@[simp]
theorem isClosed_image (h : X ≃ₜ Y) {s : Set X} : IsClosed (h '' s) ↔ IsClosed s := by
  rw [← preimage_symm, isClosed_preimage]

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