Theorems · Definition · measure theory

TopologicalGroup.IsSES.inducedMeasure

{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Group A] →
        [inst_1 : Group B] →
          [inst_2 : Group C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace C] →
                  {φ : A →* B} →
                    {ψ : B →* C} →
                      TopologicalGroup.IsSES φ ψ →
                        [IsTopologicalGroup A] →
                          [IsTopologicalGroup B] →
                            [inst_8 : MeasurableSpace A] →
                              [BorelSpace A] →
                                (μA : MeasureTheory.Measure A) →
                                  [hμA : μA.IsHaarMeasure] →
                                    [IsTopologicalGroup C] →
                                      [LocallyCompactSpace B] →
                                        [inst : MeasurableSpace C] →
                                          [BorelSpace C] →
                                            (μC : MeasureTheory.Measure C) →
                                              [hμC : μC.IsHaarMeasure] →
                                                [T2Space B] →
                                                  [inst : MeasurableSpace B] → [BorelSpace B] → MeasureTheory.Measure B

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, then we can define a Haar measure on B induced by the Haar measures on A and C.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Extension

Cited by

3 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupGroupTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalGroupIsTopologicalGroupMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsHaarMeasureIsTopologicalGroupLocallyCompactSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsHaarMeasureT2SpaceMeasurableSpaceBorelSpace