update — Mathlib

English

In HasProd, updating the function at a single index b by a value a transforms the product by multiplying by a/f(b).

Русский

При обновлении функции в индексе b значением a произведение умножается на a/f(b).

LaTeX

$$HasProd f a1 L → ∀ b, HasProd (update f b a) (a / f b * a1) L$$

Lean4

@[to_additive]
theorem update [L.LeAtTop] (hf : HasProd f a₁ L) (b : β) [DecidableEq β] (a : α) :
    HasProd (update f b a) (a / f b * a₁) L :=
  by
  convert (hasProd_ite_eq b (a / f b) (L := L)).mul hf with b'
  by_cases h : b' = b
  · rw [h, update_self]
    simp
  · simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

Похожие утверждения