canonicallyOrderedAdd — Mathlib

English

The nonnegative subtype { x ∈ α | 0 ≤ x } carries a CanonicallyOrderedAdd structure when α is a ring with order.

Русский

Неотрицательный подтип имеет канонически упорядоченное сложение, если α — кольцо упорядочено.

LaTeX

$$$\\text{CanonicallyOrderedAdd}\\, \\{ x : \\alpha \\mid 0 \\le x \\}$$$

Lean4

instance canonicallyOrderedAdd [Ring α] [PartialOrder α] [IsOrderedRing α] : CanonicallyOrderedAdd { x : α // 0 ≤ x }
    where
  le_add_self _ b := le_add_of_nonneg_left b.2
  le_self_add _ b := le_add_of_nonneg_right b.2
  exists_add_of_le := fun {a b} h => ⟨⟨b - a, sub_nonneg_of_le h⟩, Subtype.ext (add_sub_cancel _ _).symm⟩

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