English
For an Option-indexed family, updating a g at a creates a new Option.rec that commutes with the update of g via its some constructor.
Русский
Для семейства, индексированного по Option, обновление g в some-координате совместимо с рекурсивным обновлением Option.rec.
LaTeX
$$$\\mathrm{Option.rec}\\ f\\ (\\mathrm{update}\\ g\\ a\\ x) = \\mathrm{update}(\\mathrm{Option.rec}\\ f g) (\\mathrm{Some}\\ a) x$$
Lean4
@[simp]
theorem _root_.Option.rec_update {α : Type*} {β : Option α → Sort*} [DecidableEq α] (f : β none) (g : ∀ a, β (.some a))
(a : α) (x : β (.some a)) : Option.rec f (update g a x) = update (Option.rec f g) (.some a) x :=
Function.rec_update (@Option.some.inj _) (Option.rec f) (fun _ _ => rfl)
(fun
| _, _, some _, h => (h _ rfl).elim
| _, _, none, _ => rfl)
_ _ _
