isSigmaCompact_preimage — Mathlib

English

If h is a homeomorphism, a subset s ⊆ Y is σ-compact iff its preimage h^{-1}(s) ⊆ X is σ-compact.

Русский

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

LaTeX

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

Lean4

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

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