exists_ultrafilter_of_finite_inter_nonempty

English

If the complement of a set is finite, then the set lies in the hyperfilter.

Русский

Если комплемент множества конечен, то множество принадлежит гиперфильтру.

LaTeX

$$$s^{c} \text{ finite } \Rightarrow s \in hyperfilter(\alpha)$$

Lean4

theorem exists_ultrafilter_of_finite_inter_nonempty (S : Set (Set α))
    (cond : ∀ T : Finset (Set α), (↑T : Set (Set α)) ⊆ S → (⋂₀ (↑T : Set (Set α))).Nonempty) :
    ∃ F : Ultrafilter α, S ⊆ F.sets :=
  haveI : NeBot (generate S) :=
    generate_neBot_iff.2 fun _ hts ht => ht.coe_toFinset ▸ cond ht.toFinset (ht.coe_toFinset.symm ▸ hts)
  ⟨of (generate S), fun _ ht => (of_le <| generate S) <| GenerateSets.basic ht⟩

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