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 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 ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero ContinuousLinearMap.id	—	hasFDerivAt_update
hasFDerivAt_update 📖	mathematical	—	HasFDerivAt 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_pi eq_or_ne Function.update_self Pi.single_eq_same hasFDerivAt_id Function.update_of_ne Pi.single_eq_of_ne hasFDerivAt_const

---

← Back to Index