English
A compact set has a finite subfamily of neighborhoods that covers it in nhdsSet sense.
Русский
Компактное множество имеет конечную подсемью окрестностей, покрывающую его в смысле nhdsSet.
LaTeX
$$$IsCompact(s) \rightarrow \forall U : (x:X) \to Set(s),\ (\forall x \in s, U x x.2 \text{ соответствует условию}) \rightarrow \exists t : Finset s, s \subseteq \bigcup_{x \in t} U x x.2$$$
Lean4
theorem elim_nhds_subcover_nhdsSet' (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x hx, U x hx ∈ 𝓝 x) :
∃ t : Finset s, (⋃ x ∈ t, U x.1 x.2) ∈ 𝓝ˢ s :=
by
rcases
hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior) fun x hx ↦
mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with
⟨t, hst⟩
refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩
refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)
exact mem_interior_iff_mem_nhds.1 hy
