eventually_imp_distrib_left — Mathlib

English

The eventual truth of p → q is equivalent to p implies that q holds eventually.

Русский

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

LaTeX

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

Lean4

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

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