English
For any open directed cover of a compact set, there exists a single index i such that the set is contained in U_i.
Русский
Для любого открытого направленного покрытия компактного множества существует один индекс i, такой что множество s ⊆ U_i.
LaTeX
$$$IsCompact(s) \rightarrow \forall U:\ \iota \to Set X,\ (\forall i, IsOpen(U(i))) \rightarrow s \subseteq \bigcup_i U(i) \rightarrow Directed (\subseteq) U \rightarrow \exists i, s \subseteq U(i)$$$
Lean4
/-- For every open directed cover of a compact set, there exists a single element of the
cover which itself includes the set. -/
theorem elim_directed_cover {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
(hsU : s ⊆ ⋃ i, U i) (hdU : Directed (· ⊆ ·) U) : ∃ i, s ⊆ U i :=
hι.elim fun i₀ =>
IsCompact.induction_on hs ⟨i₀, empty_subset _⟩ (fun _ _ hs ⟨i, hi⟩ => ⟨i, hs.trans hi⟩)
(fun _ _ ⟨i, hi⟩ ⟨j, hj⟩ =>
let ⟨k, hki, hkj⟩ := hdU i j
⟨k, union_subset (Subset.trans hi hki) (Subset.trans hj hkj)⟩)
fun _x hx =>
let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
⟨U i, mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds (hUo i) hi), i, Subset.refl _⟩
