image_update_Ioc — Mathlib

English

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

Русский

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

LaTeX

$$$$ update f i '' Ioo a b = Ioo (update f i a) (update f i b) $$$$

Lean4

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

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