Structures · Analysis
MeasurableNeg
We say that a type has MeasurableNeg if x ↦ -x is a measurable function.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Shape
- One type argument · adds measurable_neg
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 by147
- MeasurableNeg.measurable_neg
- Measurable.neg
- MeasurableEquiv.neg
- MeasureTheory.quasiMeasurePreserving_neg
- Measurable.fun_neg
- AEMeasurable.neg
- MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant
- MeasureTheory.convolution_flip
- MeasureTheory.Integrable.convolution_integrand
- MeasureTheory.Measure.measurePreserving_neg
- MeasureTheory.absolutelyContinuous_neg
- MeasureTheory.neg_absolutelyContinuous
- MeasureTheory.IntegrableOn.comp_neg
- MeasureTheory.integral_neg_eq_self
- MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
- MeasureTheory.measure_add_right_null
- MeasureTheory.convolution_eq_swap
- MeasureTheory.Measure.neg_neg
- MeasureTheory.Measure.measurePreserving_sub_left
- MeasureTheory.aemeasurable_lconvolution
- MeasureTheory.quasiMeasurePreserving_add_right
- MeasureTheory.measure_add_lintegral_eq
- AEMeasurable.fun_neg
- MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv
- MeasurableSet.neg
- MeasureTheory.quasiMeasurePreserving_neg_add
- MeasureTheory.Measure.neg_apply
- MeasureTheory.convolutionExistsAt_flip
- MeasureTheory.HaveLebesgueDecomposition.conv
- MeasureTheory.measure_eq_sub_vadd
- MeasureTheory.measurePreserving_add_prod_neg
- MeasureTheory.measurePreserving_prod_neg_add
- MeasureTheory.measurePreserving_prod_neg_add_swap
- MeasureTheory.Integrable.comp_sub_left
- MeasureTheory.measure_neg_null
- MeasurableEquiv.subLeft
- MeasurableEquiv.neg_apply
- measurable_abs
- MeasureTheory.measurePreserving_prod_sub_swap
- MeasureTheory.lintegral_neg_eq_self
- MeasureTheory.AEStronglyMeasurable.convolution_integrand
- MeasureTheory.Integrable.comp_neg
- MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant
- BddAbove.convolutionExistsAt'
- MeasureTheory.IntegrableOn.comp_neg_Iio
- Measurable.add_iff_right
- MeasurableEquiv.shearAddRight
- AEMeasurable.add_iff_right
- MeasureTheory.neg_ae
- MeasureTheory.Measure.measure_neg
Ancestors0
No ancestors.