range_of_succ — Mathlib

English

For any f, the range of the recursion f is the union of the initial value and the range of the recursive step.

Русский

Для любой функции f множество значений рекурсии есть объединение начального значения и диапазона шага рекурсии.

LaTeX

$$$ \\mathrm{range}(fun n => \\mathrm{Nat}.rec x f n) = \\{ x \\} \\cup \\mathrm{range}(fun n => \\mathrm{Nat}.rec (f 0 x) (f \\circ \\mathrm{succ}) n)$$$

Lean4

theorem range_of_succ (f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f := by
  rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

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