instFunLike — Mathlib

English

There is a defined map that sends an EsakiaHom between α and β to a PseudoEpimorphism α→β by reusing its underlying order-preserving structure.

Русский

Определено отображение, переводящее EsakiaHom между α и β в псевдоэпиморфизм α→β, используя его базовую упорядоченную структуру.

LaTeX

$$$\mathrm{toPseudoEpimorphism}:\mathrm{EsakiaHom}(\alpha,\beta)\to \mathrm{PseudoEpimorphism}(\alpha,\beta)$$$

Lean4

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

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