preorder

Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags

URI: https://scilib.ai/kg/mathlib#Additive.preorder

English

The additive tag on α inherits the same preorder as α.

Русский

Тег Additive α наследует тот же порядок, что и α.

LaTeX

$$$\text{Preorder}(\mathrm{Additive}\,\alpha) = \text{Preorder}(\alpha)$$$

Lean4

instance preorder : ∀ [Preorder α], Preorder (Additive α) := fun {inst} => inst

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

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

Разделы

Аффилиация

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