eventually_or — Mathlib

English

An ultrafilter satisfies a disjunction p ∨ q eventually if and only if either p eventually or q eventually.

Русский

Ульрафильтр удовлетворяет дизъюнкцию p ∨ q в конце концов тогда, когда либо p, либо q выполняются в конце концов.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {p q \\\\colon \\\\alpha \\\\to \\\\mathrm{Prop}}, \\\\; (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, p(x) \\\\lor q(x)) \\\\Leftrightarrow (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, p(x)) \\\\lor (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, q(x))$$$

Lean4

theorem eventually_or : (∀ᶠ x in f, p x ∨ q x) ↔ (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, q x :=
  union_mem_iff

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