image_mulSingle_uIcc_right — Mathlib

English

For each index i and each b in α_i, the image of the i-th coordinate update map on the box uIcc(1, b) is exactly the box uIcc(1, Pi.mulSingle(i, b)).

Русский

Для каждого индекса i и каждого b в α_i образ отображения обновления i-й координаты на коробке uIcc(1, b) равен коробке uIcc(1, Pi.mulSingle(i, b)).

LaTeX

$$$\mathrm{image}\big(\mathrm{Pi.mulSingle}(i)\big)\big(\mathrm{uIcc}(1,b)\big) = \mathrm{uIcc}\big(1, \mathrm{Pi.mulSingle}(i,b)\big).$$$

Lean4

@[to_additive]
theorem image_mulSingle_uIcc_right (i : ι) (b : α i) : Pi.mulSingle i '' uIcc 1 b = uIcc 1 (Pi.mulSingle i b) :=
  image_update_uIcc_right _ _ _

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