update_one — Mathlib

English

If each coordinate space has a unit, updating the constant-1 function at i to 1 yields 1.

Русский

Если каждая координата имеет единичный элемент, обновление константной единицы в позиции i до единицы даёт единицу.

LaTeX

$$$\mathrm{update}(1 : \forall i, f_i)\, i\, 1 = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem update_one [∀ i, One (f i)] [DecidableEq I] (i : I) : update (1 : ∀ i, f i) i 1 = 1 :=
  update_eq_self i (1 : (a : I) → f a)

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