# Measurability results on groups with a lattice structure. #

## Tags #

measurable function, group, lattice operation

theorem
measurable_posPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSup α]
:

Measurable posPart

theorem
measurable_oneLePart
{α : Type u_1}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableSup α]
:

Measurable oneLePart

theorem
Measurable.posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableSup α]
(hf : Measurable f)
:

Measurable fun (x : β) => (f x)⁺

theorem
Measurable.oneLePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableSup α]
(hf : Measurable f)
:

Measurable fun (x : β) => (f x)⁺ᵐ

theorem
measurable_negPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableNeg α]
[MeasurableSup α]
:

Measurable negPart

theorem
measurable_leOnePart
{α : Type u_1}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableInv α]
[MeasurableSup α]
:

Measurable leOnePart

theorem
Measurable.negPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableNeg α]
[MeasurableSup α]
(hf : Measurable f)
:

Measurable fun (x : β) => (f x)⁻

theorem
Measurable.leOnePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableInv α]
[MeasurableSup α]
(hf : Measurable f)
:

Measurable fun (x : β) => (f x)⁻ᵐ

theorem
measurable_abs
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableNeg α]
[MeasurableSup₂ α]
:

Measurable abs

theorem
measurable_mabs
{α : Type u_1}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableInv α]
[MeasurableSup₂ α]
:

Measurable mabs

theorem
Measurable.abs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableNeg α]
[MeasurableSup₂ α]
(hf : Measurable f)
:

Measurable fun (x : β) => |f x|

theorem
Measurable.mabs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableInv α]
[MeasurableSup₂ α]
(hf : Measurable f)
:

Measurable fun (x : β) => mabs (f x)