English
In a normal space, a shrinked cover can be chosen so that the union is the whole space and closures stay inside.
Русский
Можно выбрать сжатое покрытие так, чтобы их объединение было всем пространством, а замыкания оставались внутри оригинальных множеств.
LaTeX
$$$$\exists v:\iota\to Set X, iUnion v = univ \cap \text{IsOpen}(v_i)\; \&\; closure(v_i)\subseteq u_i.$$$$
Lean4
/-- Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk"
to a new open cover so that the closure of each new open set is contained in the corresponding
original open set. -/
theorem exists_iUnion_eq_closure_subset (uo : ∀ i, IsOpen (u i)) (uf : ∀ x, {i | x ∈ u i}.Finite)
(uU : ⋃ i, u i = univ) : ∃ v : ι → Set X, iUnion v = univ ∧ (∀ i, IsOpen (v i)) ∧ ∀ i, closure (v i) ⊆ u i :=
let ⟨v, vU, hv⟩ := exists_subset_iUnion_closure_subset isClosed_univ uo (fun x _ => uf x) uU.ge
⟨v, univ_subset_iff.1 vU, hv⟩
