pred_iterate — Mathlib

English

Iterating the predecessor n times yields subtraction by n: pred^{[n]}(x) = x − n.

Русский

Повторное применение предшественника n раз даёт вычитание на n: pred^{[n]}(x) = x − n.

LaTeX

$$$\\\\mathrm{pred}^{[n]}(x) = x - n.$$$

Lean4

@[simp]
theorem pred_iterate [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) : pred^[n] x = x - n := by
  induction n with
  | zero => rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH => rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

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