English
For a dependent family γ, and a update at i of f, the curry of the updated function equals the nested updates of the curried function: Sigma.curry (update f i x) = update (Sigma.curry f) i.1 (update (Sigma.curry f i.1) i.2 x).
Русский
Пусть γ — зависимая семейство, и функция обновляется в точке i. Тогда кюрри обновленной функции равняется вложенным обновлениям кюрри-функции.
LaTeX
$$$\\Sigma\\text{curry} (\\mathrm{Function.update} f\ \ i\ x) = \\mathrm{Function.update} (\\Sigma\\text{curry} f) i.1 \\left( \\mathrm{Function.update} (\\Sigma\\text{curry} f\ \ i.1) i.2 x \\right).$$$
Lean4
theorem curry_update {γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)] (i : Σ a, β a)
(f : (i : Σ a, β a) → γ i.1 i.2) (x : γ i.1 i.2) :
Sigma.curry (Function.update f i x) =
Function.update (Sigma.curry f) i.1 (Function.update (Sigma.curry f i.1) i.2 x) :=
by
obtain ⟨ia, ib⟩ := i
ext ja jb
unfold Sigma.curry
obtain rfl | ha := eq_or_ne ia ja
· obtain rfl | hb := eq_or_ne ib jb
· simp
· simp only [update_self]
rw [Function.update_of_ne (mt _ hb.symm), Function.update_of_ne hb.symm]
rintro h
injection h
· rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
· exact ha.symm
· exact ha.symm
