Pi

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems fderiv_single, fderiv_update, hasFDerivAt_single, hasFDerivAt_update	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderiv_single 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap.pi AddCommGroup.toAddCommMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero ContinuousLinearMap.id	—	fderiv_update
fderiv_update 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace Function.update ContinuousLinearMap.pi AddCommGroup.toAddCommMonoid Pi.single ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero ContinuousLinearMap.id	—	HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.continuousAdd instContinuousSMulForall Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_update
hasFDerivAt_single 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap.pi ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero ContinuousLinearMap.id	—	hasFDerivAt_update
hasFDerivAt_update 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace Function.update ContinuousLinearMap.pi AddCommGroup.toAddCommMonoid Pi.single ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero ContinuousLinearMap.id	—	add_sub_cancel add_zero IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomCompTriple.ids RingHomIsometric.ids zero_add ContinuousLinearMap.comp_id HasFDerivAt.add hasFDerivAt_const HasFDerivAt.comp ContinuousLinearMap.hasFDerivAt hasFDerivAt_sub_const

---

← Back to Index