isClosed_preimage — Mathlib

English

Let h: X ≃ₜ Y be a homeomorphism between topological spaces. Then for every subset s of Y, the preimage h^{-1}(s) is closed in X if and only if s is closed in Y.

Русский

Пусть h: X ≃ₜ Y — гомеоморфизм между топологическими пространствами. Тогда для любого подмножества s ⊆ Y прообраз h^{-1}(s) замкнуто в X тогда и только тогда, когда s замкнуто в Y.

LaTeX

$$$\text{If } h: X \to Y \text{ is a homeomorphism and } s \subseteq Y, \quad \mathrm{IsClosed}(h^{-1}(s)) \iff \mathrm{IsClosed}(s).$$$

Lean4

@[simp]
theorem isClosed_preimage (h : X ≃ₜ Y) {s : Set Y} : IsClosed (h ⁻¹' s) ↔ IsClosed s := by
  simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

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