image_update_uIcc — Mathlib

English

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

Русский

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

LaTeX

$$$ \\text{image}(\\text{update } f i)\ \bigl( \\mathrm{uIcc}(a,b) \\bigr) = \\mathrm{uIcc}( \\text{update } f i a, \\text{update } f i b) $$$

Lean4

theorem image_update_uIcc (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' uIcc a b = uIcc (update f i a) (update f i b) :=
  (image_update_Icc _ _ _ _).trans <| by simp_rw [uIcc, update_sup, update_inf]

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