le

Mathlib.CategoryTheory.Category.Preorder

URI: https://scilib.ai/kg/mathlib#Quiver.Hom.le

English

The hom-set morphism LE is available as a Quiver.Hom.le; it is just leOfHom.

Русский

Гомоморфизм неравенств доступен как Quiver.Hom.le; он есть просто leOfHom.

LaTeX

$$$\mathrm{Quiver.Hom.le} := \mathrm{leOfHom}$.$$

Lean4

@[nolint defLemma, inherit_doc leOfHom]
abbrev _root_.Quiver.Hom.le :=
  @leOfHom

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

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

Разделы

Аффилиация

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