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 IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.Measure.real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rOut Monoid.toPow 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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	Real Real.instLE normed DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toPow 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 rOut	—	rIn_pos not_lt LT.lt.le mul_pos_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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	Filter.Tendsto Set Function.support Real Real.instZero normed Filter.smallSets nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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