Theorems · Definition · measure theory
MeasurableEquiv.addRight
{G : Type u_1} → [inst : AddGroup G] → [inst_1 : MeasurableSpace G] → [MeasurableAdd G] → G → G ≃ᵐ GIf G is an additive group with measurable addition, then addition of g : G
on the right is a measurable automorphism of G.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- Equivproof · cited by 8,337
- AddGroupstatement and proof · cited by 4,410
- MeasurableEquivstatement · cited by 269
- MeasurableAddstatement and proof · cited by 78
- Equiv.addRightproof · cited by 30
Cited by8
Results whose statement or proof uses this declaration.
- MeasureTheory.integral_add_right_eq_selfproof · cited by 7
- MeasureTheory.measure_preimage_add_rightproof · cited by 3
- MeasureTheory.lintegral_add_right_eq_selfproof · cited by 2
- MeasureTheory.map_add_right_aeproof · cited by 1
- MeasurableEquiv.coe_addRightstatement · cited by 0
- measurableEmbedding_addRightproof · cited by 0
- MeasurableEquiv.toEquiv_addRightstatement · cited by 0
- MeasurableEquiv.symm_addRightstatement · cited by 0