coe_id_pseudoEpimorphism — Mathlib

English

coe_id_pseudoEpimorphism asserts that the identity Esakia morphism, viewed as a PseudoEpimorphism, coincides with the identity at the level of morphisms.

Русский

coe_id_pseudoEpimorphism утверждает, что единичный морфизм Эзякия, рассматриваемый как псевдо-эпиморфизм, совмещается с тождеством на уровне морфизмов.

LaTeX

$$$(\\mathrm{id}_{\\alpha}: EsakiaHom \\alpha \\alpha) : PseudoEpimorphism \\alpha \\alpha$ equals $PseudoEpimorphism.id(\\alpha)$$$

Lean4

@[simp, norm_cast]
theorem coe_id_pseudoEpimorphism : (EsakiaHom.id α : PseudoEpimorphism α α) = PseudoEpimorphism.id α :=
  rfl

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