applyOrderedFinpartition_apply — Mathlib

English

The application of applyOrderedFinpartition is exactly the expected one: c.applyOrderedFinpartition p v equals the function m ↦ p m (v ∘ c.emb m).

Русский

Применение applyOrderedFinpartition равно ожидаемому: c.applyOrderedFinpartition p v = (m ↦ p m (v ∘ c.emb m)).

LaTeX

$$c.applyOrderedFinpartition p v = (fun m ↦ p m (v ∘ c.emb m))$$

Lean4

theorem applyOrderedFinpartition_apply (p : ∀ (i : Fin c.length), E [×c.partSize i]→L[𝕜] F) (v : Fin n → E) :
    c.applyOrderedFinpartition p v = (fun m ↦ p m (v ∘ c.emb m)) :=
  rfl

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