# 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 provides instances of `PosPart` and `NegPart`, the positive and negative parts of an element in a lattice ordered group.

## Main statements #

- `posPart_sub_negPart`: Every element `a` can be decomposed into `a⁺ - a⁻`, the difference of its positive and negative parts.
- `posPart_inf_negPart_eq_zero`: The positive and negative parts are coprime.

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

source
instance instOneLePart {α : Type u_1} [Lattice α] [Group α] :
OneLePart α

The positive part of an element `a` in a lattice ordered group is `a ⊔ 1`, denoted `a⁺ᵐ`.

Equations

- instOneLePart = { oneLePart := fun (a : α) => a ⊔ 1 }

source
instance instPosPart {α : Type u_1} [Lattice α] [AddGroup α] :
PosPart α

The positive part of an element `a` in a lattice ordered group is `a ⊔ 0`, denoted `a⁺`.

Equations

- instPosPart = { posPart := fun (a : α) => a ⊔ 0 }

source
instance instLeOnePart {α : Type u_1} [Lattice α] [Group α] :
LeOnePart α

The negative part of an element `a` in a lattice ordered group is `a⁻¹ ⊔ 1`, denoted `a⁻ᵐ` .

Equations

- instLeOnePart = { leOnePart := fun (a : α) => a⁻¹ ⊔ 1 }

source
instance instNegPart {α : Type u_1} [Lattice α] [AddGroup α] :
NegPart α

The negative part of an element `a` in a lattice ordered group is `(-a) ⊔ 0`, denoted `a⁻`.

Equations

- instNegPart = { negPart := fun (a : α) => -a ⊔ 0 }

source
theorem leOnePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) :
a⁻ᵐ = a⁻¹ ⊔ 1
source
theorem negPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
a⁻ = -a ⊔ 0
source
theorem oneLePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) :
a⁺ᵐ = a ⊔ 1
source
theorem posPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
a⁺ = a ⊔ 0
source
theorem oneLePart_mono {α : Type u_1} [Lattice α] [Group α] :
Monotone fun (x : α) => x⁺ᵐ
source
theorem posPart_mono {α : Type u_1} [Lattice α] [AddGroup α] :
Monotone fun (x : α) => x⁺
source
@[simp]
theorem oneLePart_one {α : Type u_1} [Lattice α] [Group α] :
1⁺ᵐ = 1
source
@[simp]
theorem posPart_zero {α : Type u_1} [Lattice α] [AddGroup α] :
0⁺ = 0
source
@[simp]
theorem leOnePart_one {α : Type u_1} [Lattice α] [Group α] :
1⁻ᵐ = 1
source
@[simp]
theorem negPart_zero {α : Type u_1} [Lattice α] [AddGroup α] :
0⁻ = 0
source
theorem one_le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
1 ≤ a⁺ᵐ
source
theorem posPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
0 ≤ a⁺
source
theorem one_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
1 ≤ a⁻ᵐ
source
theorem negPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
0 ≤ a⁻
source
theorem le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
a ≤ a⁺ᵐ
source
theorem le_posPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
a ≤ a⁺
source
theorem inv_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
a⁻¹ ≤ a⁻ᵐ
source
theorem neg_le_negPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
-a ≤ a⁻
source
@[simp]
theorem oneLePart_eq_self {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁺ᵐ = a ↔ 1 ≤ a
source
@[simp]
theorem posPart_eq_self {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁺ = a ↔ 0 ≤ a
source
@[simp]
theorem oneLePart_eq_one {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁺ᵐ = 1 ↔ a ≤ 1
source
@[simp]
theorem posPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁺ = 0 ↔ a ≤ 0
source
@[simp]
theorem oneLePart_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} :
1 ≤ a → a⁺ᵐ = a

Alias of the reverse direction of `oneLePart_eq_self`.

source
@[simp]
theorem posPart_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
0 ≤ a → a⁺ = a
source
@[simp]
theorem oneLePart_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} :
a ≤ 1 → a⁺ᵐ = 1

Alias of the reverse direction of `oneLePart_eq_one`.

source
@[simp]
theorem posPart_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a ≤ 0 → a⁺ = 0
source
theorem leOnePart_eq_inv' {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹

See also `leOnePart_eq_inv`.

source
theorem negPart_eq_neg' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁻ = -a ↔ 0 ≤ -a

See also `negPart_eq_neg`.

source
theorem leOnePart_eq_one' {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1

See also `leOnePart_eq_one`.

source
theorem negPart_eq_zero' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁻ = 0 ↔ -a ≤ 0

See also `negPart_eq_zero`.

source
theorem oneLePart_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁺ᵐ ≤ 1 ↔ a ≤ 1
source
theorem posPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁺ ≤ 0 ↔ a ≤ 0
source
theorem leOnePart_le_one' {α : Type u_1} [Lattice α] [Group α] {a : α} :
a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

See also `leOnePart_le_one`.

source
theorem negPart_nonpos' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} :
a⁻ ≤ 0 ↔ -a ≤ 0

See also `negPart_nonpos`.

source
@[simp]
theorem one_lt_oneLePart {α : Type u_1} [Lattice α] [Group α] {a : α} (ha : 1 < a) :
1 < a⁺ᵐ
source
@[simp]
theorem posPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} (ha : 0 < a) :
0 < a⁺
source
@[simp]
theorem oneLePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) :
a⁻¹⁺ᵐ = a⁻ᵐ
source
@[simp]
theorem posPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
(-a)⁺ = a⁻
source
@[simp]
theorem leOnePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) :
a⁻¹⁻ᵐ = a⁺ᵐ
source
@[simp]
theorem negPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
(-a)⁻ = a⁺
source
theorem oneLePart_max {α : Type u_1} [Lattice α] [Group α] (a b : α) :
(a ⊔ b)⁺ᵐ = a⁺ᵐ ⊔ b⁺ᵐ
source
theorem posPart_max {α : Type u_1} [Lattice α] [AddGroup α] (a b : α) :
(a ⊔ b)⁺ = a⁺ ⊔ b⁺
source
@[simp]
theorem leOnePart_eq_inv {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] :
a⁻ᵐ = a⁻¹ ↔ a ≤ 1
source
@[simp]
theorem negPart_eq_neg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] :
a⁻ = -a ↔ a ≤ 0
source
@[simp]
theorem leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] :
a⁻ᵐ = 1 ↔ 1 ≤ a
source
@[simp]
theorem negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] :
a⁻ = 0 ↔ 0 ≤ a
source
@[simp]
theorem leOnePart_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] :
a ≤ 1 → a⁻ᵐ = a⁻¹

Alias of the reverse direction of `leOnePart_eq_inv`.

source
@[simp]
theorem negPart_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] :
a ≤ 0 → a⁻ = -a
source
@[simp]
theorem leOnePart_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] :
1 ≤ a → a⁻ᵐ = 1

Alias of the reverse direction of `leOnePart_eq_one`.

source
@[simp]
theorem negPart_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] :
0 ≤ a → a⁻ = 0
source
theorem leOnePart_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] :
a⁻ᵐ ≤ 1 ↔ 1 ≤ a
source
theorem negPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] :
a⁻ ≤ 0 ↔ 0 ≤ a
source
@[simp]
theorem one_lt_leOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (ha : a < 1) :
1 < a⁻ᵐ
source
@[simp]
theorem negPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (ha : a < 0) :
0 < a⁻
source
@[deprecated one_lt_leOnePart (since := "2025-10-25")]
theorem one_lt_ltOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (ha : a < 1) :
1 < a⁻ᵐ

Alias of `one_lt_leOnePart`.

source
@[simp]
theorem oneLePart_div_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a : α) :
a⁺ᵐ / a⁻ᵐ = a
source
@[simp]
theorem posPart_sub_negPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] (a : α) :
a⁺ - a⁻ = a
source
@[simp]
theorem leOnePart_div_oneLePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a : α) :
a⁻ᵐ / a⁺ᵐ = a⁻¹
source
@[simp]
theorem negPart_sub_posPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] (a : α) :
a⁻ - a⁺ = -a
source
theorem oneLePart_leOnePart_injective {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] :
Function.Injective fun (a : α) => (a⁺ᵐ, a⁻ᵐ)
source
theorem posPart_negPart_injective {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] :
Function.Injective fun (a : α) => (a⁺, a⁻)
source
theorem oneLePart_leOnePart_inj {α : Type u_1} [Lattice α] [Group α] {a b : α} [MulLeftMono α] :
a⁺ᵐ = b⁺ᵐ ∧ a⁻ᵐ = b⁻ᵐ ↔ a = b
source
theorem posPart_negPart_inj {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} [AddLeftMono α] :
a⁺ = b⁺ ∧ a⁻ = b⁻ ↔ a = b
source
theorem leOnePart_anti {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] :
Antitone leOnePart
source
theorem negPart_anti {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] :
Antitone negPart
source
theorem leOnePart_eq_inv_inf_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) :
a⁻ᵐ = (a ⊓ 1)⁻¹
source
theorem negPart_eq_neg_inf_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) :
a⁻ = -(a ⊓ 0)
source
theorem oneLePart_mul_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) :
a⁺ᵐ * a⁻ᵐ = |a|ₘ
source
theorem posPart_add_negPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) :
a⁺ + a⁻ = |a|
source
theorem leOnePart_mul_oneLePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) :
a⁻ᵐ * a⁺ᵐ = |a|ₘ
source
theorem negPart_add_posPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) :
a⁻ + a⁺ = |a|
source
theorem oneLePart_inf_leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) :
a⁺ᵐ ⊓ a⁻ᵐ = 1
source
theorem posPart_inf_negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) :
a⁺ ⊓ a⁻ = 0
source
theorem leOnePart_min {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) :
(a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ
source
theorem negPart_min {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α) :
(a ⊓ b)⁻ = a⁻ ⊔ b⁻
source
theorem sup_eq_mul_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
a ⊔ b = b * (a / b)⁺ᵐ
source
theorem sup_eq_add_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
a ⊔ b = b + (a - b)⁺
source
theorem inf_eq_div_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
a ⊓ b = a / (a / b)⁺ᵐ
source
theorem inf_eq_sub_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
a ⊓ b = a - (a - b)⁺
source
theorem le_iff_oneLePart_leOnePart {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
source
theorem le_iff_posPart_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
source
theorem mabs_mul_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) :
|a|ₘ * a = a⁺ᵐ ^ 2
source
theorem abs_add_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) :
|a| + a = 2 • a⁺
source
theorem mul_mabs_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) :
a * |a|ₘ = a⁺ᵐ ^ 2
source
theorem add_abs_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) :
a + |a| = 2 • a⁺
source
theorem mabs_div_eq_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) :
|a|ₘ / a = a⁻ᵐ ^ 2
source
theorem abs_sub_eq_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) :
|a| - a = 2 • a⁻
source
theorem div_mabs_eq_inv_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) :
a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹
source
theorem sub_abs_eq_neg_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) :
a - |a| = -(2 • a⁻)
source
theorem oneLePart_min {α : Type u_1} [DistribLattice α] [Group α] (a b : α) :
(a ⊓ b)⁺ᵐ = a⁺ᵐ ⊓ b⁺ᵐ
source
theorem posPart_min {α : Type u_1} [DistribLattice α] [AddGroup α] (a b : α) :
(a ⊓ b)⁺ = a⁺ ⊓ b⁺
source
theorem leOnePart_max {α : Type u_1} [DistribLattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) :
(a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ
source
theorem negPart_max {α : Type u_1} [DistribLattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α) :
(a ⊔ b)⁻ = a⁻ ⊓ b⁻
source
theorem oneLePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} :
a⁺ᵐ = if 1 ≤ a then a else 1
source
theorem posPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} :
a⁺ = if 0 ≤ a then a else 0
source
@[simp]
theorem one_lt_oneLePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} :
1 < a⁺ᵐ ↔ 1 < a
source
@[simp]
theorem posPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} :
0 < a⁺ ↔ 0 < a
source
theorem oneLePart_of_one_lt_oneLePart {α : Type u_1} [LinearOrder α] [Group α] {a : α} (ha : 1 < a⁺ᵐ) :
a⁺ᵐ = a
source
theorem posPart_eq_of_posPart_pos {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} (ha : 0 < a⁺) :
a⁺ = a
source
@[simp]
theorem oneLePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a b : α} :
a⁺ᵐ < b ↔ a < b ∧ 1 < b
source
@[simp]
theorem posPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a b : α} :
a⁺ < b ↔ a < b ∧ 0 < b
source
theorem leOnePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] :
a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1
source
theorem negPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] :
a⁻ = if a ≤ 0 then -a else 0
source
@[simp]
theorem one_lt_leOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] :
1 < a⁻ᵐ ↔ a < 1
source
@[simp]
theorem negPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] :
0 < a⁻ ↔ a < 0
source
@[deprecated one_lt_leOnePart_iff (since := "2025-10-25")]
theorem one_lt_ltOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] :
1 < a⁻ᵐ ↔ a < 1

Alias of `one_lt_leOnePart_iff`.

source
@[simp]
theorem leOnePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a b : α} [MulLeftMono α] [MulRightMono α] :
a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b
source
@[simp]
theorem negPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a b : α} [AddLeftMono α] [AddRightMono α] :
a⁻ < b ↔ -b < a ∧ 0 < b
source
@[simp]
theorem Pi.oneLePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) :
f⁺ᵐ i = (f i)⁺ᵐ
source
@[simp]
theorem Pi.posPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f⁺ i = (f i)⁺
source
@[simp]
theorem Pi.leOnePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) :
f⁻ᵐ i = (f i)⁻ᵐ
source
@[simp]
theorem Pi.negPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f⁻ i = (f i)⁻
source
theorem Pi.oneLePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) :
f⁺ᵐ = fun (i : ι) => (f i)⁺ᵐ
source
theorem Pi.posPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) :
f⁺ = fun (i : ι) => (f i)⁺
source
theorem Pi.leOnePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) :
f⁻ᵐ = fun (i : ι) => (f i)⁻ᵐ
source
theorem Pi.negPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) :
f⁻ = fun (i : ι) => (f i)⁻