English
Updating the input function v at position j and then applying c.applyOrderedFinpartition p equals updating the result of c.applyOrderedFinpartition p v at position c.index j with the corresponding p-coefficient applied to the updated variable.
Русский
Обновление функции v по позиции j и последующее применение c.applyOrderedFinpartition p равно обновлению результата на позиции c.index j соответствующим коэффициентом p, примененным к обновляемой переменной.
LaTeX
$$c.applyOrderedFinpartition p (update v j z) = update (c.applyOrderedFinpartition p v) (c.index j) (p (c.index j) (Function.update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))$$
Lean4
theorem applyOrderedFinpartition_update_left (p : ∀ (i : Fin c.length), E [×c.partSize i]→L[𝕜] F) (m : Fin c.length)
(v : Fin n → E) (q : E [×c.partSize m]→L[𝕜] F) :
c.applyOrderedFinpartition (update p m q) v = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) :=
by
ext d
by_cases h : d = m
· rw [h]
simp [applyOrderedFinpartition]
· simp [h, applyOrderedFinpartition]
