em — Mathlib · SciLib

English

For any ultrafilter f and predicate p, either p holds frequently or its negation holds frequently.

Русский

Для любого ульрафильтра f и предиката p либо p выполняется часто, либо его отрицание выполняется часто.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {p \\\\colon \\\\alpha \\\\to \\\\mathrm{Prop}}, \\\\; \\\\exists^{\\\\mathrm{em}} x \\\\in f\, p(x) \\\\lor \\\\exists^{\\\\mathrm{em}} x \\\\in f\, \\neg p(x)$$$

Lean4

protected theorem em (f : Ultrafilter α) (p : α → Prop) : (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, ¬p x :=
  f.mem_or_compl_mem {x | p x}

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