hyperfilter_le_cofinite — Mathlib

English

For a family S of sets, if every finite subfamily has nonempty intersection, there exists an ultrafilter F on α containing S.

Русский

Для семейства S множеств, если пересечение любой конечной подсемьи не пусто, существует ульрафильтр F на α, содержащий S.

LaTeX

$$$\bigl(\forall \mathcal{T}\subseteq S,\mathcal{T}\text{ finite} \Rightarrow \bigcap \mathcal{T} \neq \emptyset\bigr) \Rightarrow \exists F: Ultrafilter\ α, S \subseteq F.sets$$

Lean4

theorem hyperfilter_le_cofinite : ↑(hyperfilter α) ≤ @cofinite α :=
  Ultrafilter.of_le cofinite

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