homOfLE_leOfHom — Mathlib

English

The morphism corresponding to h is equal to h when viewed as a morphism between the same objects, i.e., h.hom = h.

Русский

Морфизм, соответствующий h, равен самому h, когда рассматривается как морфизм между теми же объектами;

LaTeX

$$$\mathrm{homOfLE\_leOfHom} : \forall h : x \to y, \mathrm{homOfLE}(h) = h$.$$

Lean4

@[simp]
theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
  rfl

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