toSub — Mathlib

English

There is a Sub structure on a canonically ordered additive monoid defined by a choice principle that makes subtraction well-defined when possible.

Русский

На канонически упорядоченном аддитивном моноиде существует структура вычитания, определяемая выбором, когда вычитание возможно.

LaTeX

$$$\text{CanonicallyOrderedAdd}(\alpha) \Rightarrow \text{Sub}\,\alpha$$$

Lean4

/-- `Sub` structure in linearly canonically ordered monoid using choice. -/
noncomputable abbrev toSub : Sub α where sub x y := if h : y ≤ x then (exists_add_of_le h).choose else 0

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