English
If for every indexed family of closed sets t_i the intersection with s being empty implies there exists a finite subfamily with empty intersection, then s is compact.
Русский
Если для любой семейство замкнутых множеств t_i пересечение с s даёт пустоту только если существует конечная подпоследовательность, дающая пустоту пересечения, то s компактно.
LaTeX
$$$\\Big(\\forall t: ι \\to Set X,\\; (\\forall i,\\; IsClosed (t_i)) \\rightarrow (s \\cap \\bigcap_i t_i) = \\emptyset \\rightarrow \\exists\\ u\\subseteq ι,\\; u\\text{ finite} \\land (s \\cap \\bigcap_{i\\in u} t_i) = \\emptyset\\Big) \\Rightarrow IsCompact s$$
Lean4
/-- A set `s` is compact if for every open cover of `s`, there exists a finite subcover. -/
theorem isCompact_of_finite_subcover
(h : ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i) :
IsCompact s := fun f hf hfs => by
contrapose! h
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall', (nhds_basis_opens _).disjoint_iff_left] at h
choose U hU hUf using h
refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
refine compl_notMem (le_principal_iff.1 hfs) ?_
refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_
rw [subset_compl_comm, compl_iInter₂]
simpa only [compl_compl]
-- TODO: reformulate using `Disjoint`
