canonicallyOrderedAdd — Mathlib

English

WithTop α inherits CanonicallyOrderedAdd from α; define le_self_add and le_add_self accordingly.

Русский

WithTop α наследует CanonicallyOrderedAdd от α; определяем le_self_add и le_add_self соответственно.

LaTeX

$$$\\text{WithTop}(\\alpha)$ имеет CanonicallyOrderedAdd, если $\\alpha$ имеет CanonicallyOrderedAdd$$

Lean4

instance canonicallyOrderedAdd [Add α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithTop α)
    where
  le_self_add
    | ⊤, _ => le_rfl
    | (a : α), ⊤ => le_top
    | (a : α), (b : α) => WithTop.coe_le_coe.2 le_self_add
  le_add_self
    | ⊤, ⊤ | ⊤, (b : α) => le_rfl
    | (a : α), ⊤ => le_top
    | (a : α), (b : α) => WithTop.coe_le_coe.2 le_add_self

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