# 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 `PosPart`

and `NegPart`

classes
which add unary operators `pos`

and `neg`

, representing the maps taking an element to its positive
and negative part respectively along with the notation `⁺⁺`

and `⁻⁻`

.

## Notations #

The following notation is introduced:

`|.|`

for the absolute value;`.⁺⁺`

for the positive part;`.⁻⁻`

for the negative part.

## Tags #

absolute

The absolute value function.

## Equations

- One or more equations did not get rendered due to their size.

The positive part function.

## Equations

- «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1000 1000 (Lean.ParserDescr.symbol "⁺")

The negative part function.

## Equations

- «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1000 1000 (Lean.ParserDescr.symbol "⁻")