FLT/Mathlib/MeasureTheory/Group/Action.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma _root_.MeasurableEmbedding.isMulLeftInvariant_comap line 26 source
2. lemma _root_.MeasurableEmbedding.isMulRightInvariant_comap line 49 source
3. instance MeasureTheory.(instance at line 81) line 81 source
4. instance MeasureTheory.(instance at line 85) line 85 source
5. instance MeasureTheory.(instance at line 91) line 91 source
6. lemma MeasureTheory.isMulLeftInvariant_subtypeVal line 96 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Group, MeasurableSpace, Subgroup, MeasurableMul, MeasureTheory.Measure, MeasureTheory.Measure.IsMulLeftInvariant, MeasurableSet, Subtype, Membership.mem, MeasureTheory.Measure.comap

   Proof uses: MeasurableEmbedding, MonoidHom, Subgroup.subtype, MeasurableEmbedding.subtype_coe, MeasurableEmbedding.isMulLeftInvariant_comap

   27 instances, coercions and auxiliary constants left out.

7. lemma MeasureTheory.isMulRightInvariant_subtypeVal line 102 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Group, MeasurableSpace, Subgroup, MeasurableMul, MeasureTheory.Measure, MeasureTheory.Measure.IsMulRightInvariant, MeasurableSet, Subtype, Membership.mem, MeasureTheory.Measure.comap

   Proof uses: MeasurableEmbedding, MonoidHom, Subgroup.subtype, MeasurableEmbedding.subtype_coe, MeasurableEmbedding.isMulRightInvariant_comap

   27 instances, coercions and auxiliary constants left out.

8. lemma MeasureTheory.index_mul_haar_subgroup_eq_haar_subgroup line 108 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Group, MeasurableSpace, Subgroup, MeasurableMul, Subgroup.IsFiniteRelIndex, LE.le, MeasurableSet, MeasureTheory.Measure, MeasureTheory.Measure.IsMulLeftInvariant, Eq, ENNReal, HMul.hMul, Subgroup.relIndex, Set

   Proof uses: Subtype, Membership.mem, MeasureTheory.Measure.comap, MeasureTheory.isMulLeftInvariant_subtypeVal, Subgroup.index, Subgroup.subgroupOf, Set.univ, MeasureTheory.Subgroup.index_mul_measure, measurable_subtype_coe, Subsemigroup, Submonoid.toSubsemigroup, Subgroup.toSubmonoid, Eq.mp, Subgroup.comap, Subgroup.subtype, Set.image, Set.preimage, congrArg, Set.image_preimage_eq_of_subset, Eq.mpr and 11 more

   56 instances, coercions and auxiliary constants left out.

   Tactic trace: 12 steps

   Open to load the checked before-and-after goal states.