English
A subset s is compact iff every ultrafilter on X that concentrates on s has a point of s as a cluster point; equivalently, for every ultrafilter f, if f ≤ 𝓟 s then there exists x ∈ s with f ≤ 𝓝 x.
Русский
Подмножество s компактно тогда и только тогда, когда каждый ультрафильтр на X, сосредоточенный на s, имеет кластерную точку в s; эквивалентно: для любого ультрафильтра f, если f ≤ 𝓟 s, то существует x ∈ s такой, что f ≤ 𝓝 x.
LaTeX
$$$IsCompact(s) \iff \forall f:\! Ultrafilter X, \ \, \uparrow f \le 𝓟 s \rightarrow \exists x \in s, \uparrow f \le 𝓝 x$$$
Lean4
theorem isCompact_iff_ultrafilter_le_nhds : IsCompact s ↔ ∀ f : Ultrafilter X, ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x :=
by
refine (forall_neBot_le_iff ?_).trans ?_
· rintro f g hle ⟨x, hxs, hxf⟩
exact ⟨x, hxs, hxf.mono hle⟩
· simp only [Ultrafilter.clusterPt_iff]
