English
If HasProd f a L and HasProd (update f b x) a' L, then a·x = a'·f(b).
Русский
Если HasProd f на a и HasProd обновления f в точке b даёт a', то a·x = a'·f(b).
LaTeX
$$a * x = a' * f(b)$$
Lean4
/-- Version of `HasProd.update` for `CommMonoid` rather than `CommGroup`.
Rather than showing that `f.update` has a specific product in terms of `HasProd`,
it gives a relationship between the products of `f` and `f.update` given that both exist. -/
@[to_additive /-- Version of `HasSum.update` for `AddCommMonoid` rather than `AddCommGroup`.
Rather than showing that `f.update` has a specific sum in terms of `HasSum`,
it gives a relationship between the sums of `f` and `f.update` given that both exist. -/
]
theorem update' [L.LeAtTop] [L.NeBot] {α : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α]
[DecidableEq β] {f : β → α} {a a' : α} (hf : HasProd f a L) (b : β) (x : α) (hf' : HasProd (update f b x) a' L) :
a * x = a' * f b :=
by
have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 :=
by
intro b'
split_ifs with hb'
· simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x
· simp only [Function.update_apply, hb', if_false]
have h := hf.mul (hasProd_ite_eq b x L)
simp_rw [this] at h
exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b) L))
