image_update_Ico_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 Ico(f(i), b) under the coordinate-update map equals Ico(f, update f i b).

Русский

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

LaTeX

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

Lean4

theorem image_update_Ico_right (f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Ico (f i) b = Ico f (update f i b) := by
  simpa using image_update_Ico f i (f i) b

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