zeckendorf_of_pos — Mathlib

English

For n>0: zeckendorf(n) = greatestFib(n) :: zeckendorf(n - fib(greatestFib(n))).

Русский

Для n>0: zeckendorf(n) = greatestFib(n) :: zeckendorf(n - fib(greatestFib(n))).

LaTeX

$$$$ \operatorname{zeckendorf}(n) = \operatorname{greatestFib}(n) :: \operatorname{zeckendorf}(n - \operatorname{fib}(\operatorname{greatestFib}(n))). $$$$

Lean4

@[simp]
theorem zeckendorf_of_pos : ∀ {n}, 0 < n → zeckendorf n = greatestFib n :: zeckendorf (n - fib (greatestFib n))
  | _n + 1, _ => zeckendorf_succ _

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