mono — Mathlib

English

Let p and q be predicates on α and f a filter on α. If p holds eventually and p x implies q x for all x, then q holds eventually.

Русский

Пусть p и q — предикаты на α, а f — фильтр на α. Если p выполняется часто и p x ⇒ q x для всех x, тогда q выполняется часто.

LaTeX

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

Lean4

theorem mono {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) (hq : ∀ x, p x → q x) : ∀ᶠ x in f, q x :=
  hp.mp (Eventually.of_forall hq)

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