English
A variant of shrinking lemma producing a new closed cover where each closed set is contained in the corresponding original open set.
Русский
Вариант леммы об уменьшении, дающий новое закрытое покрытие, где каждое новое закрытое множество входит в соответствующее исходное открытое множество.
LaTeX
$$$$\exists v: ι→Set X, s\subseteq iUnion v \wedge \forall i, IsClosed(v_i) \wedge \forall i, 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 new closed set is contained in the corresponding
original open set. See also `exists_subset_iUnion_closure_subset` for a stronger statement. -/
theorem exists_subset_iUnion_closed_subset (hs : IsClosed s) (uo : ∀ i, IsOpen (u i))
(uf : ∀ x ∈ s, {i | x ∈ u i}.Finite) (us : s ⊆ ⋃ i, u i) :
∃ v : ι → Set X, s ⊆ iUnion v ∧ (∀ i, IsClosed (v i)) ∧ ∀ i, v i ⊆ u i :=
let ⟨v, hsv, _, hv⟩ := exists_subset_iUnion_closure_subset hs uo uf us
⟨fun i => closure (v i), Subset.trans hsv (iUnion_mono fun _ => subset_closure), fun _ => isClosed_closure, hv⟩
