uncurryBilinear_apply — Mathlib

English

For a bilinear f and m: Fin 2 → E × F, f.uncurryBilinear m equals the evaluation f (m(0)).1 (m(1)).2.

Русский

Для билинейного отображения f и m: Fin 2 → E × F, выполняется f.uncurryBilinear m = f (m(0)).1 (m(1)).2.

LaTeX

$$$ f.uncurryBilinear(m) = f( m(0).1 )( m(1).2 ) $$$

Lean4

@[simp]
theorem uncurryBilinear_apply (f : E →L[𝕜] F →L[𝕜] G) (m : Fin 2 → E × F) : f.uncurryBilinear m = f (m 0).1 (m 1).2 :=
  rfl

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