Deriv

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

Statistics

Metric	Count
Definitions	0
Theorems continuous_deriv, continuous_deriv_one, deriv', differentiable_deriv_two, iterate_deriv, iterate_deriv', derivWithin, continuousOn_derivWithin, continuousOn_deriv_of_isOpen, derivWithin, deriv_of_isOpen, derivWithin, contDiffOn_infty_iff_derivWithin, contDiffOn_infty_iff_deriv_of_isOpen, contDiffOn_succ_iff_derivWithin, contDiffOn_succ_iff_deriv_of_isOpen, contDiff_infty_iff_deriv, contDiff_one_iff_deriv, contDiff_succ_iff_deriv	19
Total	19

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_deriv 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	continuous contDiff_succ_iff_deriv of_le
continuous_deriv_one 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	continuous_deriv le_refl
deriv' 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	clm_apply fderiv_succ fun_comp snd contDiff_fun_id contDiff_const
differentiable_deriv_two 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace deriv	—	Nat.instAtLeastTwoHAddOfNat Differentiable.clm_apply Differentiable.fderiv_two fun_comp snd contDiff_fun_id differentiable_const
iterate_deriv 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop.some ENat Top.top instTopENat	Nat.iterate deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	contDiff_infty_iff_deriv
iterate_deriv' 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Nat.iterate deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	contDiff_succ_iff_deriv

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivWithin 📖	mathematical	ContDiffAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	derivWithin_univ ContDiffWithinAt.derivWithin contDiffWithinAt NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_derivWithin 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	ContinuousOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup derivWithin	—	continuousOn contDiffOn_succ_iff_derivWithin of_le
continuousOn_deriv_of_isOpen 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	ContinuousOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	continuousOn contDiffOn_succ_iff_deriv_of_isOpen of_le
derivWithin 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	derivWithin NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	contDiffOn_succ_iff_derivWithin of_le
deriv_of_isOpen 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	congr derivWithin IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd derivWithin_of_isOpen

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivWithin 📖	mathematical	ContDiffWithinAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set Set.instMembership	derivWithin NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	comp RingHomIsometric.ids smulCommClass_self clm_apply contDiffWithinAt_fun_id contDiffWithinAt_const fderivWithin_right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_infty_iff_derivWithin 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	ContDiffOn WithTop.some ENat Top.top instTopENat DifferentiableOn NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace derivWithin	—	contDiffOn_succ_iff_derivWithin instIsEmptyFalse
contDiffOn_infty_iff_deriv_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedSpace WithTop.some ENat Top.top instTopENat DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace deriv	—	contDiffOn_succ_iff_deriv_of_isOpen instIsEmptyFalse
contDiffOn_succ_iff_derivWithin 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	ContDiffOn WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DifferentiableOn NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn derivWithin	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids contDiffOn_succ_iff_fderivWithin
contDiffOn_succ_iff_deriv_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedSpace WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn deriv	—	contDiffOn_succ_iff_derivWithin IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd Iff.and contDiffOn_congr derivWithin_of_isOpen
contDiff_infty_iff_deriv 📖	mathematical	—	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop.some ENat Top.top instTopENat Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace deriv	—	contDiff_succ_iff_deriv instIsEmptyFalse
contDiff_one_iff_deriv 📖	mathematical	—	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Continuous deriv	—	contDiff_succ_iff_deriv instIsEmptyFalse
contDiff_succ_iff_deriv 📖	mathematical	—	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn Set.univ deriv	—	—

---

← Back to Index