English
If s ⊆ t, then updateFinset (updateFinset x s y) t z = updateFinset x t z.
Русский
Если s ⊆ t, тогда обновление по s затем по t эквивалентно обновлению по t.
LaTeX
$$$s \\subseteq t \\Rightarrow \\text{updateFinset}(\\text{updateFinset } x\\ s\\ y)\\ t\\ z = \\text{updateFinset}\\; x\\; t\\; z$$$
Lean4
/-- If one replaces the variable indexed by `i`, then `f` no longer depends on
this variable. -/
theorem _root_.DependsOn.update {α : Type*} {f : (Π i, π i) → α} {s : Finset ι} (hf : DependsOn f s) (i : ι) (y : π i) :
DependsOn (fun x ↦ f (Function.update x i y)) (s.erase i) :=
by
simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]
exact hf.updateFinset _
