findGreatest_succ — Mathlib

English

Find greatest at a successor: findGreatest P (n+1) equals n+1 if P(n+1) holds, otherwise equals findGreatest P n.

Русский

Для следующего шага: findGreatest P (n+1) = n+1, если P(n+1) истинно; иначе = findGreatest P n.

LaTeX

$$$\\mathrm{findGreatest}(P, n+1) = \\begin{cases} n+1, & P(n+1) \\\\ \\mathrm{findGreatest}(P, n), & \\text{иначе} \\end{cases}$$$

Lean4

theorem findGreatest_succ (n : ℕ) : Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n :=
  rfl

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