hom_ofHom

Mathlib.Order.Category.NonemptyFinLinOrd

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

← MathLib Explorer

English

For f: X →o Y, the associated LinOrd.Hom is such that (ofHom f).hom = f.

Русский

Для f: X →o Y связанный LinOrd.Hom удовлетворяет (ofHom f).hom = f.

LaTeX

$$$ (\mathrm{ofHom}(f)).\mathrm{hom} = f. $$$

Lean4

@[simp]
theorem hom_ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y]
    (f : X →o Y) : (ofHom f).hom = f :=
  rfl

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

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

Разделы

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

Аффилиация

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