instPreorder — Mathlib

English

Given a Monoid α and a Preorder α, the units α carry a natural preorder defined by a ≤ b if and only if a.val ≤ b.val.

Русский

Пусть α — Моноид и имеется предустройство α. Единицы α наделяются естественным порядком: a ≤ b тогда и только тогда, когда a.val ≤ b.val.

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ a \\le_{\\mathrm{Units}} b \\iff a_{\mathrm{val}} \\le b_{\mathrm{val}}$$$

Lean4

@[to_additive]
instance [Monoid α] [Preorder α] : Preorder αˣ :=
  Preorder.lift val

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