∀ {M : Type u_1} {X : Type u_2} [inst : AddMonoid M] [inst_1 : VAdd M X] [inst_2 : TopologicalSpace X] [R1Space X]
  [inst_4 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] (N : Type u_3) [inst_8 : AddAction M N] [inst_9 : AddMonoid N] [inst_10 : TopologicalSpace N]
  [AddAction.IsMinimal M N] [inst_12 : AddAction N X] [VAddAssocClass M N X] [ContinuousVAdd N X] [ErgodicVAdd N X μ],
  ErgodicVAdd M X μ