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
• Bourbaki, Algebra II
• Fuchs, Partially Ordered Algebraic Systems
• Zaanen, Lectures on "Riesz Spaces"
• Banasiak, Banach Lattices in Applications

Tags

positive part, negative part

def 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

• Eq instOneLePart { oneLePart := fun (a : α) => Max.max a 1 }

def 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

• Eq instPosPart { posPart := fun (a : α) => Max.max a 0 }

def 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

• Eq instLeOnePart { leOnePart := fun (a : α) => Max.max (Inv.inv a) 1 }

def 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

• Eq instNegPart { negPart := fun (a : α) => Max.max (Neg.neg a) 0 }

theorem leOnePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) : Eq (LeOnePart.leOnePart a) (Max.max (Inv.inv a) 1)

theorem negPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : Eq (NegPart.negPart a) (Max.max (Neg.neg a) 0)

theorem oneLePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) : Eq (OneLePart.oneLePart a) (Max.max a 1)

theorem posPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : Eq (PosPart.posPart a) (Max.max a 0)

theorem oneLePart_mono {α : Type u_1} [Lattice α] [Group α] : Monotone fun (x : α) => OneLePart.oneLePart x

theorem posPart_mono {α : Type u_1} [Lattice α] [AddGroup α] : Monotone fun (x : α) => PosPart.posPart x

theorem oneLePart_one {α : Type u_1} [Lattice α] [Group α] : Eq (OneLePart.oneLePart 1) 1

theorem posPart_zero {α : Type u_1} [Lattice α] [AddGroup α] : Eq (PosPart.posPart 0) 0

theorem leOnePart_one {α : Type u_1} [Lattice α] [Group α] : Eq (LeOnePart.leOnePart 1) 1

theorem negPart_zero {α : Type u_1} [Lattice α] [AddGroup α] : Eq (NegPart.negPart 0) 0

theorem one_le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) : LE.le 1 (OneLePart.oneLePart a)

theorem posPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : LE.le 0 (PosPart.posPart a)

theorem one_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (a : α) : LE.le 1 (LeOnePart.leOnePart a)

theorem negPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : LE.le 0 (NegPart.negPart a)

theorem le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) : LE.le a (OneLePart.oneLePart a)

theorem le_posPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : LE.le a (PosPart.posPart a)

theorem inv_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (a : α) : LE.le (Inv.inv a) (LeOnePart.leOnePart a)

theorem neg_le_negPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : LE.le (Neg.neg a) (NegPart.negPart a)

theorem oneLePart_eq_self {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (Eq (OneLePart.oneLePart a) a) (LE.le 1 a)

theorem posPart_eq_self {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (Eq (PosPart.posPart a) a) (LE.le 0 a)

theorem oneLePart_eq_one {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (Eq (OneLePart.oneLePart a) 1) (LE.le a 1)

theorem posPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (Eq (PosPart.posPart a) 0) (LE.le a 0)

theorem oneLePart_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} : LE.le 1 a → Eq (OneLePart.oneLePart a) a

Alias of the reverse direction of oneLePart_eq_self.

theorem posPart_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : LE.le 0 a → Eq (PosPart.posPart a) a

theorem oneLePart_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} : LE.le a 1 → Eq (OneLePart.oneLePart a) 1

Alias of the reverse direction of oneLePart_eq_one.

theorem posPart_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : LE.le a 0 → Eq (PosPart.posPart a) 0

theorem leOnePart_eq_inv' {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (Eq (LeOnePart.leOnePart a) (Inv.inv a)) (LE.le 1 (Inv.inv a))

See also leOnePart_eq_inv.

theorem negPart_eq_neg' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (Eq (NegPart.negPart a) (Neg.neg a)) (LE.le 0 (Neg.neg a))

See also negPart_eq_neg.

theorem leOnePart_eq_one' {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (Eq (LeOnePart.leOnePart a) 1) (LE.le (Inv.inv a) 1)

See also leOnePart_eq_one.

theorem negPart_eq_zero' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (Eq (NegPart.negPart a) 0) (LE.le (Neg.neg a) 0)

See also negPart_eq_zero.

theorem oneLePart_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (LE.le (OneLePart.oneLePart a) 1) (LE.le a 1)

theorem posPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (LE.le (PosPart.posPart a) 0) (LE.le a 0)

theorem leOnePart_le_one' {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (LE.le (LeOnePart.leOnePart a) 1) (LE.le (Inv.inv a) 1)

See also leOnePart_le_one.

theorem negPart_nonpos' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (LE.le (NegPart.negPart a) 0) (LE.le (Neg.neg a) 0)

See also negPart_nonpos.

theorem leOnePart_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} : Iff (LE.le (LeOnePart.leOnePart a) 1) (LE.le (Inv.inv a) 1)

theorem negPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : Iff (LE.le (NegPart.negPart a) 0) (LE.le (Neg.neg a) 0)

theorem one_lt_oneLePart {α : Type u_1} [Lattice α] [Group α] {a : α} (ha : LT.lt 1 a) : LT.lt 1 (OneLePart.oneLePart a)

theorem posPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} (ha : LT.lt 0 a) : LT.lt 0 (PosPart.posPart a)

theorem oneLePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) : Eq (OneLePart.oneLePart (Inv.inv a)) (LeOnePart.leOnePart a)

theorem posPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : Eq (PosPart.posPart (Neg.neg a)) (NegPart.negPart a)

theorem leOnePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) : Eq (LeOnePart.leOnePart (Inv.inv a)) (OneLePart.oneLePart a)

theorem negPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : Eq (NegPart.negPart (Neg.neg a)) (PosPart.posPart a)

theorem leOnePart_eq_inv {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : Iff (Eq (LeOnePart.leOnePart a) (Inv.inv a)) (LE.le a 1)

theorem negPart_eq_neg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : Iff (Eq (NegPart.negPart a) (Neg.neg a)) (LE.le a 0)

theorem leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : Iff (Eq (LeOnePart.leOnePart a) 1) (LE.le 1 a)

theorem negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : Iff (Eq (NegPart.negPart a) 0) (LE.le 0 a)

theorem leOnePart_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : LE.le a 1 → Eq (LeOnePart.leOnePart a) (Inv.inv a)

Alias of the reverse direction of leOnePart_eq_inv.

theorem negPart_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : LE.le a 0 → Eq (NegPart.negPart a) (Neg.neg a)

theorem leOnePart_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : LE.le 1 a → Eq (LeOnePart.leOnePart a) 1

Alias of the reverse direction of leOnePart_eq_one.

theorem negPart_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : LE.le 0 a → Eq (NegPart.negPart a) 0

theorem one_lt_ltOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (ha : LT.lt a 1) : LT.lt 1 (LeOnePart.leOnePart a)

theorem negPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (ha : LT.lt a 0) : LT.lt 0 (NegPart.negPart a)

theorem oneLePart_div_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a : α) : Eq (HDiv.hDiv (OneLePart.oneLePart a) (LeOnePart.leOnePart a)) a

theorem posPart_sub_negPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] (a : α) : Eq (HSub.hSub (PosPart.posPart a) (NegPart.negPart a)) a

theorem leOnePart_div_oneLePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a : α) : Eq (HDiv.hDiv (LeOnePart.leOnePart a) (OneLePart.oneLePart a)) (Inv.inv a)

theorem negPart_sub_posPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] (a : α) : Eq (HSub.hSub (NegPart.negPart a) (PosPart.posPart a)) (Neg.neg a)

theorem oneLePart_leOnePart_injective {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] : Function.Injective fun (a : α) => { fst := OneLePart.oneLePart a, snd := LeOnePart.leOnePart a }

theorem posPart_negPart_injective {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] : Function.Injective fun (a : α) => { fst := PosPart.posPart a, snd := NegPart.negPart a }

theorem oneLePart_leOnePart_inj {α : Type u_1} [Lattice α] [Group α] {a b : α} [MulLeftMono α] : Iff (And (Eq (OneLePart.oneLePart a) (OneLePart.oneLePart b)) (Eq (LeOnePart.leOnePart a) (LeOnePart.leOnePart b))) (Eq a b)

theorem posPart_negPart_inj {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} [AddLeftMono α] : Iff (And (Eq (PosPart.posPart a) (PosPart.posPart b)) (Eq (NegPart.negPart a) (NegPart.negPart b))) (Eq a b)

theorem leOnePart_anti {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] : Antitone LeOnePart.leOnePart

theorem negPart_anti {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] : Antitone NegPart.negPart

theorem leOnePart_eq_inv_inf_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : Eq (LeOnePart.leOnePart a) (Inv.inv (Min.min a 1))

theorem negPart_eq_neg_inf_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : Eq (NegPart.negPart a) (Neg.neg (Min.min a 0))

theorem oneLePart_mul_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : Eq (HMul.hMul (OneLePart.oneLePart a) (LeOnePart.leOnePart a)) (mabs a)

theorem posPart_add_negPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : Eq (HAdd.hAdd (PosPart.posPart a) (NegPart.negPart a)) (abs a)

theorem leOnePart_mul_oneLePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : Eq (HMul.hMul (LeOnePart.leOnePart a) (OneLePart.oneLePart a)) (mabs a)

theorem negPart_add_posPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : Eq (HAdd.hAdd (NegPart.negPart a) (PosPart.posPart a)) (abs a)

theorem oneLePart_inf_leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : Eq (Min.min (OneLePart.oneLePart a) (LeOnePart.leOnePart a)) 1

theorem posPart_inf_negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : Eq (Min.min (PosPart.posPart a) (NegPart.negPart a)) 0

theorem sup_eq_mul_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : Eq (Max.max a b) (HMul.hMul b (OneLePart.oneLePart (HDiv.hDiv a b)))

theorem sup_eq_add_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : Eq (Max.max a b) (HAdd.hAdd b (PosPart.posPart (HSub.hSub a b)))

theorem inf_eq_div_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : Eq (Min.min a b) (HDiv.hDiv a (OneLePart.oneLePart (HDiv.hDiv a b)))

theorem inf_eq_sub_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : Eq (Min.min a b) (HSub.hSub a (PosPart.posPart (HSub.hSub a b)))

theorem le_iff_oneLePart_leOnePart {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : Iff (LE.le a b) (And (LE.le (OneLePart.oneLePart a) (OneLePart.oneLePart b)) (LE.le (LeOnePart.leOnePart b) (LeOnePart.leOnePart a)))

theorem le_iff_posPart_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : Iff (LE.le a b) (And (LE.le (PosPart.posPart a) (PosPart.posPart b)) (LE.le (NegPart.negPart b) (NegPart.negPart a)))

theorem mabs_mul_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : Eq (HMul.hMul (mabs a) a) (HPow.hPow (OneLePart.oneLePart a) 2)

theorem abs_add_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : Eq (HAdd.hAdd (abs a) a) (HSMul.hSMul 2 (PosPart.posPart a))

theorem mul_mabs_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : Eq (HMul.hMul a (mabs a)) (HPow.hPow (OneLePart.oneLePart a) 2)

theorem add_abs_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : Eq (HAdd.hAdd a (abs a)) (HSMul.hSMul 2 (PosPart.posPart a))

theorem mabs_div_eq_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : Eq (HDiv.hDiv (mabs a) a) (HPow.hPow (LeOnePart.leOnePart a) 2)

theorem abs_sub_eq_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : Eq (HSub.hSub (abs a) a) (HSMul.hSMul 2 (NegPart.negPart a))

theorem div_mabs_eq_inv_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : Eq (HDiv.hDiv a (mabs a)) (Inv.inv (HPow.hPow (LeOnePart.leOnePart a) 2))

theorem sub_abs_eq_neg_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : Eq (HSub.hSub a (abs a)) (Neg.neg (HSMul.hSMul 2 (NegPart.negPart a)))

theorem oneLePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} : Eq (OneLePart.oneLePart a) (ite (LE.le 1 a) a 1)

theorem posPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} : Eq (PosPart.posPart a) (ite (LE.le 0 a) a 0)

theorem one_lt_oneLePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} : Iff (LT.lt 1 (OneLePart.oneLePart a)) (LT.lt 1 a)

theorem posPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} : Iff (LT.lt 0 (PosPart.posPart a)) (LT.lt 0 a)

theorem oneLePart_of_one_lt_oneLePart {α : Type u_1} [LinearOrder α] [Group α] {a : α} (ha : LT.lt 1 (OneLePart.oneLePart a)) : Eq (OneLePart.oneLePart a) a

theorem posPart_eq_of_posPart_pos {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} (ha : LT.lt 0 (PosPart.posPart a)) : Eq (PosPart.posPart a) a

theorem oneLePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a b : α} : Iff (LT.lt (OneLePart.oneLePart a) b) (And (LT.lt a b) (LT.lt 1 b))

theorem posPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a b : α} : Iff (LT.lt (PosPart.posPart a) b) (And (LT.lt a b) (LT.lt 0 b))

theorem leOnePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] : Eq (LeOnePart.leOnePart a) (ite (LE.le a 1) (Inv.inv a) 1)

theorem negPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] : Eq (NegPart.negPart a) (ite (LE.le a 0) (Neg.neg a) 0)

theorem one_lt_ltOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] : Iff (LT.lt 1 (LeOnePart.leOnePart a)) (LT.lt a 1)

theorem negPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] : Iff (LT.lt 0 (NegPart.negPart a)) (LT.lt a 0)

theorem leOnePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a b : α} [MulLeftMono α] [MulRightMono α] : Iff (LT.lt (LeOnePart.leOnePart a) b) (And (LT.lt (Inv.inv b) a) (LT.lt 1 b))

theorem negPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a b : α} [AddLeftMono α] [AddRightMono α] : Iff (LT.lt (NegPart.negPart a) b) (And (LT.lt (Neg.neg b) a) (LT.lt 0 b))

theorem Pi.oneLePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) : Eq (OneLePart.oneLePart f i) (OneLePart.oneLePart (f i))

theorem Pi.posPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) : Eq (PosPart.posPart f i) (PosPart.posPart (f i))

theorem Pi.leOnePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) : Eq (LeOnePart.leOnePart f i) (LeOnePart.leOnePart (f i))

theorem Pi.negPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) : Eq (NegPart.negPart f i) (NegPart.negPart (f i))

theorem Pi.oneLePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) : Eq (OneLePart.oneLePart f) fun (i : ι) => OneLePart.oneLePart (f i)

theorem Pi.posPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) : Eq (PosPart.posPart f) fun (i : ι) => PosPart.posPart (f i)

theorem Pi.leOnePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) : Eq (LeOnePart.leOnePart f) fun (i : ι) => LeOnePart.leOnePart (f i)

theorem Pi.negPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) : Eq (NegPart.negPart f) fun (i : ι) => NegPart.negPart (f i)