eqToHom_eq_homOfLE

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.eqToHom_eq_homOfLE

English

In any preorder, the canonical equality-to-hom correspondence equals the homOfLE construction.

Русский

В любой предобразной структуре каноническое соответствие равенств и морфизмов совпадает с построением homOfLE.

LaTeX

$$$eqToHom e = homOfLE e.le$ for $e: X=Y$$$

Lean4

theorem eqToHom_eq_homOfLE {C} [Preorder C] {X Y : C} (e : X = Y) : eqToHom e = homOfLE e.le :=
  rfl

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

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

Разделы

Аффилиация

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