paracompact_of_compact — Mathlib

English

A compact space is paracompact.

Русский

Компактное пространство — паракомпактно.

LaTeX

$$$ \\text{ParacompactSpace } X \\text{ при } [CompactSpace X] $$$

Lean4

/-- A compact space is paracompact. -/
instance (priority := 100) paracompact_of_compact [CompactSpace X] : ParacompactSpace X := by
  -- the proof is trivial: we choose a finite subcover using compactness, and use it

  refine ⟨fun ι s ho hu ↦ ?_⟩
  rcases isCompact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩
  refine ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _, fun t ↦ ⟨t, Subset.rfl⟩⟩
  simpa only [iUnion_coe_set, ← univ_subset_iff]

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