isCompact_iff_ultrafilter_le_nhds'

English

A compact set s is characterized by: for every ultrafilter f, f ≤ nhdsSet s iff ∃ x ∈ s with f ≤ nhds x.

Русский

Компактность множества s эквивалентна тому, что для любого ультрафильтра f выполняется f ≤ nhdsSet s тогда и только тогда, когда существует x ∈ s такой, что f ≤ nhds x.

LaTeX

$$$IsCompact(s) \iff \forall f : Ultrafilter X, s \in f \rightarrow \exists x \in s, \uparrow f \le 𝓝 x$$$

Lean4

theorem isCompact_iff_ultrafilter_le_nhds' : IsCompact s ↔ ∀ f : Ultrafilter X, s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x := by
  simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff, Ultrafilter.mem_coe]

Похожие утверждения