BoundedContinuousFunction

📁 Source: Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Statistics

Metric	Count
Definitions	0
Theorems apply_le_nndist_zero, integrable, integrable_of_nnreal, integral_add_const, integral_const_sub, integral_eq_integral_nnrealPart_sub, isBounded_range_integral, lintegral_le_edist_mul, lintegral_lt_top_of_nnreal, lintegral_nnnorm_le, lintegral_of_real_lt_top, measurable_coe_ennreal_comp, norm_integral_le_mul_norm, norm_integral_le_norm, tendsto_integral_of_forall_integral_le_liminf_integral, tendsto_integral_of_forall_limsup_integral_le_integral, toReal_lintegral_coe_eq_integral	17
Total	17

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_le_nndist_zero 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction instPseudoMetricSpaceNNReal instFunLike NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpace instZero instZeroNNReal	—	NNReal.nndist_zero_eq_val nndist_coe_le_nndist
integrable 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe BoundedContinuousFunction instFunLike	—	Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Continuous.measurable continuous MeasureTheory.hasFiniteIntegral_def lintegral_nnnorm_le ENNReal.mul_lt_top ENNReal.coe_lt_top MeasureTheory.measure_lt_top
integrable_of_nnreal 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NNReal NNReal.toReal DFunLike.coe BoundedContinuousFunction instPseudoMetricSpaceNNReal instFunLike	—	Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Continuous.measurable Continuous.comp NNReal.continuous_coe continuous NNReal.enorm_eq lintegral_lt_top_of_nnreal
integral_add_const 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace instFunLike instAdd Real.instAdd instBoundedAddOfLipschitzAdd Real.instAddMonoid Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal const Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id MeasureTheory.Measure.real Set.univ	—	instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.integral_add integrable instSecondCountableTopologyReal Real.borelSpace MeasureTheory.integrable_const MeasureTheory.integral_const Real.instCompleteSpace
integral_const_sub 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace instFunLike instSub Real.instSub instBoundedSub NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing IsTopologicalAddGroup.to_continuousSub UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.instAddGroup instIsTopologicalAddGroupReal const Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id MeasureTheory.Measure.real Set.univ	—	instBoundedSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal MeasureTheory.integral_sub MeasureTheory.integrable_const integrable instSecondCountableTopologyReal Real.borelSpace MeasureTheory.integral_const Real.instCompleteSpace
integral_eq_integral_nnrealPart_sub 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace instFunLike Real.instSub NNReal.toReal NNReal instPseudoMetricSpaceNNReal nnrealPart instNeg NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	—	self_eq_nnrealPart_sub_nnrealPart_neg MeasureTheory.integral_sub
isBounded_range_integral 📖	mathematical	MeasureTheory.IsProbabilityMeasure	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range MeasureTheory.integral DFunLike.coe BoundedContinuousFunction instFunLike	—	isBounded_iff_forall_norm_le norm_integral_le_norm
lintegral_le_edist_mul 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpace instMetricSpaceNNReal instZero instZeroNNReal MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	le_trans MeasureTheory.lintegral_mono ENNReal.coe_le_coe apply_le_nndist_zero coe_nnreal_ennreal_nndist MeasureTheory.lintegral_const
lintegral_lt_top_of_nnreal 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal instFunLike Top.top instTopENNReal	—	IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal NNReal.upper_bound ENNReal.coe_le_coe
lintegral_nnnorm_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instSeminormedAddCommGroup MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	MeasureTheory.lintegral_mono_fn' le_refl ENNReal.coe_le_coe_of_le nnnorm_coe_le_nnnorm MeasureTheory.lintegral_const
lintegral_of_real_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofReal DFunLike.coe BoundedContinuousFunction Real Real.pseudoMetricSpace instFunLike Top.top instTopENNReal	—	lintegral_lt_top_of_nnreal
measurable_coe_ennreal_comp 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace ENNReal.ofNNReal DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal instFunLike	—	Measurable.comp measurable_coe_nnreal_ennreal Continuous.measurable NNReal.borelSpace continuous
norm_integral_le_mul_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.integral DFunLike.coe BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike Real.instMul MeasureTheory.Measure.real Set.univ instNorm	—	MeasureTheory.norm_integral_le_integral_norm MeasureTheory.integral_mono Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.integrable_norm_iff Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Continuous.measurable continuous integrable MeasureTheory.integrable_const norm_coe_le_norm MeasureTheory.integral_const Real.instCompleteSpace
norm_integral_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.integral DFunLike.coe BoundedContinuousFunction SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike instNorm	—	MeasureTheory.probReal_univ one_mul norm_integral_le_mul_norm MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure
tendsto_integral_of_forall_integral_le_liminf_integral 📖	mathematical	MeasureTheory.IsProbabilityMeasure Real Real.instLE MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace instFunLike Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Filter.eq_or_neBot isBounded_range_integral instSecondCountableTopologyReal Real.borelSpace BddAbove.isBoundedUnder Filter.univ_mem Set.image_univ Bornology.IsBounded.bddAbove Real.instIsOrderBornology BddBelow.isBoundedUnder Bornology.IsBounded.bddBelow tendsto_of_le_liminf_of_limsup_le instOrderTopologyReal instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal add_norm_nonneg liminf_add_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.IsBounded.isCobounded_ge Filter.map_neBot add_le_add_iff_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le MeasureTheory.probReal_univ one_mul integral_add_const MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instBoundedSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal norm_sub_nonneg liminf_const_sub AddGroup.toOrderedSub Filter.IsBounded.isCobounded_le sub_le_sub_iff_left integral_const_sub
tendsto_integral_of_forall_limsup_integral_le_integral 📖	mathematical	MeasureTheory.IsProbabilityMeasure Real Real.instLE Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace instFunLike	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Filter.eq_or_neBot isBounded_range_integral instSecondCountableTopologyReal Real.borelSpace BddAbove.isBoundedUnder Filter.univ_mem Set.image_univ Bornology.IsBounded.bddAbove Real.instIsOrderBornology BddBelow.isBoundedUnder Bornology.IsBounded.bddBelow tendsto_of_le_liminf_of_limsup_le instOrderTopologyReal instBoundedSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal norm_sub_nonneg limsup_const_sub AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.IsBounded.isCobounded_ge Filter.map_neBot sub_le_sub_iff_left MeasureTheory.probReal_univ one_mul integral_const_sub MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal add_norm_nonneg limsup_add_const Filter.IsBounded.isCobounded_le add_le_add_iff_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le integral_add_const
toReal_lintegral_coe_eq_integral 📖	mathematical	—	ENNReal.toReal MeasureTheory.lintegral ENNReal.ofNNReal DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal instFunLike MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField NNReal.toReal	—	MeasureTheory.integral_eq_lintegral_of_nonneg_ae Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Continuous.measurable Continuous.comp NNReal.continuous_coe continuous ENNReal.ofReal_coe_nnreal

---

← Back to Index