ofHom_id — Mathlib

English

The image of the identity order isomorphism under the OfHom construction is the identity morphism on the image object.

Русский

Образ обратимого порядка-изоморфизма, полученный через OfHom, равен тождественному морфизму на образе.

LaTeX

$$$ \\operatorname{ofHom}(\\mathrm{OrderHom.id}) = \\mathbf{1}_{\\operatorname{of}(X)} $$$

Lean4

@[simp]
theorem ofHom_id {X : Type u} [Preorder X] : ofHom OrderHom.id = 𝟙 (of X) :=
  rfl

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