image_update_Icc_left — Mathlib

English

For f, i, a, the image of Icc(a, b) under update f i equals Icc(update f i a, update f i b).

Русский

Для f, i, a образ Icc(a,b) под обновлением f i равен Icc(update f i a, update f i b).

LaTeX

$$$$ image (update f i) '' Icc a b = Icc (update f i a) (update f i b) $$$$

Lean4

theorem image_update_Icc_left (f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Icc a (f i) = Icc (update f i a) f := by
  simpa using image_update_Icc f i a (f i)

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