English
Recursors can be pushed inside Function.update: applying a recursor after an update equals updating the recursor applied to the function with the updated constructor.
Русский
Рекурсоры могут быть перенесены внутрь Function.update: применение рекурсора после обновления эквивалентно обновлению рекурсора, применённого к функции в соответствующем конструкторе.
LaTeX
$$$\\operatorname{recursor}(\\mathrm{update} f\\ i\\ x) = \\mathrm{update}(\\operatorname{recursor} f) (\\mathrm{ctor}(i)) x$$$
Lean4
/-- Non-dependent version of `Function.update_comp_eq_of_injective'` -/
theorem update_comp_eq_of_injective {β : Sort*} (g : α' → β) {f : α → α'} (hf : Function.Injective f) (i : α) (a : β) :
Function.update g (f i) a ∘ f = Function.update (g ∘ f) i a :=
update_comp_eq_of_injective' g hf i a
