orderedSub — Mathlib

English

The nonnegative subtype { x ∈ α | 0 ≤ x } supports an OrderedSub structure compatible with subtraction.

Русский

Неотрицательный подтип поддерживает структуру OrderedSub, совместимую с вычитанием.

LaTeX

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

Lean4

instance orderedSub [Ring α] [LinearOrder α] [IsStrictOrderedRing α] : OrderedSub { x : α // 0 ≤ x } :=
  ⟨by
    rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
    simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le]⟩

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