apply_update — Mathlib

English

A general distributive law: f j (update g i v j) = update (λk, f k (g k)) i (f i v) j for suitable f, g, i, v, j.

Русский

Общее распределительное свойство: $f(j, update g i v j)$ равно обновлению композиции $f k (g k)$ в точке i и аргументе v.

LaTeX

$$$f j (update g i v j) = update (\\lambda k \\mapsto f k (g k)) i (f i v) j$$

Lean4

theorem apply_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*} (f : ∀ i, α i → β i) (g : ∀ i, α i) (i : ι) (v : α i)
    (j : ι) : f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j :=
  by
  by_cases h : j = i
  · subst j
    simp
  · simp [h]

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