instFunLike — Mathlib

English

The collection of ContinuousAlgHom R A B carries a FunLike structure: each element acts as a function A → B, with equality determined by the underlying AlgHom.

Русский

Множество ContinuousAlgHom R A B имеет структуру FunLike: каждый элемент действует как отображение A → B, и равенство определяется по базовой AlgHom.

LaTeX

$$$\\text{ContinuousAlgHom}\\;R\\;A\\;B\\text{ is a FunLike structure with } f \\mapsto f.toAlgHom$$$

Lean4

instance : FunLike (A →A[R] B) A B where
  coe f := f.toAlgHom
  coe_injective' f g
    h := by
    cases f; cases g
    simp only [mk.injEq]
    exact AlgHom.ext (congrFun h)

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