instOrderedSub — Mathlib

English

WithTop α carries an OrderedSub structure, i.e., subtraction respects the order in WithTop.

Русский

WithTop α имеет структуру упорядоченного вычитания, то есть вычитание в WithTop сохраняет порядок.

LaTeX

$$$\text{OrderedSub}(\text{WithTop } \alpha)$$$

Lean4

instance : OrderedSub (WithTop α) := by
  constructor
  rintro x y z
  cases y
  · cases z <;> simp
  cases x
  · simp
  cases z
  · simp
  norm_cast
  exact tsub_le_iff_right

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