ContinuousCompMeasurePreserving

📁 Source: Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean

Statistics

Metric	Count
Definitions	0
Theorems compMeasurePreservingLp, compMeasurePreservingLp, compMeasurePreservingLp, compMeasurePreservingLp, compMeasurePreservingLp, compMeasurePreserving_continuous	6
Total	6

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreservingLp 📖	mathematical	Continuous MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap ContinuousMap.compactOpen MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_iff_continuousAt ContinuousAt.compMeasurePreservingLp continuousAt

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreservingLp 📖	mathematical	ContinuousAt MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap ContinuousMap.compactOpen MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.compMeasurePreservingLp

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreservingLp 📖	mathematical	ContinuousOn MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap ContinuousMap.compactOpen MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousWithinAt.compMeasurePreservingLp

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreservingLp 📖	mathematical	ContinuousWithinAt MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap ContinuousMap.compactOpen MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.compMeasurePreservingLp

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreservingLp 📖	mathematical	Filter.Tendsto MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp nhds MeasureTheory.Lp.instNormedAddCommGroup ContinuousMap ContinuousMap.compactOpen MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.tendsto MeasureTheory.Lp.compMeasurePreserving_continuous tendsto_subtype_rng comp prodMk_nhds

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreserving_continuous 📖	mathematical	—	Continuous MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ContinuousMap MeasureTheory.MeasurePreserving DFunLike.coe ContinuousMap.instFunLike instTopologicalSpaceProd instNormedAddCommGroup instTopologicalSpaceSubtype ContinuousMap.compactOpen AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving	—	LT.lt.ne' LT.lt.trans_le one_pos IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out continuous_prod_of_dense_continuous_lipschitzWith SeminormedAddCommGroup.toIsTopologicalAddGroup simpleFunc.dense CanLift.prf Subtype.canLift simpleFunc.induction LT.lt.ne MeasureTheory.continuous_indicatorConstLp_set MeasurableSet.preimage MeasureTheory.MeasurePreserving.measurable MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val Filter.Eventually.of_forall MeasurableSet.nullMeasurableSet Continuous.add IsTopologicalAddGroup.toContinuousAdd Isometry.lipschitz isometry_compMeasurePreserving

---

← Back to Index