Absolute value #
This file defines a notational class
Abs which adds the unary operator
abs and the notation
|.|. The concept of an absolute value occurs in lattice ordered groups and in GL and GM spaces.
Mathematical structures possessing an absolute value often also possess a unique decomposition of
elements into "positive" and "negative" parts which are in some sense "disjoint" (e.g. the Jordan
decomposition of a measure). This file also defines
which add unary operators
neg, representing the maps taking an element to its positive
and negative part respectively along with the notation
The following notation is introduced:
|.|for the absolute value;
.⁺⁺for the positive part;
.⁻⁻for the negative part.
The absolute value function.
- One or more equations did not get rendered due to their size.
The positive part function.
- «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1000 1000 (Lean.ParserDescr.symbol "⁺")
The negative part function.
- «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1000 1000 (Lean.ParserDescr.symbol "⁻")