image_update_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_update_Ico (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' Ico a b = Ico (update f i a) (update f i b) := by
  rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton, image_update_Icc]

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