elim — Mathlib

English

Let a, b ∈ ℤ with a ≤ b, and P a proposition. If for every natural n the implication a + n = b → P holds, then P holds.

Русский

Пусть a, b ∈ ℤ такие, что a ≤ b, и P — некоторое утверждение. Если для каждого натурального числа n верно: a + n = b → P, тогда P истинно.

LaTeX

$$$\forall a,b \in \mathbb{Z}, a \le b \to \forall P, (\forall n \in \mathbb{N}, a + n = b \to P) \to P.$$$

Lean4

theorem elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P :=
  Exists.elim (le.dest h) h'

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