imp_left — Mathlib

English

If there exists x with p x and r x, and for all x, p x implies q x, then there exists x with q x and r x.

Русский

Если существует x such that p(x) и r(x), и для всех x предикат p(x) ⇒ q(x), то существует x such that q(x) и r(x).

LaTeX

$$$\bigl(\exists x\,\exists h\,(p(x)\,\&\, P(x,h))\,\&\, r(x)\bigr)\to \exists x\,\exists h\,(q(x,h)\,\&\, r(x))\quad\text{при }(\forall x\,p(x)\to q(x)).$$$

Lean4

theorem imp_left (H : ∀ x, p x → q x) : (∃ (x : _) (_ : p x), r x) → ∃ (x : _) (_ : q x), r x
  | ⟨x, hp, hr⟩ => ⟨x, H _ hp, hr⟩

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