congr — Mathlib

English

If p holds eventually and p x is equivalent to q x eventually, then q x holds eventually.

Русский

Если p выполняется часто, и p x эквивалентно q x часто, то q x выполняется часто.

LaTeX

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

Lean4

theorem congr {f : Filter α} {p q : α → Prop} (h' : ∀ᶠ x in f, p x) (h : ∀ᶠ x in f, p x ↔ q x) : ∀ᶠ x in f, q x :=
  h'.mp (h.mono fun _ hx => hx.mp)

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