coe_toContinuousMultilinearMap — Mathlib

English

The underlying function of the continuous multilinear map associated to a continuous alternating map is exactly the original map.

Русский

Функция, лежащая в основе непрерывной мультилинейной карты, связанной с непрерывным чередующимся отображением, равна самой карте.

LaTeX

$$$\\forall f : \\mathrm{ContinuousAlternatingMap}(R,M,N,\\iota),\\; (f.toContinuousMultilinearMap) = f$ as functions, i.e. $(f.toContinuousMultilinearMap)(v)=f(v)$ for all $v$.$$

Lean4

@[simp]
theorem coe_toContinuousMultilinearMap : ⇑f.toContinuousMultilinearMap = f :=
  rfl

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