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

class Abs (α : Type u_1) : Type u_1

Absolute value is a unary operator with properties similar to the absolute value of a real number.

• abs : α → α

  The absolute value function.

class PosPart (α : Type u_1) : Type u_1

The positive part of an element admitting a decomposition into positive and negative parts.

• pos : α → α

  The positive part function.

class NegPart (α : Type u_1) : Type u_1

The negative part of an element admitting a decomposition into positive and negative parts.

• neg : α → α

  The negative part function.

def «term|___|» : Lean.ParserDescr

The absolute value function.

Equations

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

def Abs.abs.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the notation |a| for abs a. Tries to add discretionary parentheses in unparseable cases.

Equations

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

def «term_⁺» : Lean.TrailingParserDescr

The positive part function.

Equations

• «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")

def «term_⁻» : Lean.TrailingParserDescr

The negative part function.

Equations

• «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1024 1024 (Lean.ParserDescr.symbol "⁻")