Documentation Verification Report

SmoothApprox

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_contDiff_dist_le_of_forall_mem_ball_dist_le`, `dense_setOf_contDiff`, `exists_contDiff_dist_le_of_forall_mem_ball_dist_le`, `exists_contDiff_dist_le`	4
Total	4

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contDiff_dist_le_of_forall_mem_ball_dist_le` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLT` `Real.instZero`	`ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	—	`MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `locallyIntegrable` `BorelSpace.opensMeasurable` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `secondCountableTopologyEither_of_left` `secondCountable_of_proper`

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_setOf_contDiff` 📖	mathematical	—	`Dense` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `setOf` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat` `DFunLike.coe` `instFunLike`	—	`mem_closure_iff_nhds_basis` `nhds_basis_uniformity` `Filter.HasBasis.compactConvergenceUniformity` `Metric.uniformity_basis_dist` `IsCompact.uniformContinuousOn_of_continuous` `IsCompact.cthickening` `FiniteDimensional.proper_real` `Continuous.continuousOn` `ContinuousMapClass.map_continuous` `instContinuousMapClass` `Nat.instAtLeastTwoHAddOfNat` `Metric.uniformContinuousOn_iff` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le` `lt_min` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ContDiff.continuous` `LE.le.trans_lt` `LT.lt.le` `Metric.mem_cthickening_of_dist_le` `lt_min_iff` `Metric.mem_ball` `Metric.self_subset_cthickening` `half_lt_self`

MeasureTheory.LocallyIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contDiff_dist_le_of_forall_mem_ball_dist_le` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `Real.instLT` `Real.instZero`	`ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `half_lt_self` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `HasCompactSupport.contDiff_convolution_left` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `ContDiffBump.hasCompactSupport_normed` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `ContDiffBump.contDiff_normed` `ContDiffBump.dist_normed_convolution_le` `aestronglyMeasurable`

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contDiff_dist_le` 📖	mathematical	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLT` `Real.instZero`	`ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Nat.instAtLeastTwoHAddOfNat` `Metric.uniformContinuous_iff` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le` `continuous` `LE.le.trans_lt` `LT.lt.le` `half_lt_self`

---

← Back to Index