compAlongOrderFinpartition_apply — Mathlib

English

Taylor-type decomposition: the Taylor composition equals applying q to the sigma-structured blocks, i.e., q.compAlongOrderedFinpartition p c evaluated at v is the same as applying q to the concatenation of p-blocks across c.applyOrderedFinpartition.

Русский

Тип Тейлора: композиция q.taylor внутри f равна применению q к блочно-структурированным блокам; эквивалентно применению q к q-компонентам, полученным через p.

LaTeX

$$∑ c : OrderedFinpartition n, q.compAlongOrderedFinpartition p c$$

Lean4

@[simp]
theorem compAlongOrderFinpartition_apply (f : F [×c.length]→L[𝕜] G) (p : ∀ i, E [×c.partSize i]→L[𝕜] F)
    (v : Fin n → E) : c.compAlongOrderedFinpartition f p v = f (c.applyOrderedFinpartition p v) :=
  rfl

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