English
In a locally compact T2 space, from a shrinking lemma for closures one obtains a refinement by taking closures, preserving cover properties and compactness of closures.
Русский
В локально компактном T2-пространстве из леммы о сжатии для замыканий получается уточнение через замыкания, сохраняя покрытие и компактность замыканий.
LaTeX
$$$$\exists v : ι → Set X, \; s ⊆ iUnion v \wedge \forall i, IsClosed(closure(v_i)) \wedge \forall i, closure(v_i) ⊆ u_i, \forall i, IsCompact(closure(v_i)).$$$$
Lean4
/-- **Shrinking lemma**. A point-finite open cover of a compact subset of a locally compact T2 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_t2space` for a stronger statement.
-/
theorem exists_subset_iUnion_compact_subset_t2space (hs : IsCompact 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) ∧ ∀ i, IsCompact (v i) :=
by
let ⟨v, hsv, _, hv⟩ := exists_subset_iUnion_closure_subset_t2space hs uo uf us
use fun i => closure (v i)
refine ⟨?_, ?_, hv⟩
· exact Subset.trans hsv (iUnion_mono fun _ => subset_closure)
· simp only [isClosed_closure, implies_true]
