Theorems · Definition · measure theory

MulAction.aestabilizer

(G : Type u_1) →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {x : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) → [MeasureTheory.SMulInvariantMeasure G α μ] → Set α → Subgroup G

A.e. stabilizer of a set under a group action.

Defined in

Mathlib.MeasureTheory.Group.AEStabilizer

Cited by

12 results in Mathlib

Foundations

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

Assumes

GroupMulActionMeasureTheory.SMulInvariantMeasure