English
For any α, x, f, the range of the recursion Nat.rec x f is the union of {x} with the range of Nat.rec (f 0 x) (f ∘ succ).
Русский
Для любых α, x, f диапазон рекурсии Nat.rec x f равен объединению {x} с диапазоном Nat.rec (f 0 x) (f ∘ succ).
LaTeX
$$$ \\forall {α : Type*} (x : α) (f : Nat → α → α),\\; \\mathrm{range}(fun n => \\mathrm{Nat}.rec x f n) = \\mathrm{Set}.instUnion.union (\\mathrm{Set}.instSingletonSet.singleton x) (\\mathrm{Set}.range fun n => \\mathrm{Nat}.rec (f 0 x) (Function.\\text{comp } f Nat.succ) n)$$$
Lean4
theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
(Set.range fun n => Nat.rec x f n : Set α) = { x } ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ succ) n :=
by
convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
dsimp
rename_i n
induction n with
| zero => rfl
| succ n ihn => dsimp at ihn ⊢; rw [ihn]
