paracompactSpace — Mathlib

English

If Y is a paracompact space and e: X → Y is a closed embedding, then X is a paracompact space.

Русский

Если Y — паракомпактное пространство, и e: X → Y является закрытым вложением, то X тоже паракомпактно.

LaTeX

$$$ [\operatorname{ParacompactSpace} Y] \wedge \text{IsClosedEmbedding}(e) \Rightarrow \operatorname{ParacompactSpace}(X). $$$

Lean4

theorem paracompactSpace [ParacompactSpace Y] {e : X → Y} (he : IsClosedEmbedding e) : ParacompactSpace X where
  locallyFinite_refinement α s ho
    hu := by
    choose U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)
    simp only [← hU] at hu ⊢
    have heU : range e ⊆ ⋃ i, U i := by simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu
    rcases precise_refinement_set he.isClosed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩
    refine
      ⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_, hVf.preimage_continuous he.continuous,
        fun a ↦ ⟨a, preimage_mono (hVU a)⟩⟩
    simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using heV

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