Structures · Analysis
MeasureTheory.Measure.IsInvInvariant
A measure is invariant under inversion if μ⁻¹ = μ. Equivalently, this means that for all
measurable A we have μ (A⁻¹) = μ A, where A⁻¹ is the pointwise inverse of A.
- Defined in
- Mathlib.MeasureTheory.Group.Measure
- Shape
- One type argument · adds inv_eq_self
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 by27
- MeasureTheory.Measure.map_inv_eq_self
- MeasureTheory.IntegrableOn.comp_inv
- MeasureTheory.lintegral_inv_eq_self
- MeasureTheory.Measure.measurePreserving_div_left
- MeasureTheory.Measure.IsInvInvariant.inv_eq_self
- MeasureTheory.Measure.measurePreserving_inv
- MeasureTheory.Measure.measure_inv
- MeasureTheory.Measure.map_div_left_eq_self
- MeasureTheory.Integrable.comp_inv
- MeasureTheory.Integrable.comp_div_left
- MeasureTheory.integral_inv_eq_self
- MeasureTheory.Measure.measurePreserving_mul_right_inv
- MeasureTheory.Measure.inv_eq_self
- MeasureTheory.integrable_comp_div_left
- MeasureTheory.IntegrableOn.comp_inv_Iio
- MeasureTheory.Measure.map_div_left_ae
- MeasureTheory.IntegrableOn.comp_inv_Ioi
- MeasureTheory.lintegral_div_left_eq_self
- MeasureTheory.mlconvolution_comm
- MeasureTheory.IntegrableOn.comp_inv_Ici
- MeasureTheory.integral_div_left_eq_self
- MeasureTheory.Measure.pi.isInvInvariant
- MeasureTheory.Pi.isInvInvariant_volume
- MeasureTheory.Measure.measure_preimage_inv
- MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite
- MeasureTheory.IntegrableOn.comp_inv_Iic
- MeasureTheory.Measure.map_mul_right_inv_eq_self
Ancestors0
No ancestors.