eventually_congr — Mathlib

English

If the predicate p is eventually equivalent to q, then eventually p holds if and only if eventually q holds.

Русский

Если p и q совпадают поздно (в пределе), то верно: p выполняется поздно тогда и только тогда, когда q выполняется поздно.

LaTeX

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

Lean4

theorem eventually_congr {f : Filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p x ↔ q x) :
    (∀ᶠ x in f, p x) ↔ ∀ᶠ x in f, q x :=
  ⟨fun hp => hp.congr h, fun hq => hq.congr <| by simpa only [Iff.comm] using h⟩

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