funLike — Mathlib

English

There is a natural way to view ContinuousAlternatingMap as a function on ι → M: each f corresponds to a function f: (ι → M) → N, and this correspondence is injective (two maps are equal whenever they agree as functions).

Русский

Существует естественный способ рассмотреть непрерывные чередующиеся отображения как функции на ι → M: каждому f соответствует функция f: (ι → M) → N, и эта связь инъективна (два отображения равны тогда и только если они совпадают как функции).

LaTeX

$$$\\forall f,g : \\mathrm{ContinuousAlternatingMap}(R,M,N,\\iota),\\, f.toFun = g.toFun \\Rightarrow f = g$$$

Lean4

instance funLike : FunLike (M [⋀^ι]→L[R] N) (ι → M) N
    where
  coe f := f.toFun
  coe_injective' _ _ h := toContinuousMultilinearMap_injective <| DFunLike.ext' h

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