Theorems · Theorem · measure theory

MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain

∀ {G : Type u_6} {α : Type u_7} {inst : One G} {inst_1 : SMul G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasFundamentalDomain._auto_1}
  [self : MeasureTheory.HasFundamentalDomain G α ν], ∃ s, MeasureTheory.IsFundamentalDomain 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.HasFundamentalDomain