mem_or_compl_mem — Mathlib

English

For any ultrafilter f and set s, either s ∈ f or s^c ∈ f.

Русский

Для любого ульрафильтра f и множества s верно: либо s ∈ f, либо s^c ∈ f.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {s \\\\subseteq \\\\alpha}, \\\\; s \\\\in f \\\\lor s^c \\\\in f$$$

Lean4

theorem mem_or_compl_mem (f : Ultrafilter α) (s : Set α) : s ∈ f ∨ sᶜ ∈ f :=
  or_iff_not_imp_left.2 compl_mem_iff_notMem.2

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