Map

📁 Source: Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean

Statistics

Metric	Count
Definitions	0
Theorems lintegral_map, lintegral_comp, lintegral_comp_emb, lintegral_map_equiv, setLIntegral_comp_emb, setLIntegral_comp_preimage, setLIntegral_comp_preimage_emb, lintegral_comp, lintegral_indicator_const_comp, lintegral_map, lintegral_map', lintegral_map_equiv, lintegral_map_le, lintegral_subtype_comap, setLIntegral_map, setLIntegral_subtype	16
Total	16

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_map 📖	mathematical	MeasurableEmbedding	MeasureTheory.lintegral MeasureTheory.Measure.map	—	MeasureTheory.lintegral_def le_antisymm iSup₂_le measurable MeasureTheory.SimpleFunc.lintegral_map le_iSup_of_le le_iSup MeasureTheory.SimpleFunc.extend_comp_eq MeasureTheory.SimpleFunc.lintegral_eq_lintegral MeasureTheory.lintegral_mono_ae MeasureTheory.Measure.instOuterMeasureClass ae_map_iff Filter.Eventually.of_forall Eq.trans_le MeasureTheory.SimpleFunc.extend_apply

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_comp 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.map	—	lintegral_map
lintegral_indicator_const_comp 📖	mathematical	Measurable MeasurableSet	lintegral Set.indicator ENNReal instZeroENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.preimage	—	lintegral_comp Measurable.indicator measurable_const lintegral_indicator_const Measure.map_apply
lintegral_map 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.map	—	lintegral_eq_iSup_eapprox_lintegral Measurable.comp SimpleFunc.ext SimpleFunc.eapprox_comp SimpleFunc.lintegral_map
lintegral_map' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.map	lintegral	—	lintegral_congr_ae Measure.map_congr lintegral_map Filter.EventuallyEq.fun_comp Measure.instOuterMeasureClass Filter.EventuallyEq.symm ae_eq_comp
lintegral_map_equiv 📖	mathematical	—	lintegral Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike	—	MeasurableEmbedding.lintegral_map MeasurableEquiv.measurableEmbedding
lintegral_map_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.map	—	iSup_lintegral_measurable_le_eq_lintegral iSup₂_le iSup_le lintegral_map' Measurable.aemeasurable lintegral_mono Measure.map_of_not_aemeasurable lintegral_zero_measure ENNReal.instCanonicallyOrderedAdd
lintegral_subtype_comap 📖	mathematical	MeasurableSet	lintegral Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Measure.comap Measure.restrict	—	MeasurableEmbedding.lintegral_map MeasurableEmbedding.subtype_coe map_comap_subtype_coe
setLIntegral_map 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.restrict Measure.map Set.preimage	—	Measure.restrict_map lintegral_map
setLIntegral_subtype 📖	mathematical	MeasurableSet	lintegral Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Measure.restrict Measure.comap Set.image	—	MeasurableEmbedding.restrict_comap MeasurableEmbedding.subtype_coe lintegral_subtype_comap Measure.restrict_restrict Set.inter_eq_right Subtype.coe_image_subset

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_comp 📖	mathematical	MeasureTheory.MeasurePreserving Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral	—	map_eq MeasureTheory.lintegral_map measurable
lintegral_comp_emb 📖	mathematical	MeasureTheory.MeasurePreserving MeasurableEmbedding	MeasureTheory.lintegral	—	map_eq MeasurableEmbedding.lintegral_map
lintegral_map_equiv 📖	mathematical	MeasureTheory.MeasurePreserving DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike	MeasureTheory.lintegral	—	MeasureTheory.lintegral_map_equiv map_eq
setLIntegral_comp_emb 📖	mathematical	MeasureTheory.MeasurePreserving MeasurableEmbedding	MeasureTheory.lintegral MeasureTheory.Measure.restrict Set.image	—	setLIntegral_comp_preimage_emb Set.preimage_image_eq MeasurableEmbedding.injective
setLIntegral_comp_preimage 📖	mathematical	MeasureTheory.MeasurePreserving MeasurableSet Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral MeasureTheory.Measure.restrict Set.preimage	—	map_eq MeasureTheory.setLIntegral_map measurable
setLIntegral_comp_preimage_emb 📖	mathematical	MeasureTheory.MeasurePreserving MeasurableEmbedding	MeasureTheory.lintegral MeasureTheory.Measure.restrict Set.preimage	—	map_eq MeasurableEmbedding.restrict_map MeasurableEmbedding.lintegral_map

---

← Back to Index