Theorems · Definition · measure theory

TopologicalAddGroup.IsSES.inducedMeasure

{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : AddGroup A] →
        [inst_1 : AddGroup B] →
          [inst_2 : AddGroup C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace C] →
                  {φ : A →+ B} →
                    {ψ : B →+ C} →
                      TopologicalAddGroup.IsSES φ ψ →
                        [IsTopologicalAddGroup A] →
                          [IsTopologicalAddGroup B] →
                            [inst_8 : MeasurableSpace A] →
                              [BorelSpace A] →
                                (μA : MeasureTheory.Measure A) →
                                  [hμA : μA.IsAddHaarMeasure] →
                                    [IsTopologicalAddGroup C] →
                                      [LocallyCompactSpace B] →
                                        [inst : MeasurableSpace C] →
                                          [BorelSpace C] →
                                            (μC : MeasureTheory.Measure C) →
                                              [hμC : μC.IsAddHaarMeasure] →
                                                [T2Space B] →
                                                  [inst : MeasurableSpace B] → [BorelSpace B] → MeasureTheory.Measure B

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive 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

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroupTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasureIsTopologicalAddGroupLocallyCompactSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasureT2SpaceMeasurableSpaceBorelSpace