Theorems · Theorem · measure theory

MeasureTheory.fundamentalInterior_smul

∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Group H]
  [inst_3 : MulAction H α] [SMulCommClass H G α] (g : H),
  MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionGroupMulActionSMulCommClass