curryFinFinset_symm_apply — Mathlib

English

A specialized lemma that computes symm application on a piecewise-constant input by separating left and right parts.

Русский

Специализированная лемма для вычисления симм применения к входу с кусочно-постоянным значением через разложение на левую и правую части.

LaTeX

$$$\\text{curryFinFinset_symm_apply_piecewise_const}(hk,hl,f,x,y) = \\text{...}$$$

Lean4

@[simp]
theorem curryFinFinset_symm_apply {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (m : Fin n → M') :
    (curryFinFinset R M₂ M' hk hl).symm f m =
      f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i => m <| finSumEquivOfFinset hk hl (Sum.inr i) :=
  rfl

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