aeconst_of_aestabilizer_eq_top — Mathlib

English

If the stabilizer of a set s under a group action is top, then s is ae-constant with respect to the averaging measure.

Русский

Если aestabilizer G μ s равен вершине подгруппы, то s является ae-константной относительно ae μ.

LaTeX

$$$\forall G,\alpha,\mu, s\ (NullMeasurableSet\ s\ μ)\to \ aestabilizer\ G\ μ\ s = \top \to\ EventuallyConst\ s\ (ae\ μ)$$$

Lean4

@[to_additive]
theorem _root_.MulAction.aeconst_of_aestabilizer_eq_top (hm : NullMeasurableSet s μ) (h : aestabilizer G μ s = ⊤) :
    EventuallyConst s (ae μ) :=
  aeconst_of_forall_smul_ae_eq G hm <| (Subgroup.eq_top_iff' _).1 h

Похожие утверждения