image_update_uIcc_right — Mathlib

English

Replacing the i-th coordinate by b and then taking the image of uIcc yields the uIcc between f and update f i b.

Русский

Замещая i-ю координату на b и затем беря образ uIcc, получаем uIcc между f и update f i b.

LaTeX

$$$ update(f,i) '' uIcc(f(i), b) = uIcc(f, update(f,i)(b)) $$$

Lean4

theorem image_update_uIcc_right (f : ∀ i, α i) (i : ι) (b : α i) : update f i '' uIcc (f i) b = uIcc f (update f i b) :=
  by simpa using image_update_uIcc f i (f i) b

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