hom_ofHom — Mathlib

English

For f: X →o Y, the associated underlying morphism satisfies that its hom component equals f.

Русский

Для f: X →o Y соответствующий морфизм имеет такую же действующую на элементах функцию, то есть его характеристика равна f.

LaTeX

$$$ (\\operatorname{ofHom}(f)).\\mathrm{hom} = f $$$

Lean4

@[simp]
theorem hom_ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) : (ofHom f).hom = f :=
  rfl

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