English
In a normal space, a shrinking lemma gives a cover of the whole space by sets whose closures stay within the given open cover.
Русский
В нормальном пространстве лемма об уменьшении обеспечивает покрытие всего пространства множестами, closure которых вложено в исходные открытые множества.
LaTeX
$$$$\exists v: ι→Set X, iUnion v = univ ∧ ∀ i, IsOpen(v_i) ∧ ∀ i, closure(v_i) ⊆ 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_subset_iUnion_closure_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, IsOpen (v i)) ∧ ∀ i, closure (v i) ⊆ u i :=
by
haveI : Nonempty (PartialRefinement u s ⊤) := ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩
have : ∀ c : Set (PartialRefinement u s ⊤), IsChain (· ≤ ·) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub := fun c hc ne =>
⟨.chainSup c hc ne uf us, fun v hv => PartialRefinement.le_chainSup _ _ _ _ hv⟩
rcases zorn_le_nonempty this with ⟨v, hv⟩
suffices ∀ i, i ∈ v.carrier from ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩
refine fun i ↦ by_contra fun hi ↦ ?_
rcases v.exists_gt hs i hi with ⟨v', hlt⟩
exact hv.not_lt hlt
