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

Русский

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

LaTeX

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

Lean4

theorem image_update_Ioc_left (f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Ioc a (f i) = Ioc (update f i a) f := by
  simpa using image_update_Ioc f i a (f i)

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