Theorems · Theorem · measure theory

MeasureTheory.addFundamentalFrontier_vadd

∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α)
  [inst_2 : AddGroup H] [inst_3 : AddAction H α] [VAddCommClass H G α] (g : H),
  MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier G s

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddGroupAddActionVAddCommClass