English
If every set invariant under aestabilizer is ae-constant, then the action of G on X is ergodic.
Русский
Если aestabilizer G μ s верен для всех множества s тогда ergodicSMul G X μ.
LaTeX
$$$\forall G\, X\, μ,\ (\forall s, MeasurableSet s \to (Eq (MulAction.aestabilizer G μ s) Top) \to\ EventuallyConst\ s\ (ae\ μ)) \to ErgodicSMul G X μ$$$
Lean4
theorem _root_.ErgodicSMul.of_aestabilizer [Group G] [MulAction G α] [SMulInvariantMeasure G α μ]
(h : ∀ s, MeasurableSet s → aestabilizer G μ s = ⊤ → EventuallyConst s (ae μ)) : ErgodicSMul G α μ :=
⟨fun hm hs ↦ h _ hm <| (Subgroup.eq_top_iff' _).2 fun g ↦ by simpa only [preimage_smul_inv] using hs g⁻¹⟩