Positive & negative parts #
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 defines posPart
and negPart
, the positive and negative parts of an element in a
lattice ordered group.
Main statements #
posPart_sub_negPart
: Every elementa
can be decomposed intoa⁺ - a⁻
, the difference of its positive and negative parts.posPart_inf_negPart_eq_zero
: The positive and negative parts are coprime.
Notations #
a⁺ᵐ = a ⊔ 1
: Positive component of an elementa
of a multiplicative lattice ordered groupa⁻ᵐ = a⁻¹ ⊔ 1
: Negative component of an elementa
of a multiplicative lattice ordered groupa⁺ = a ⊔ 0
: Positive component of an elementa
of a lattice ordered groupa⁻ = (-a) ⊔ 0
: Negative component of an elementa
of a lattice ordered group
References #
- [Birkhoff, Lattice-ordered Groups][birkhoff1942]
- [Bourbaki, Algebra II][bourbaki1981]
- [Fuchs, Partially Ordered Algebraic Systems][fuchs1963]
- [Zaanen, Lectures on "Riesz Spaces"][zaanen1966]
- [Banasiak, Banach Lattices in Applications][banasiak]
Tags #
positive part, negative part
The positive part of an element a
in a lattice ordered group is a ⊔ 1
, denoted a⁺ᵐ
.
Equations
- «term_⁺ᵐ» = Lean.ParserDescr.trailingNode `term_⁺ᵐ 1024 1024 (Lean.ParserDescr.symbol "⁺ᵐ ")
Instances For
The negative part of an element a
in a lattice ordered group is a⁻¹ ⊔ 1
, denoted a⁻ᵐ
.
Equations
- «term_⁻ᵐ» = Lean.ParserDescr.trailingNode `term_⁻ᵐ 1024 1024 (Lean.ParserDescr.symbol "⁻ᵐ")
Instances For
The positive part of an element a
in a lattice ordered group is a ⊔ 0
, denoted a⁺
.
Equations
- «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")
Instances For
The negative part of an element a
in a lattice ordered group is (-a) ⊔ 0
, denoted a⁻
.
Equations
- «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1024 1024 (Lean.ParserDescr.symbol "⁻")
Instances For
See also negPart_nonpos
.
See also leOnePart_le_one
.