paracompactSpace_iff — Mathlib

English

A homeomorphism preserves paracompactness: X is paracompact iff Y is paracompact whenever X ≃ₜ Y.

Русский

Гомеоморфизм сохраняет паракомпактность: X паракомпактно тогда и только тогда, когда Y паракомпактно, если X и Y гомеоморфны.

LaTeX

$$$ \\text{ParacompactSpace } X \\iff \\text{ParacompactSpace } Y \\quad \\text{for } e : X \\simeq_t Y $$$

Lean4

theorem paracompactSpace_iff (e : X ≃ₜ Y) : ParacompactSpace X ↔ ParacompactSpace Y :=
  ⟨fun _ ↦ e.symm.isClosedEmbedding.paracompactSpace, fun _ ↦ e.isClosedEmbedding.paracompactSpace⟩

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