eventually_or_distrib_right — Mathlib

English

The eventual truth of p x ∨ q is equivalent to the truth of p x eventually or q.

Русский

Истинность p x ∨ q эквивалентна тому, что p x выполняется часто или q истинно.

LaTeX

$$$ (\forall^\infty x \in f, p x \lor q) \leftrightarrow (\forall^\infty x \in f, p x) \lor q $$$

Lean4

@[simp]
theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q := by simp only [@or_comm _ q, eventually_or_distrib_left]

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