instFunLike — Mathlib

English

The type of pseudo-epimorphisms from α to β carries a function-like structure: each element is a function α→β, and equality of two such elements is determined by equality of their underlying functions.

Русский

У множества псевдоэпиморфизмов между α и β имеется структура как у функции: каждый элемент является отображением α→β, и равенство двух таких элементов определяется равенством их базовых функций.

LaTeX

$$$\mathrm{FunLike}(\mathrm{PseudoEpimorphism}(\alpha,\beta), \alpha, \beta)$$$

Lean4

instance instFunLike : FunLike (PseudoEpimorphism α β) α β
    where
  coe f := f.toFun
  coe_injective' f g
    h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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