ofHom

Mathlib.Order.Category.Preord

URI: https://scilib.ai/kg/mathlib#Preord.ofHom

← MathLib Explorer

English

Typecheck an OrderHom as a morphism in Preord.

Русский

Типизировать OrderHom как морфизм в Preord.

LaTeX

$$$\mathrm{Preord.ofHom}(f) : \mathrm{Preord.of}(X) \to \mathrm{Preord.of}(Y)$$$

Lean4

/-- Typecheck a `OrderHom` as a morphism in `Preord`. -/
abbrev ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := Preord) f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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