continuousMultilinearCurryLeftEquiv_apply

English

The value of the curryLeft equivalence applied to f at x and v coincides with the evaluation of f at the appropriately concatenated input.

Русский

Значение эквивалентности curryLeft, примененное к f на x и v, совпадает с значением f на соответствующем соединенном вводе.

LaTeX

$$$\text{(continuousMultilinearCurryLeftEquiv 𝕜 Ei G)}\!\, f\; x\; v = f(\text{cons } x\; v)$$$

Lean4

@[simp]
theorem continuousMultilinearCurryLeftEquiv_apply (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0)
    (v : Π i : Fin n, Ei i.succ) : continuousMultilinearCurryLeftEquiv 𝕜 Ei G f x v = f (cons x v) :=
  rfl

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