English
A version of shrinking lemma ensuring a new closed cover with each closed set contained in the corresponding open set.
Русский
Версия леммы о схлопывании, обеспечивающая новое закрытое покрытие, где каждое закрытое множество лежит внутри соответствующего открытого множества.
LaTeX
$$$$\exists v: ι→Set X, iUnion v \subseteq \bigcup_i u_i, \forall i, IsClosed(v_i) \wedge 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 closed cover so that each of the new closed sets is contained in the corresponding
original open set. See also `exists_iUnion_eq_closure_subset` for a stronger statement. -/
theorem exists_iUnion_eq_closed_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, IsClosed (v i)) ∧ ∀ i, v i ⊆ u i :=
let ⟨v, vU, hv⟩ := exists_subset_iUnion_closed_subset isClosed_univ uo (fun x _ => uf x) uU.ge
⟨v, univ_subset_iff.1 vU, hv⟩
