image_update_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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