instFunLike — Mathlib

English

An instance that equips Derivation with a FunLike interface, enabling pointwise evaluation and functional extensionality.

Русский

Инстанс, устанавливающий у Derivation интерфейс FunLike, позволяющий поэлементную оценку и функциональную эквивалентность.

LaTeX

$$instFunLike : Derivation R A M → FunLike (Derivation R A M) A M$$

Lean4

instance : FunLike (Derivation R A M) A M where
  coe D := D.toFun
  coe_injective' D1 D2 h := by cases D1; cases D2; congr; exact DFunLike.coe_injective h

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