SmoothApprox

📁 Source: Mathlib/Geometry/Manifold/SmoothApprox.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_contDiff_approx, exists_contDiff_approx_and_eqOn, exists_contMDiff_approx, exists_contMDiff_approx_and_eqOn	4
Total	4

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_contDiff_approx 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.pseudoMetricSpace Real.instLT Real.instZero	ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Dist.dist PseudoMetricSpace.toDist Set Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	exists_contDiff_approx_and_eqOn isClosed_empty mem_nhdsSet_empty contDiffOn_empty
exists_contDiff_approx_and_eqOn 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.pseudoMetricSpace Real.instLT Real.instZero Set Filter Filter.instMembership nhdsSet ContDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat	ContDiff Dist.dist PseudoMetricSpace.toDist Set.EqOn Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	exists_contMDiff_approx_and_eqOn ContMDiffAdd.toIsManifold instContMDiffAddSelf SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContDiffOn.contMDiffOn ContMDiff.contDiff ContMDiffMap.contMDiff
exists_contMDiff_approx 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.pseudoMetricSpace Real.instLT Real.instZero	Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContMDiffMap DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField modelWithCornersSelf chartedSpaceSelf WithTop.some ENat ContMDiffMap.instFunLike Set Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	exists_contMDiff_approx_and_eqOn isClosed_empty mem_nhdsSet_empty contMDiffOn_empty
exists_contMDiff_approx_and_eqOn 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.pseudoMetricSpace Real.instLT Real.instZero Set Filter Filter.instMembership nhdsSet ContMDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField modelWithCornersSelf chartedSpaceSelf WithTop.some ENat	Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContMDiffMap ContMDiffMap.instFunLike Set.EqOn Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	dist_self Convex.inter convex_ball Convex.setOf_const_imp convex_singleton exists_contMDiffMap_forall_mem_convex_of_local mem_nhdsSet_iff_forall Filter.Eventually.and IsOpen.eventually_mem IsClosed.isOpen_compl ContinuousAt.eventually_lt HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid continuousAt dist continuous_const dist_zero ContinuousAt.eventually_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace contMDiffOn_const instIsEmptyFalse

---

← Back to Index