coe_mk — Mathlib

English

Constructing a continuous alternating map from a continuous multilinear map preserves the underlying function: the canonical coercion of mk f h is f.

Русский

Построение непрерывного чередующегося отображения из непрерывной мультил линейной карты сохраняет функцию: сопоставление mk f h эквивалентно f.

LaTeX

$$$\\forall f:\\mathrm{ContinuousMultilinearMap}(R\\; (\\lambda\\_,M)\\to N),\\; \\forall h,\\; \\bigl(\\text{mk } f\\, h\\bigr) = f$ как функции.$$

Lean4

@[simp]
theorem coe_mk (f : ContinuousMultilinearMap R (fun _ : ι => M) N) (h) : ⇑(mk f h) = f :=
  rfl

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