Theorems · Theorem · measure theory

MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain

∀ {G : Type u_6} {α : Type u_7} {inst : Zero G} {inst_1 : VAdd G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasAddFundamentalDomain._auto_1}
  [self : MeasureTheory.HasAddFundamentalDomain G α ν], ∃ s, MeasureTheory.IsAddFundamentalDomain G s ν

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

6 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

MeasureTheory.HasAddFundamentalDomain