English
The eventually-implication principle: p ⇒ q holds eventually if and only if p holds eventually implies q holds eventually.
Русский
Необходимость и достаточность импликации в пределе: если p x → q x держится в конечном виде, то из этого следует, что p держится часто тогда и только тогда, когда q держится часто.
LaTeX
$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {p q : \\\\alpha \\\\to \\\\mathrm{Prop}}, \\\\; (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, p(x) \\\\rightarrow q(x)) \\\\Leftrightarrow (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, p(x)) \\\\rightarrow (\\\\forall^{\\\\mathrm{ev}} x \\\\in f, q(x))$$$
Lean4
theorem eventually_imp : (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∀ᶠ x in f, q x := by
simp only [imp_iff_not_or, eventually_or, eventually_not]
