id — Mathlib · SciLib

English

There is an identity pseudo-epimorphism id on α, given by the order-id map, with the property that it maps each a to itself and its toFun equals the identity function.

Русский

Существует тождественный псевдоэпиморфизм id на α, задаваемый тождественным отображением по порядку, который от a до a и у которого toFun равен тождественной функцией.

LaTeX

$$$\mathrm{PseudoEpimorphism}.\mathrm{id}:\alpha\to\alpha$ с характеристиками: $\mathrm{id}.toOrderHom=\mathrm{Id}$ и $\mathrm{toFun} = \mathrm{id}$$$

Lean4

/-- `id` as a `PseudoEpimorphism`. -/
protected def id : PseudoEpimorphism α α :=
  ⟨OrderHom.id, fun _ b h => ⟨b, h, rfl⟩⟩

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