image_update_Ioo_right — Mathlib

English

Let (α_i) be a family of ordered sets indexed by ι, and f ∈ ∀ i, α_i. For any i and b ∈ α_i, the image of Ioo(f(i), b) under the coordinate-update map equals Ioo(f, update f i b).

Русский

Пусть (α_i) — семейство упорядоченных множеств индексированное ι, и f ∈ ∀ i, α_i. Пусть i ∈ ι и b ∈ α_i. Образ Ioo(f(i), b) при обновлении i-й координаты равен Ioo(f, update f i b).

LaTeX

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

Lean4

theorem image_update_Ioo_right (f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Ioo (f i) b = Ioo f (update f i b) := by
  simpa using image_update_Ioo f i (f i) b

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