instFunLikeForall — Mathlib

English

The function extracted from a constructor is the same as the original function: the action of the constructed multilinear map equals the original f.

Русский

Функция, полученная конструктором, совпадает с исходной функцией: действие сконструированного многочленного отображения совпадает с исходной функцией f.

LaTeX

$$$ \forall x, \bigl( \langle f, h_1, h_2 \rangle \bigr)(x) = f(x) $$$

Lean4

instance : FunLike (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
    where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; cases h; rfl

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