imp — Mathlib

English

If for all a,b, p a b implies q a b, then from existence of a,b with p a b, one can conclude existence of a,b with q a b.

Русский

Если для всех a,b верно p(a,b)→q(a,b), то из существования некоторых a,b с p(a,b) следует существование таких a,b с q(a,b).

LaTeX

$$$(\\\\exists a\\\\,\\\\exists b, p(a,b))\\\\rightarrow\\\\exists a\\\\,\\\\exists b, q(a,b)$$$

Lean4

theorem imp {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) : (∃ a b, p a b) → ∃ a b, q a b :=
  Exists.imp fun a ↦ Exists.imp <| h a

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