comp_update — Mathlib

English

The composition law for updates in multi-argument function: f ∘ update g i v = update (f ∘ g) i (f v).

Русский

Закон композиции обновлений для функций с двумя аргументами: $f \\circ update\\ g i v = update (f \\circ g) i (f v)$.

LaTeX

$$$f \\circ update g i v = update (f \\circ g) i (f v)$$

Lean4

theorem comp_update {α' : Sort*} {β : Sort*} (f : α' → β) (g : α → α') (i : α) (v : α') :
    f ∘ update g i v = update (f ∘ g) i (f v) :=
  funext <| apply_update _ _ _ _

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