mp — Mathlib · SciLib

English

Let f be a filter on α, and let p, q : α → Prop. If p holds eventually and p implies q holds eventually, then q holds eventually.

Русский

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

LaTeX

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

Lean4

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

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