comap_cocompact — Mathlib

English

For a homeomorphism h, comap h (cocompact Y) = cocompact X.

Русский

Для гомеоморфизма h выполняется: предобраз комаппактной части пространства Y равен кокомпактной части пространства X.

LaTeX

$$$comap\\, h\\, (cocompact\\, Y) = cocompact\\, X$$$

Lean4

@[simp]
theorem comap_cocompact (h : X ≃ₜ Y) : comap h (cocompact Y) = cocompact X :=
  (comap_cocompact_le h.continuous).antisymm <|
    (hasBasis_cocompact.le_basis_iff (hasBasis_cocompact.comap h)).2 fun K hK =>
      ⟨h ⁻¹' K, h.isCompact_preimage.2 hK, Subset.rfl⟩

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