imp_left — Mathlib

English

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

Русский

Если для всех x выполняется p(x) → q(x) и для всех x выполняется q(x) → r(x), то для всех x выполняется p(x) → r(x).

LaTeX

$$$\bigl(\forall x\,(p(x)\to q(x))\bigr)\to\bigl(\forall x\,(q(x)\to r(x))\bigr)\to\forall x\,(p(x)\to r(x))$$$

Lean4

theorem imp_left (H : ∀ x, p x → q x) (h₁ : ∀ x, q x → r x) (x) (h : p x) : r x :=
  h₁ _ <| H _ h

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