hom

Mathlib.CategoryTheory.Category.Preorder

URI: https://scilib.ai/kg/mathlib#LE.le.hom

English

The morphism builder LE.hom is just homOfLE; it is a convenient name for the same morphism.

Русский

Конструктор морфизмов LE.hom является тем же самым как и homOfLE; это удобное обозначение.

LaTeX

$$$\mathrm{LE.hom} := \mathrm{homOfLE}$.$$

Lean4

@[inherit_doc homOfLE]
abbrev _root_.LE.le.hom :=
  @homOfLE

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

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

Разделы

Аффилиация

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