id_apply — Mathlib

English

coe_id_continuousOrderHom states that the identity Esakia morphism corresponds to the identity continuous-order homomorphism.

Русский

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

LaTeX

$$$\\operatorname{coe\\_id\\_continuousOrderHom}: (\\mathrm{id}\\_\\alpha) = \\mathrm{ContinuousOrderHom.id}(\\alpha)$$$

Lean4

@[simp]
theorem id_apply (a : α) : EsakiaHom.id α a = a :=
  rfl

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