Structures · Analysis
MeasureTheory.HasFundamentalDomain
We say a quotient of α by G HasFundamentalDomain if there is a measurable set s for
which IsFundamentalDomain G s holds.
- Shape
- 3 explicit arguments · adds ExistsIsFundamentalDomain
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
- MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
- MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage
- MeasureTheory.QuotientMeasureEqMeasurePreimage.unique
- MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume
- MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient
- MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient
Ancestors0
No ancestors.