homOfLE_refl

Mathlib.CategoryTheory.Category.Preorder

URI: https://scilib.ai/kg/mathlib#CategoryTheory.homOfLE_refl

English

If h is a reflexive inequality x ≤ x, then the corresponding morphism is the identity on x.

Русский

Если неравенство рефлексивно: x ≤ x, соответствующая морфизм — тождественный на x.

LaTeX

$$$\mathrm{homOfLE}(h) = \mathrm{Id}_x$ for $h : x \le x$.$$

Lean4

@[simp]
theorem homOfLE_refl {x : X} (h : x ≤ x) : h.hom = 𝟙 x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru