English
The function Nat.findGreatest returns the largest i ≤ n with P(i), or 0 if none exists.
Русский
Функция Nat.findGreatest возвращает наибольший i ≤ n с P(i), либо 0, если такого i нет.
LaTeX
$$$\\text{findGreatest}(P): \\mathbb{N} \\to \\mathbb{N},\\ \\, \\text{findGreatest}(P)(n) = \\begin{cases} 0, & n=0 \\\\ \\text{if } P(n) \\text{ then } n \\text{ else findGreatest}(P)(n-1) \\end{cases}$$$
Lean4
/-- `Nat.findGreatest P n` is the largest `i ≤ n` such that `P i` holds, or `0` if no such `i`
exists -/
def findGreatest (P : ℕ → Prop) [DecidablePred P] : ℕ → ℕ
| 0 => 0
| n + 1 => if P (n + 1) then n + 1 else Nat.findGreatest P n
