English
Recursor on ULift commutes with pointwise update: updating a dependent family and then recursing equals recursing after updating.
Русский
Рекурсор ULift сохраняет совместимость с точечным обновлением: обновление зависимой семьи и затем рекурсия равно рекурсии после обновления.
LaTeX
$$$\\mathrm{ULift.rec}(\\mathrm{update}\\ f\\ a\\ x) = \\mathrm{update}(\\mathrm{ULift.rec}\,f) (\\mathrm{up}(a))\\ x$$$
Lean4
@[simp]
theorem rec_update {β : ULift α → Type*} [DecidableEq α] (f : ∀ a, β (.up a)) (a : α) (x : β (.up a)) :
ULift.rec (update f a x) = update (ULift.rec f) (.up a) x :=
Function.rec_update up_injective (ULift.rec ·) (fun _ _ => rfl)
(fun
| _, _, .up _, h => (h _ rfl).elim)
_ _ _
