image_update_Ioo_left — Mathlib

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 interval Ioo(a, f(i)) under the coordinate-update map equals the interval Ioo(update f i a, f).

Русский

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

LaTeX

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

Lean4

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

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