curryFinFinset_apply — Mathlib

English

A variant of curryFinFinset_apply expresses equality in terms of Sum-elimination on coordinates.

Русский

Вариант curryFinFinset_apply' выражает равенство через устранение суммы координат.

LaTeX

$$$\\text{curryFinFinset_apply}'(hk,hl,f,mk,ml) = f(\\cdot)$$$

Lean4

@[simp]
theorem curryFinFinset_apply {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin n => M') M₂) (mk : Fin k → M') (ml : Fin l → M') :
    curryFinFinset R M₂ M' hk hl f mk ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i) :=
  rfl

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