English
In a paracompact space, a closed set S covered by open sets u_i has a locally finite refinement v_i with v_i open, v_i ⊆ u_i, and S ⊆ ⋃ i v_i.
Русский
В паракомпактном пространстве замкнутое множество S, покрытое открытыми множествами u_i, имеет локально конечное точное разбиение v_i вершинами, причём v_i открыты и вложены в u_i, а S ⊆ ⋃ i v_i.
LaTeX
$$$ \\exists v : ι \\to Set X, \\left( \\forall i, IsOpen(v(i)) \\right) \\land (S \\subseteq \\bigcup_i v(i)) \\land LocallyFinite v \\land \\forall i, v(i) \\subseteq u(i). $$$
Lean4
/-- In a paracompact space, every open covering of a closed set admits a locally finite refinement
indexed by the same type. -/
theorem precise_refinement_set [ParacompactSpace X] {s : Set X} (hs : IsClosed s) (u : ι → Set X)
(uo : ∀ i, IsOpen (u i)) (us : s ⊆ ⋃ i, u i) :
∃ v : ι → Set X, (∀ i, IsOpen (v i)) ∧ (s ⊆ ⋃ i, v i) ∧ LocallyFinite v ∧ ∀ i, v i ⊆ u i :=
by
have uc : (iUnion fun i => Option.elim' sᶜ u i) = univ :=
by
apply Subset.antisymm (subset_univ _)
· simp_rw [← compl_union_self s, Option.elim', iUnion_option]
apply union_subset_union_right sᶜ us
rcases precise_refinement (Option.elim' sᶜ u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩) uc with
⟨v, vo, vc, vf, vu⟩
refine ⟨v ∘ some, fun i ↦ vo _, ?_, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
· simp only [iUnion_option, ← compl_subset_iff_union] at vc
exact Subset.trans (subset_compl_comm.1 <| vu Option.none) vc
