instOrderHomClass

Mathlib.Algebra.Order.Hom.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#OrderMonoidWithZeroHom.instOrderHomClass

English

For an order-monoid-with-zero hom, the function component coincides with its coe to a plain function.

Русский

Для гомоморфизма с нулём в порядке равенствo функции совпадает с неким отображением.

LaTeX

$$$f.toFun = (f : \\alpha \\to \\beta)$$$

Lean4

instance : OrderHomClass (α →*₀o β) α β where map_rel f _ _ h := f.monotone' h

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

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

Разделы

Аффилиация

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