isCompact_image — Mathlib

English

If h: X ≃ₜ Y is a homeomorphism, then h''s is compact iff s is compact.

Русский

Если h: X ≃ₜ Y — гомеоморфизм, то образ s под h компактен тогда и только тогда, когда s компактен.

LaTeX

$$$ \\forall s \\subset X,\\; IsCompact (h''s) \\iff IsCompact s $$$

Lean4

/-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is. -/
@[simp]
theorem isCompact_image {s : Set X} (h : X ≃ₜ Y) : IsCompact (h '' s) ↔ IsCompact s :=
  h.isEmbedding.isCompact_iff.symm

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