comap_coclosedCompact — Mathlib

English

Two spaces are locally compact with respect to a homeomorphism: LocallyCompactSpace X iff LocallyCompactSpace Y.

Русский

Два пространства локально компактны взаимно через гомеоморфизм: LocallyCompactSpace X эквивалично LocallyCompactSpace Y.

LaTeX

$$$LocallyCompactSpace X \\iff LocallyCompactSpace Y$$$

Lean4

@[simp]
theorem comap_coclosedCompact (h : X ≃ₜ Y) : comap h (coclosedCompact Y) = coclosedCompact X :=
  (hasBasis_coclosedCompact.comap h).eq_of_same_basis <| by
    simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective

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