English
A variant formulation: if for every indexed family of closed sets the finite sub-intersection avoids s whenever the whole intersection avoids s, then s is compact.
Русский
Вариант формулировки: если для каждой индексированной совокупности замкнутых множеств конечная общая часть пересечения с 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 \\, (u\\text{ finite}) ,\\; (s \\cap \\bigcap_{i\\in u} t_i) = \\emptyset\\Big) \\Rightarrow IsCompact s$$
Lean4
/-- A set `s` is compact if for every family of closed sets whose intersection avoids `s`,
there exists a finite subfamily whose intersection avoids `s`. -/
theorem isCompact_of_finite_subfamily_closed
(h :
∀ {ι : Type u} (t : ι → Set X),
(∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅) :
IsCompact s :=
isCompact_of_finite_subcover fun U hUo hsU =>
by
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
refine ⟨t, ?_⟩
rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
