go_succ — Mathlib

English

The auxiliary function go satisfies go(k+1, p, n) = go(k, p, n) + 1.

Русский

Вспомогательная функция go удовлетворяет go(k+1, p, n) = go(k, p, n) + 1.

LaTeX

$$$ go(k+1, p, n) = go(k, p, n) + 1 $$$

Lean4

theorem go_succ {k p n : ℕ} : go (k + 1) p n = go k p n + 1 :=
  by
  fun_induction go
  case case1 h ih =>
    conv_lhs => unfold go
    simpa [if_pos h] using ih
  case case2 h =>
    conv_lhs => unfold go
    simp [if_neg h]

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