Lemmas

📁 Source: Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems aestronglyMeasurable_comp₂, apply_continuousLinearMap, comp_measurePreserving, aestronglyMeasurable_comp_iff, apply_continuousLinearMap, aestronglyMeasurable_dirac, aestronglyMeasurable_smul_const_iff, aestronglyMeasurable_withDensity_iff	8
Total	8

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_comp₂ 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Continuous.comp_aestronglyMeasurable₂ continuous₂

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_continuousLinearMap 📖	mathematical	MeasureTheory.AEStronglyMeasurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	DFunLike.coe ContinuousLinearMap.funLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.comp_aestronglyMeasurable IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.continuous
comp_measurePreserving 📖	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.MeasurePreserving	—	—	comp_quasiMeasurePreserving MeasureTheory.MeasurePreserving.quasiMeasurePreserving

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_comp_iff 📖	mathematical	MeasureTheory.MeasurePreserving MeasurableEmbedding	MeasureTheory.AEStronglyMeasurable	—	map_eq MeasurableEmbedding.aestronglyMeasurable_map_iff

StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_continuousLinearMap 📖	mathematical	MeasureTheory.StronglyMeasurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	DFunLike.coe ContinuousLinearMap.funLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.comp_stronglyMeasurable IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.continuous

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_dirac 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.dirac	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stronglyMeasurable_const MeasureTheory.ae_eq_dirac
aestronglyMeasurable_smul_const_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace Topology.IsClosedEmbedding.isEmbedding isClosedEmbedding_smul_left SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
aestronglyMeasurable_withDensity_iff 📖	mathematical	Measurable NNReal NNReal.measurableSpace	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Measure.withDensity ENNReal.ofNNReal Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NNReal.toReal	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSet.compl MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable NNReal.borelSpace NNReal.instSecondCountableTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasureTheory.StronglyMeasurable.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal Real.borelSpace Measurable.coe_nnreal_real MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl MeasureTheory.ae_restrict_iff' Filter.mp_mem MeasureTheory.ae_withDensity_iff Measurable.coe_nnreal_ennreal Filter.EventuallyEq.eq_1 Filter.univ_mem' MeasureTheory.ae_restrict_mem zero_smul Measurable.inv ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal smul_smul inv_mul_cancel₀ one_smul

---

← Back to Index