Measurability results on groups with a lattice structure. #
Tags #
measurable function, group, lattice operation
theorem
measurable_oneLePart
{α : Type u_1}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableSup α]
:
Measurable oneLePart
theorem
measurable_posPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSup α]
:
Measurable posPart
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.posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableSup α]
(hf : Measurable f)
:
Measurable fun (x : β) => (f x)⁺
theorem
measurable_leOnePart
{α : Type u_1}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableInv α]
[MeasurableSup α]
:
Measurable leOnePart
theorem
measurable_negPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableNeg α]
[MeasurableSup α]
:
Measurable negPart
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.negPart
{α : 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}
[Lattice α]
[Group α]
[MeasurableSpace α]
[MeasurableInv α]
[MeasurableSup₂ α]
:
Measurable mabs
theorem
measurable_abs
{α : Type u_1}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableNeg α]
[MeasurableSup₂ α]
:
Measurable abs
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)
theorem
Measurable.abs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[AddGroup α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[MeasurableNeg α]
[MeasurableSup₂ α]
(hf : Measurable f)
:
Measurable fun (x : β) => |f x|