English
Let ι be an index set, α(i) and β(i) be families of types, f(i): α(i) → β(i). For any g: ∀i, α(i) → β(i), index i, and a ∈ α(i), the Pi-map of f applied to the update g(i) a equals the update of Pi-map g at i by f(i) a.
Русский
Пусть ι — множество индексов, α(i) и β(i) — семейства типов, f(i): α(i) → β(i). Для любого g: ∀i, α(i) → β(i), и элемента a ∈ α(i) выполняется равенство: Pi.map f (update g i a) = update (Pi.map f g) i (f i a).
LaTeX
$$$\mathrm{Pi.map}\ f\ (\mathrm{update}\ g\ i\ a) = \mathrm{update}\ (\mathrm{Pi.map}\ f\ g)\ i\ (f\ i\ a)$$$
Lean4
@[simp]
theorem _root_.Pi.map_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*} {f : ∀ i, α i → β i} (g : ∀ i, α i) (i : ι)
(a : α i) : Pi.map f (Function.update g i a) = Function.update (Pi.map f g) i (f i a) :=
by
ext j
obtain rfl | hij := eq_or_ne j i <;> simp [*]
