Structures · Analysis
MeasureTheory.HasAddFundamentalDomain
We say a quotient of α by G HasAddFundamentalDomain if there is a measurable set
s for which IsAddFundamentalDomain G s holds.
- Shape
- 3 explicit arguments · adds ExistsIsAddFundamentalDomain
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.unique
- MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage
Ancestors0
No ancestors.