instFunLike — Mathlib

English

There is a canonical function-like structure turning a PerfectPairing R M N into a map M → (N → R) sending m to the linear form n ↦ p(m,n).

Русский

Существует каноническая функциональная структура, превращающая совершенную пару в отображение M → (N → R), отправляющее m в форму n ↦ p(m,n).

LaTeX

$$$\text{FunLike}(\mathrm{PerfectPairing}\ R\ M\ N)\ M\ (N\to R)$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
instance instFunLike : FunLike (PerfectPairing R M N) M (N →ₗ[R] R)
    where
  coe f := f.toLinearMap
  coe_injective' x y h := by cases x; cases y; simpa using h

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