English
A locally compact sigma-compact Hausdorff space is paracompact.
Русский
Локально компактное σ-компактное хаусдорфово пространство является паракомпактным.
LaTeX
$$$ \\text{ParacompactSpace } X $$$
Lean4
/-- A locally compact sigma compact Hausdorff space is paracompact. See also
`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` for a more precise statement. -/
instance (priority := 100) paracompact_of_locallyCompact_sigmaCompact [WeaklyLocallyCompactSpace X]
[SigmaCompactSpace X] [T2Space X] : ParacompactSpace X :=
by
refine ⟨fun α s ho hc ↦ ?_⟩
choose i hi using iUnion_eq_univ_iff.1 hc
have : ∀ x : X, (𝓝 x).HasBasis (fun t : Set X ↦ (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id := fun x : X ↦
(nhds_basis_opens x).restrict_subset (IsOpen.mem_nhds (ho (i x)) (hi x))
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis this with ⟨β, c, t, hto, htc, htf⟩
exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩
