imp_right — Mathlib

English

Let α be a type. Suppose for all x and h with p x, P x h implies Q x h. If there exists x and h with P x h, then there exists x and h with Q x h.

Русский

Пусть α — множество, p — предикат на x, P x h → Q x h для всех x и h с p x. Если существует пара (x, h) такая, что P x h, то существует пара (x, h) такая, что Q x h.

LaTeX

$$$\bigl(\forall x,h\,(P(x,h)\to Q(x,h))\bigr)\to\bigl((\exists x\,\exists h\, P(x,h))\to (\exists x\,\exists h\, Q(x,h))\bigr)$$$

Lean4

theorem imp_right (H : ∀ x h, P x h → Q x h) : (∃ x h, P x h) → ∃ x h, Q x h
  | ⟨_, _, h'⟩ => ⟨_, _, H _ _ h'⟩

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