sub — Mathlib

English

The subtraction on the nonnegative subtype is defined by taking the nonnegative part of the ambient difference: Sub x y = toNonneg (x − y).

Русский

Вычитание на подтипе неотрицательных элементов определяется взятием неотрицательной части разности: Sub x y = toNonneg (x − y).

LaTeX

$$$ Sub x y = toNonneg (x - y) $$$

Lean4

instance sub [Sub α] : Sub { x : α // 0 ≤ x } :=
  ⟨fun x y => toNonneg (x - y)⟩

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