Notations for operations involving order and algebraic structure

Notations

• 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.

Equations

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

def «term_⁻ᵐ» : Lean.TrailingParserDescr

The negative part of an element a.

Equations

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

def «term_⁺» : Lean.TrailingParserDescr

The positive part of an element a.

Equations

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

def «term_⁻» : Lean.TrailingParserDescr

The negative part of an element a.

Equations

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