elim_left — Mathlib

English

Let P be a proposition. If a | b and for every c with b = c · a we have P, then P holds.

Русский

Пусть P — произвольное утверждение. Если a|b и для каждого c при b = c · a выполняется P, то P истинно.

LaTeX

$${P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P$$

Lean4

theorem elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
  Exists.elim (exists_eq_mul_left_of_dvd h₁) fun c => fun h₃ : b = c * a => h₂ c h₃

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