Notations for operations involving order and algebraic structure

Notation

• a⁺ᵐ = a ⊔ 1: Positive component of an element a of a multiplicative lattice ordered group
• a⁻ᵐ = a⁻¹ ⊔ 1: Negative component of an element a of a multiplicative lattice ordered group
• a⁺ = a ⊔ 0: Positive component of an element a of a lattice ordered group
• a⁻ = (-a) ⊔ 0: Negative component of an element a of a lattice ordered group

class PosPart (α : Type u_1) : Type u_1

A notation class for the positive part function: a⁺.

• posPart : α → α

  The positive part of an element a.

class OneLePart (α : Type u_1) : Type u_1

A notation class for the positive part function (multiplicative version): a⁺ᵐ.

• oneLePart : α → α

  The positive part of an element a.

class NegPart (α : Type u_1) : Type u_1

A notation class for the negative part function: a⁻.

• negPart : α → α

  The negative part of an element a.

class LeOnePart (α : Type u_1) : Type u_1

A notation class for the negative part function (multiplicative version): a⁻ᵐ.

• leOnePart : α → α

  The negative part of an element a.

def «term_⁺ᵐ» : Lean.TrailingParserDescr

The positive part of an element a.

def «term_⁻ᵐ» : Lean.TrailingParserDescr

The negative part of an element a.

def «term_⁺» : Lean.TrailingParserDescr

The positive part of an element a.

def «term_⁻» : Lean.TrailingParserDescr

The negative part of an element a.