frequently_or_distrib — Mathlib

English

Frequently distributes over Or: ∃ᶠ x, p x ∨ q x is equivalent to (∃ᶠ x, p x) ∨ (∃ᶠ x, q x).

Русский

Частотность распространяется на или: ∃ᶠ x, p x ∨ q x эквивалентно (∃ᶠ x, p x) ∨ (∃ᶠ x, q x).

LaTeX

$$$ (\exists^\! x, p(x) \lor q(x)) \iff (\exists^\! x, p(x)) \lor (\exists^\! x, q(x)) $$$

Lean4

@[simp]
theorem frequently_or_distrib {f : Filter α} {p q : α → Prop} :
    (∃ᶠ x in f, p x ∨ q x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in f, q x := by
  simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

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