Normed

📁 Source: Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

Statistics

Metric	Count
Definitions	0
Theorems contDiff_normed, continuous_normed, hasCompactSupport_normed, integrable, integrable_normed, integral_le_measure_closedBall, integral_normed, integral_normed_smul, integral_pos, measure_closedBall_div_le_integral, measure_closedBall_le_integral, nonneg_normed, normed_def, normed_le_div_measure_closedBall_rIn, normed_le_div_measure_closedBall_rOut, normed_neg, normed_sub, support_normed_eq, tendsto_support_normed_smallSets, tsupport_normed_eq	20
Total	20

ContDiffBump

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_normed 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop.some ENat normed	—	ContDiff.div_const contDiff
continuous_normed 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.pseudoMetricSpace normed	—	Continuous.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous
hasCompactSupport_normed 📖	mathematical	—	HasCompactSupport Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero normed	—	tsupport_normed_eq FiniteDimensional.proper_real
integrable 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing toFun	—	Continuous.integrable_of_hasCompactSupport BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper continuous hasCompactSupport
integrable_normed 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing normed	—	MeasureTheory.Integrable.div_const integrable
integral_le_measure_closedBall 📖	mathematical	—	Real Real.instLE MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal toFun MeasureTheory.Measure.real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace rOut	—	MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero zero_of_le_dist le_of_lt MeasureTheory.setIntegral_mono Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.Integrable.integrableOn integrable enorm_one NormedDivisionRing.to_normOneClass NeZero.charZero_one ENNReal.instCharZero FiniteDimensional.proper_real MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper le_one MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply Set.univ_inter mul_one
integral_normed 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal normed Real.instOne	—	div_eq_mul_inv mul_comm MeasureTheory.integral_smul NormedSpace.toNormSMulClass Algebra.to_smulCommClass inv_mul_cancel₀ LT.lt.ne' integral_pos
integral_normed_smul 📖	mathematical	—	MeasureTheory.integral Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField normed	—	integral_smul_const integral_normed one_smul
integral_pos 📖	mathematical	—	Real Real.instLT Real.instZero MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal toFun	—	MeasureTheory.integral_pos_iff_support_of_nonneg nonneg' integrable support_eq Metric.measure_ball_pos rOut_pos
measure_closedBall_div_le_integral 📖	mathematical	Real Real.instLE rOut Real.instMul rIn	DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.Measure.real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Monoid.toNatPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal toFun	—	rIn_pos not_lt LT.lt.le mul_pos_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le LT.lt.trans_le rOut_pos le_trans div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE pow_pos Real.instZeroLEOneClass MeasureTheory.Measure.addHaar_real_closedBall' mul_assoc mul_comm mul_pow mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toPosMulMono MeasureTheory.measureReal_nonneg measure_closedBall_le_integral
measure_closedBall_le_integral 📖	mathematical	—	Real Real.instLE MeasureTheory.Measure.real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rIn MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal toFun	—	MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply Set.univ_inter mul_one MeasureTheory.setIntegral_congr_fun measurableSet_closedBall BorelSpace.opensMeasurable one_of_mem_closedBall MeasureTheory.setIntegral_le_integral Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing HasSolidNorm.orderClosedTopology instHasSolidNormReal integrable Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass nonneg
nonneg_normed 📖	mathematical	—	Real Real.instLE Real.instZero normed	—	div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing nonneg MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal nonneg'
normed_def 📖	mathematical	—	normed Real DivInvMonoid.toDiv Real.instDivInvMonoid toFun MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	—
normed_le_div_measure_closedBall_rIn 📖	mathematical	—	Real Real.instLE normed DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne MeasureTheory.Measure.real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rIn	—	normed_def div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_one ENNReal.toReal_pos LT.lt.ne' Metric.measure_closedBall_pos rIn_pos LT.lt.ne MeasureTheory.measure_closedBall_lt_top FiniteDimensional.proper_real MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper measure_closedBall_le_integral
normed_le_div_measure_closedBall_rOut 📖	mathematical	Real Real.instLE rOut Real.instMul rIn	normed DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Metric.closedBall	—	rIn_pos not_lt LT.lt.le mul_pos_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le LT.lt.trans_le rOut_pos div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE le_one integral_pos MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure LE.le.trans div_le_div_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE ENNReal.toReal_pos LT.lt.ne' Metric.measure_closedBall_pos LT.lt.ne MeasureTheory.measure_closedBall_lt_top FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts one_mul div_le_iff₀' pow_pos Real.instZeroLEOneClass measure_closedBall_div_le_integral
normed_neg 📖	mathematical	—	normed NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toNeg	—	normed_def neg
normed_sub 📖	mathematical	—	normed SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	normed_def sub
support_normed_eq 📖	mathematical	—	Function.support Real Real.instZero normed Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rOut	—	Function.support_div support_eq Function.support_const LT.lt.ne' integral_pos Set.inter_univ
tendsto_support_normed_smallSets 📖	mathematical	Filter.Tendsto Real rOut nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	Set Function.support normed Filter.smallSets SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Filter.HasBasis.tendsto_right_iff Filter.HasBasis.smallSets Metric.nhds_basis_ball Filter.Eventually.mono abs_eq_self Real.instIsOrderedAddMonoid LT.lt.le rOut_pos support_normed_eq Metric.ball_subset_ball
tsupport_normed_eq 📖	mathematical	—	tsupport Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normed Metric.closedBall rOut	—	tsupport.eq_1 support_normed_eq closure_ball LT.lt.ne' rOut_pos

---

← Back to Index