frequently_or_distrib_left — Mathlib

English

With NeBot f, a single true proposition p yields either p or a frequent q: (∃ᶠ x, p ∨ q x) ↔ p ∨ ∃ᶠ x, q x.

Русский

При NeBot f однажды истинное p приводит либо к p, либо к частой q: (∃ᶠ x, p ∨ q x) ⇔ p ∨ ∃ᶠ x, q x.

LaTeX

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

Lean4

theorem frequently_or_distrib_left {f : Filter α} [NeBot f] {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p ∨ q x) ↔ p ∨ ∃ᶠ x in f, q x := by simp

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