English
Let (α_i) be a family of ordered sets indexed by ι, and f ∈ ∀ i, α_i. For any i and a ∈ α_i, the image of the half-open interval Ico(a, f(i)) under the coordinate-update map that replaces the i-th coordinate by its argument equals the half-open interval Ico(update f i a, f).
Русский
Пусть (α_i) — семейство упорядоченных множеств, индексируемое ι, и f ∈ ∀ i, α_i. Пусть i ∈ ι и a ∈ α_i. Образ полупрямого интервала Ico(a, f(i)) при отображении update f i равен Ico(update f i a, f).
LaTeX
$$$ update(f,i) '' Ico(a,f(i)) = Ico(update(f,i)(a), f) $$$
Lean4
theorem image_update_Ico_left (f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Ico a (f i) = Ico (update f i a) f := by
simpa using image_update_Ico f i a (f i)
