LIntegral

📁 Source: Mathlib/MeasureTheory/Group/LIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems lintegral_add_left_eq_self, lintegral_add_right_eq_self, lintegral_div_left_eq_self, lintegral_div_right_eq_self, lintegral_eq_zero_of_isAddLeftInvariant, lintegral_eq_zero_of_isMulLeftInvariant, lintegral_inv_eq_self, lintegral_mul_left_eq_self, lintegral_mul_right_eq_self, lintegral_neg_eq_self, lintegral_sub_left_eq_self, lintegral_sub_right_eq_self	12
Total	12

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_add_left_eq_self 📖	mathematical	—	lintegral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	map_add_left_eq_self lintegral_map_equiv
lintegral_add_right_eq_self 📖	mathematical	—	lintegral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	map_add_right_eq_self lintegral_map_equiv
lintegral_div_left_eq_self 📖	mathematical	—	lintegral DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv lintegral_inv_eq_self lintegral_mul_left_eq_self
lintegral_div_right_eq_self 📖	mathematical	—	lintegral DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv lintegral_mul_right_eq_self
lintegral_eq_zero_of_isAddLeftInvariant 📖	mathematical	Continuous ENNReal ENNReal.instTopologicalSpace	lintegral instZeroENNReal Pi.instZero	—	Measure.instOuterMeasureClass lintegral_eq_zero_iff Continuous.measurable BorelSpace.opensMeasurable ENNReal.borelSpace Continuous.ae_eq_iff_eq ENNReal.instT2Space isOpenPosMeasure_of_addLeftInvariant_of_regular continuous_zero
lintegral_eq_zero_of_isMulLeftInvariant 📖	mathematical	Continuous ENNReal ENNReal.instTopologicalSpace	lintegral instZeroENNReal Pi.instZero	—	Measure.instOuterMeasureClass lintegral_eq_zero_iff Continuous.measurable BorelSpace.opensMeasurable ENNReal.borelSpace Continuous.ae_eq_iff_eq ENNReal.instT2Space isOpenPosMeasure_of_mulLeftInvariant_of_regular continuous_zero
lintegral_inv_eq_self 📖	mathematical	—	lintegral InvolutiveInv.toInv	—	Measure.map_inv_eq_self lintegral_map_equiv
lintegral_mul_left_eq_self 📖	mathematical	—	lintegral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	map_mul_left_eq_self lintegral_map_equiv
lintegral_mul_right_eq_self 📖	mathematical	—	lintegral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	map_mul_right_eq_self lintegral_map_equiv
lintegral_neg_eq_self 📖	mathematical	—	lintegral InvolutiveNeg.toNeg	—	Measure.map_neg_eq_self lintegral_map_equiv
lintegral_sub_left_eq_self 📖	mathematical	—	lintegral SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg lintegral_neg_eq_self lintegral_add_left_eq_self
lintegral_sub_right_eq_self 📖	mathematical	—	lintegral SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg lintegral_add_right_eq_self

---

← Back to Index