Support

📁 Source: Mathlib/Analysis/Calculus/Deriv/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv, support_deriv_subset	2
Total	2

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	deriv NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	mono' support_deriv_subset

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
support_deriv_subset 📖	mathematical	—	Set Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup deriv NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace tsupport SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	not_imp_not Function.notMem_support Filter.EventuallyEq.deriv_eq notMem_tsupport_iff_eventuallyEq deriv_const

---

← Back to Index