instCanonicallyOrderedAdd — Mathlib

English

If α is CanonicallyOrderedAdd, then WithZero α is CanonicallyOrderedAdd.

Русский

Если α обладает канонически упорядоченным сложением, то WithZero α также обладает канонически упорядоченным сложением.

LaTeX

$$$[AddZeroClass\ α] \land [Preorder\ α] \land [CanonicallyOrderedAdd\ α] \Rightarrow [CanonicallyOrderedAdd(\mathrm{WithZero}\ α)]$$$

Lean4

/-- Adding a new zero to a canonically ordered additive monoid produces another one. -/
instance instCanonicallyOrderedAdd [AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] :
    CanonicallyOrderedAdd (WithZero α)
    where
  le_add_self
    | 0, _ => bot_le
    | (a : α), 0 => le_rfl
    | (a : α), (b : α) => WithZero.coe_le_coe.2 le_add_self
  le_self_add
    | 0, _ => bot_le
    | (a : α), 0 => le_rfl
    | (a : α), (b : α) => WithZero.coe_le_coe.2 le_self_add

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