Theorems · Theorem · Lie groups
MeasureTheory.isMulLeftInvariant_map
∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G]
{H : Type u_3} [inst_3 : MeasurableSpace H] [inst_4 : Mul H] [MeasurableMul H] [μ.IsMulLeftInvariant] (f : G →ₙ* H),
Measurable ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsMulLeftInvariant- Defined in
- Mathlib.MeasureTheory.Group.Measure
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Measurablestatement and proof · cited by 1,499
- map_mulproof · cited by 1,137
- MeasureTheory.Measure.mapstatement and proof · cited by 858
- MulHomstatement and proof · cited by 299
- MeasureTheory.Measure.IsMulLeftInvariantstatement and proof · cited by 118
- MeasurableMulstatement and proof · cited by 71
- MeasureTheory.Measure.map_mapproof · cited by 67
- MeasurableMul.measurable_const_mulproof · cited by 12
- MeasureTheory.map_mul_left_eq_selfproof · cited by 9
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasureproof · cited by 1
- MeasureTheory.Measure.isHaarMeasure_mapproof · cited by 1