ofHom

Mathlib.Order.Category.NonemptyFinLinOrd

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

Lean4

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

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

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

Разделы

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

Аффилиация

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