frequently_imp_distrib_right — Mathlib

English

Equivalently, (∃ᶠ x, p x → q) is equivalent to (∀ᶠ x, p x) → q.

Русский

Эквивалентно, (∃ᶠ x, p x → q) эквивалентно (∀ᶠ x, p x) → q.

LaTeX

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

Lean4

theorem frequently_imp_distrib_right {f : Filter α} [NeBot f] {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x → q) ↔ (∀ᶠ x in f, p x) → q := by simp only [frequently_imp_distrib, frequently_const]

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