English
Updating with division commutes with division: update (f1 / f2) at i by (x1 / x2) equals update f1 at i by x1 divided by update f2 at i by x2.
Русский
Обновление деления согласуется с делением: обновление (f1/f2) в i на (x1/x2) равно обновлению f1 в i на x1, делённому на обновление f2 в i на x2.
LaTeX
$$$\mathrm{update}(\,f_1 / f_2\, )\; i\; (x_1 / x_2) = \mathrm{update}\, f_1\; i\; x_1 \/\; \mathrm{update}\, f_2\; i\; x_2$$$
Lean4
@[to_additive]
theorem update_div [∀ i, Div (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i) (x₂ : f i) :
update (f₁ / f₂) i (x₁ / x₂) = update f₁ i x₁ / update f₂ i x₂ :=
funext fun j => (apply_update₂ (fun _ => (· / ·)) f₁ f₂ i x₁ x₂ j).symm
