eventually_imp_distrib_right — Mathlib

English

The universal implication over p within a filter is equivalent to (∃ᶠ x, p x) → q.

Русский

Универсальная импликация над p внутри фильтра эквивалентна (∃ᶠ x, p x) → q.

LaTeX

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

Lean4

theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q := by
  simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

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