Theorems · Theorem · dynamical systems

MeasureTheory.aeconst_of_forall_vadd_ae_eq

∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : AddGroup G]
  [inst_1 : AddAction G α] [ErgodicVAdd G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (∀ (g : G), g +ᵥ s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)

Defined in: Mathlib.Dynamics.Ergodic.Action.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup AddAction ErgodicVAdd

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
AddGroupstatement and proof · cited by 4,410
MeasureTheory.aestatement and proof · cited by 2,352
Filter.EventuallyEqstatement and proof · cited by 1,912
HVAdd.hVAddstatement and proof · cited by 1,820
AddActionstatement and proof · cited by 820
Set.vaddSetstatement · cited by 403
MeasureTheory.NullMeasurableSetstatement and proof · cited by 337
Filter.EventuallyConststatement · cited by 93
Set.preimage_vaddproof · cited by 14

Cited by1

Results whose statement or proof uses this declaration.

AddAction.aeconst_of_aestabilizer_eq_topproof · cited by 0