frequently_congr — Mathlib

English

If p x is frequently equivalent to q x, then p frequently holds if and only if q frequently holds.

Русский

Если p x часто эквивалентно q x, то 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 frequently_congr {p q : α → Prop} {f : Filter α} (h : ∀ᶠ x in f, p x ↔ q x) :
    (∃ᶠ x in f, p x) ↔ ∃ᶠ x in f, q x :=
  ⟨fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mp), fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mpr)⟩

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