Comap

📁 Source: Mathlib/MeasureTheory/Measure/Comap.lean

Statistics

Metric	Count
Definitions comap, comapₗ	2
Theorems comap_add, comap_symm, map_symm, image, ae_eq_image_of_ae_eq_comap, comap_apply, comap_apply_le, comap_apply₀, comap_comap, comap_id, comap_preimage, comap_smul, comap_swap, comap_undef, comap_zero, comapₗ_apply, comapₗ_eq_comap, le_comap_apply, measure_image_eq_zero_of_comap_eq_zero	19
Total	21

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_add 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.comap MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	MeasureTheory.Measure.ext IsScalarTower.right MeasureTheory.Measure.comapₗ_eq_comap injective measurableSet_image map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_symm 📖	mathematical	—	MeasureTheory.Measure.comap DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm MeasureTheory.Measure.map	—	MeasureTheory.Measure.ext map_apply MeasureTheory.Measure.comap_apply injective measurableSet_image image_symm
map_symm 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm MeasureTheory.Measure.comap	—	comap_symm symm_symm

MeasureTheory.Measure

Definitions

Name	Category	Theorems
comap 📖	CompOp	74 math math: comap_undef, MeasurableEmbedding.comap_add, IsMulRightInvariant.comap, le_comap_apply, unitInterval.volume_def, volume_set_coe_def, measure_subtype_coe_le_comap, OuterRegular.comap, comapₗ_eq_comap, MeasureTheory.isProbabilityMeasure_comap, IsAddHaarMeasure.comap, comap_preimage, InnerRegularWRT.comap, InnerRegular.comap', MeasurableEquiv.comap_apply, MeasureTheory.IsProbabilityMeasure_comap_equiv, MeasurableEmbedding.integrableAtFilter_iff_comap, map_eq_comap, aemeasurable_restrict_iff_comap_subtype, InnerRegular.comap, comap_id, IsAddLeftInvariant.comap, MeasureTheory.IsFiniteMeasureOnCompacts.comap', MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, comap_swap, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, ProbabilityTheory.comap_cond, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', MeasureTheory.lintegral_subtype_comap, IsFiniteMeasureOnCompacts.comap, MeasureTheory.integrableOn_iff_comap_subtypeVal, MeasurableEquiv.comap_symm, comap_apply, Regular.comap', comap_subtype_coe_apply, Subtype.volume_def, IsAddRightInvariant.comap, ae_restrict_iff_subtype, MeasurableEmbedding.gaussianReal_comap_apply, OuterRegular.comap', MeasurableEmbedding.comap_map, measurePreserving_homeomorphUnitSphereProd, AddCircle.measurePreserving_equivIoc, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul, comap_smul, comap_comap, MeasurableEmbedding.comap_restrict, MeasurableEmbedding.comap_apply, MeasureTheory.IsFiniteMeasure_comap, MeasureTheory.measurePreserving_subtype_coe, MeasureTheory.setLIntegral_subtype, MeasureTheory.isProbabilityMeasure_comap_down, MeasureTheory.integral_subtype_comap, MeasurableEmbedding.integrableOn_range_iff_comap, MeasurableEmbedding.restrict_comap, Regular.comap, IsHaarMeasure.comap, MeasureTheory.locallyIntegrable_comap, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, ProbabilityTheory.Kernel.borelMarkovFromReal_apply, MeasurableEmbedding.comap_preimage, MeasureTheory.addEquivAddHaarChar_smul_eq_comap, MeasureTheory.mulEquivHaarChar_smul_eq_comap, IsOpenPosMeasure.comap, MeasurableEmbedding.integrableOn_iff_comap, ProbabilityTheory.Kernel.comapRight_apply, MeasurableEmbedding.map_comap, map_comap_subtype_coe, MeasureTheory.FiniteMeasure.toMeasure_comap, MeasurableEmbedding.isProbabilityMeasure_comap, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, MeasurableEquiv.map_symm, comap_zero, IsMulLeftInvariant.comap
comapₗ 📖	CompOp	2 math math: comapₗ_eq_comap, comapₗ_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_image_of_ae_eq_comap 📖	—	MeasureTheory.NullMeasurableSet Set.image Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass comap	—	—	instOuterMeasureClass Filter.EventuallyEq.eq_1 MeasureTheory.ae_iff Set.ext Set.image_union Set.image_diff measure_image_eq_zero_of_comap_eq_zero
comap_apply 📖	mathematical	MeasurableSet Set.image	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike comap	—	comap_apply₀ MeasurableSet.nullMeasurableSet
comap_apply_le 📖	mathematical	MeasureTheory.NullMeasurableSet comap	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike Set.image	—	comap_apply₀ le_refl comap_undef ENNReal.instCanonicallyOrderedAdd
comap_apply₀ 📖	mathematical	MeasureTheory.NullMeasurableSet Set.image comap	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	comap.eq_1 MeasureTheory.toMeasure_apply₀ IsScalarTower.right MeasureTheory.OuterMeasure.comap_apply coe_toOuterMeasure
comap_comap 📖	mathematical	MeasurableSet Set.image	comap	—	ext comap_apply Set.image_comp comap.eq_1 Function.Injective.of_comp
comap_id 📖	mathematical	—	comap	—	ext comap_apply Set.image_id'
comap_preimage 📖	mathematical	Measurable MeasureTheory.NullMeasurableSet Set.image MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike comap Set.preimage Set.instInter Set.range	—	comap_apply₀ MeasurableSet.nullMeasurableSet Set.image_preimage_eq_inter_range
comap_smul 📖	mathematical	—	comap ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right eq_or_ne zero_smul comap_zero ext comap_apply₀ MeasureTheory.nullMeasurableSet_smul_measure_iff MeasurableSet.nullMeasurableSet smul_apply comap_undef smul_zero
comap_swap 📖	mathematical	—	comap Prod.instMeasurableSpace map	—	MeasurableEquiv.comap_symm
comap_undef 📖	mathematical	MeasureTheory.NullMeasurableSet Set.image	comap MeasureTheory.Measure instZero	—	—
comap_zero 📖	mathematical	—	comap MeasureTheory.Measure instZero	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MeasureTheory.OuterMeasure.toMeasure.congr_simp MeasureTheory.OuterMeasure.toMeasure_zero
comapₗ_apply 📖	mathematical	MeasurableSet Set.image	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comapₗ	—	IsScalarTower.right comapₗ.eq_1 liftLinear_apply MeasureTheory.OuterMeasure.comap_apply coe_toOuterMeasure
comapₗ_eq_comap 📖	mathematical	MeasurableSet Set.image	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comapₗ comap	—	IsScalarTower.right comapₗ_apply comap_apply
le_comap_apply 📖	mathematical	MeasureTheory.NullMeasurableSet Set.image	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike comap	—	comap.eq_1 MeasureTheory.le_toMeasure_apply
measure_image_eq_zero_of_comap_eq_zero 📖	—	MeasureTheory.NullMeasurableSet Set.image DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike comap instZeroENNReal	—	—	le_antisymm LE.le.trans le_comap_apply Eq.le zero_le ENNReal.instCanonicallyOrderedAdd

MeasureTheory.Measure.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image 📖	—	MeasureTheory.NullMeasurableSet Set.image MeasureTheory.Measure.comap	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measurableSet_toMeasurable Filter.EventuallyEq.trans MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap Filter.EventuallyEq.symm

---

← Back to Index