leOfHom

Mathlib.CategoryTheory.Category.Preorder

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

English

From a morphism h in the preorder category, recover the underlying inequality: le h.

Русский

Из морфизма h в предкатегории восстанавливаем исходное неравенство: le h.

LaTeX

$$$\mathrm{leOfHom}(h) : x \le y$ where $h : x \to y$.$$

Lean4

/-- Extract the underlying inequality from a morphism in a preorder category. -/
theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
  h.down.down

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

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

Разделы

Аффилиация

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