English
A refinement can always be extended to a larger index with preserved compactness properties.
Русский
Всегда можно расширить уточнение до большего индекса, сохранив свойства компактности.
LaTeX
$$$$\exists v' : PartialRefinement u s (fun w => IsCompact (closure w)), v < v' \land IsCompact (closure (v' i)).$$$$
Lean4
/-- **Shrinking lemma** . A point-finite open cover of a compact subset of a `T2Space`
`LocallyCompactSpace` 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_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, IsOpen (v i)) ∧ (∀ i, closure (v i) ⊆ u i) ∧ (∀ i, IsCompact (closure (v i))) :=
by
haveI : Nonempty (PartialRefinement u s (fun w => IsCompact (closure w))) :=
⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩
have :
∀ c : Set (PartialRefinement u s (fun w => IsCompact (closure w))),
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), ?_⟩
· intro i
exact v.pred_of_mem (this i)
· intro i
by_contra! hi
rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩
exact hv.not_lt hlt
