ContinuousMapZero

📁 Source: Mathlib/MeasureTheory/SpecificCodomains/ContinuousMapZero.lean

Statistics

Metric	Count
Definitions	0
Theorems aeStronglyMeasurable_mkD_of_uncurry, aeStronglyMeasurable_mkD_restrict_of_uncurry, aeStronglyMeasurable_restrict_mkD_of_uncurry, aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, hasFiniteIntegral_mkD_of_bound, hasFiniteIntegral_mkD_restrict_of_bound, hasFiniteIntegral_of_bound	7
Total	7

ContinuousMapZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeStronglyMeasurable_mkD_of_uncurry 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEStronglyMeasurable ContinuousMapZero instTopologicalSpace mkD	—	MeasureTheory.Measure.instOuterMeasureClass instContinuousMapClass Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace isEmbedding_toContinuousMap aestronglyMeasurable_congr Filter.mp_mem Filter.univ_mem' mkD_eq_mkD_of_map_zero ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry
aeStronglyMeasurable_mkD_restrict_of_uncurry 📖	mathematical	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.univ Filter.Eventually Set.instMembership Set.Elem NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEStronglyMeasurable ContinuousMapZero instTopologicalSpaceSubtype instTopologicalSpace mkD Set.restrict	—	MeasureTheory.Measure.instOuterMeasureClass instContinuousMapClass Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace isEmbedding_toContinuousMap aestronglyMeasurable_congr Filter.mp_mem Filter.univ_mem' mkD_eq_mkD_of_map_zero ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry
aeStronglyMeasurable_restrict_mkD_of_uncurry 📖	mathematical	MeasurableSet ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.univ Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict	MeasureTheory.AEStronglyMeasurable ContinuousMapZero instTopologicalSpace mkD	—	MeasureTheory.Measure.instOuterMeasureClass instContinuousMapClass Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace isEmbedding_toContinuousMap aestronglyMeasurable_congr Filter.mp_mem Filter.univ_mem' mkD_eq_mkD_of_map_zero ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry
aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry 📖	mathematical	MeasurableSet ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Filter.Eventually Set.instMembership Set.Elem NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict	MeasureTheory.AEStronglyMeasurable ContinuousMapZero instTopologicalSpaceSubtype instTopologicalSpace mkD Set.restrict	—	MeasureTheory.Measure.instOuterMeasureClass instContinuousMapClass Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace isEmbedding_toContinuousMap aestronglyMeasurable_congr Filter.mp_mem Filter.univ_mem' mkD_eq_mkD_of_map_zero ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry
hasFiniteIntegral_mkD_of_bound 📖	mathematical	Filter.Eventually Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.HasFiniteIntegral Real ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm	ContinuousMapZero instNormedAddCommGroup mkD	—	MeasureTheory.Measure.instOuterMeasureClass hasFiniteIntegral_of_bound Filter.mp_mem Filter.univ_mem' mkD_apply_of_continuous
hasFiniteIntegral_mkD_restrict_of_bound 📖	mathematical	Filter.Eventually ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.instMembership Set.Elem NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.HasFiniteIntegral Real ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm	ContinuousMapZero instTopologicalSpaceSubtype instNormedAddCommGroup mkD Set.restrict	—	MeasureTheory.Measure.instOuterMeasureClass hasFiniteIntegral_mkD_of_bound
hasFiniteIntegral_of_bound 📖	mathematical	MeasureTheory.HasFiniteIntegral Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ContinuousMapZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem' le_trans norm_nonneg MeasureTheory.HasFiniteIntegral.mono' ContinuousMap.norm_le

---

← Back to Index