English
Every natural number has a unique Zeckendorf representation as a sum of non-consecutive Fibonacci numbers (ignoring F0 = 0 and F1 = 1). Equivalently, there is a bijection between the natural numbers and the Zeckendorf representations.
Русский
У каждого натурального числа существует уникальное представление по Зекендорфу как сумма непоследовательных чисел Фибоначчи (исключая F0 = 0 и F1 = 1). Эквивалентно: между натуральными числами и представлениями по Зекендорфу существует биекция.
LaTeX
$$$\\exists!\\, l \\ \\text{such that} \\ IsZeckendorfRep(l) \\text{ and } n = \\sum_{i \\in l} F_i,$ i.e. every $n \\in \\mathbb{N}$ has a unique Zeckendorf representation.$$
Lean4
/-- **Zeckendorf's Theorem** as an equivalence between natural numbers and Zeckendorf
representations. Every natural number can be written uniquely as a sum of non-consecutive Fibonacci
numbers (if we forget about the first two terms `F₀ = 0`, `F₁ = 1`). -/
def zeckendorfEquiv : ℕ ≃ { l // IsZeckendorfRep l }
where
toFun n := ⟨zeckendorf n, isZeckendorfRep_zeckendorf _⟩
invFun l := (map fib l).sum
left_inv := sum_zeckendorf_fib
right_inv l := Subtype.ext <| zeckendorf_sum_fib l.2
