instFunLike — Mathlib

English

There is a canonical FunLike structure turning an affine basis into a function from the index set to points, with an injective coe.

Русский

Существует каноническая структура FunLike превращающая аффинный базис в функцию от индексов в точки пространства, причём вложение функция-инъекция.

LaTeX

$$$\text{Injective}\big(\text{toFun} : \text{AffineBasis } ι k P \to (ι \to P)\big)$$$

Lean4

instance instFunLike : FunLike (AffineBasis ι k P) ι P
    where
  coe := AffineBasis.toFun
  coe_injective' f g h := by cases f; cases g; congr

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