image_update_uIcc_left — Mathlib

English

Replacing the i-th coordinate by a and then taking the image of uIcc with bounds (a, f(i)) yields the uIcc between update f i a and f.

Русский

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

LaTeX

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

Lean4

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

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