orderLHom_order — Mathlib

English

The order-preserving map for the Language.order is the identity morphism on Language.order.

Русский

Порядко-целевой отображение для языка order является тождественным отображением на языке order.

LaTeX

$$$ orderLHom Language.order = LHom.id Language.order $$$

Lean4

@[simp]
theorem orderLHom_order : orderLHom Language.order = LHom.id Language.order :=
  LHom.funext (Subsingleton.elim _ _) (Subsingleton.elim _ _)

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