mp — Mathlib · SciLib

English

If p holds frequently and p implies q holds frequently, then q holds frequently.

Русский

Если p выполняется часто и p ⇒ q выполняется часто, тогда q выполняется часто.

LaTeX

$$$ (\text{Frequently} (p)) \rightarrow (\text{Eventually} (p \rightarrow q)) \rightarrow \text{Frequently} (q) $$$

Lean4

theorem mp {p q : α → Prop} {f : Filter α} (h : ∃ᶠ x in f, p x) (hpq : ∀ᶠ x in f, p x → q x) : ∃ᶠ x in f, q x :=
  mt (fun hq => hq.mp <| hpq.mono fun _ => mt) h

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