isCompact_preimage — Mathlib

English

Let h be a homeomorphism between X and Y. A subset s of Y is compact if and only if its preimage under h is compact in X.

Русский

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

LaTeX

$$$IsCompact(h^{-1}(s)) \\iff IsCompact(s)$$$

Lean4

/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is. -/
@[simp]
theorem isCompact_preimage {s : Set Y} (h : X ≃ₜ Y) : IsCompact (h ⁻¹' s) ↔ IsCompact s := by rw [← image_symm];
  exact h.symm.isCompact_image

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