FDeriv

📁 Source: Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean

Statistics

Metric	Count
Definitions	0
Theorems mdifferentiable, mdifferentiableAt, mdifferentiableOn, mdifferentiableWithinAt, hasMFDerivAt, hasMFDerivWithinAt, hasFDerivAt, hasFDerivWithinAt, differentiable, differentiableAt, differentiableOn, differentiableWithinAt, uniqueMDiffOn, uniqueMDiffOn, uniqueMDiffWithinAt, uniqueDiffOn, uniqueDiffWithinAt, hasMFDerivAt_iff_hasFDerivAt, hasMFDerivWithinAt_iff_hasFDerivWithinAt, mdifferentiableAt_iff_differentiableAt, mdifferentiableOn_iff_differentiableOn, mdifferentiableWithinAt_iff_differentiableWithinAt, mdifferentiable_iff_differentiable, mfderivWithin_eq_fderivWithin, mfderiv_eq_fderiv, uniqueMDiffOn_iff_uniqueDiffOn, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt, writtenInExtChartAt_model_space	28
Total	28

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mdifferentiable 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MDifferentiable modelWithCornersSelf chartedSpaceSelf	—	mdifferentiable_iff_differentiable

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mdifferentiableAt 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MDifferentiableAt modelWithCornersSelf chartedSpaceSelf	—	mdifferentiableAt_iff_differentiableAt

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mdifferentiableOn 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MDifferentiableOn modelWithCornersSelf chartedSpaceSelf	—	mdifferentiableOn_iff_differentiableOn

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mdifferentiableWithinAt 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MDifferentiableWithinAt modelWithCornersSelf chartedSpaceSelf	—	mdifferentiableWithinAt_iff_differentiableWithinAt

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMFDerivAt 📖	mathematical	HasFDerivAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf instTopologicalSpaceTangentSpace	HasMFDerivAt	—	hasMFDerivAt_iff_hasFDerivAt

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMFDerivWithinAt 📖	mathematical	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf instTopologicalSpaceTangentSpace	HasMFDerivWithinAt	—	hasMFDerivWithinAt_iff_hasFDerivWithinAt

HasMFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFDerivAt 📖	mathematical	HasMFDerivAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	HasFDerivAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace instTopologicalSpaceTangentSpace	—	hasMFDerivAt_iff_hasFDerivAt

HasMFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFDerivWithinAt 📖	mathematical	HasMFDerivWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace instTopologicalSpaceTangentSpace	—	hasMFDerivWithinAt_iff_hasFDerivWithinAt

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiable 📖	mathematical	MDifferentiable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	mdifferentiable_iff_differentiable

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt 📖	mathematical	MDifferentiableAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	mdifferentiableAt_iff_differentiableAt

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableOn 📖	mathematical	MDifferentiableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	mdifferentiableOn_iff_differentiableOn

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableWithinAt 📖	mathematical	MDifferentiableWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	mdifferentiableWithinAt_iff_differentiableWithinAt

ModelWithCorners

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueMDiffOn 📖	mathematical	—	UniqueMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set.range toFun'	—	UniqueDiffOn.uniqueMDiffOn uniqueDiffOn

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueMDiffOn 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	UniqueMDiffOn modelWithCornersSelf chartedSpaceSelf	—	uniqueMDiffOn_iff_uniqueDiffOn

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueMDiffWithinAt 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	UniqueMDiffWithinAt modelWithCornersSelf chartedSpaceSelf	—	uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

UniqueMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueDiffOn 📖	mathematical	UniqueMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	uniqueMDiffOn_iff_uniqueDiffOn

UniqueMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueDiffWithinAt 📖	mathematical	UniqueMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMFDerivAt_iff_hasFDerivAt 📖	mathematical	—	HasMFDerivAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf HasFDerivAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace instTopologicalSpaceTangentSpace	—	hasMFDerivWithinAt_univ hasMFDerivWithinAt_iff_hasFDerivWithinAt hasFDerivWithinAt_univ
hasMFDerivWithinAt_iff_hasFDerivWithinAt 📖	mathematical	—	HasMFDerivWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup instModuleTangentSpace instTopologicalSpaceTangentSpace	—	PartialEquiv.trans_refl Set.range_id Set.inter_univ HasFDerivWithinAt.continuousWithinAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
mdifferentiableAt_iff_differentiableAt 📖	mathematical	—	MDifferentiableAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	PartialEquiv.trans_refl Set.range_id DifferentiableAt.continuousAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
mdifferentiableOn_iff_differentiableOn 📖	mathematical	—	MDifferentiableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	—
mdifferentiableWithinAt_iff_differentiableWithinAt 📖	mathematical	—	MDifferentiableWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	PartialEquiv.trans_refl Set.range_id Set.inter_univ DifferentiableWithinAt.continuousWithinAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
mdifferentiable_iff_differentiable 📖	mathematical	—	MDifferentiable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	—
mfderivWithin_eq_fderivWithin 📖	mathematical	—	mfderivWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf fderivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	PartialEquiv.trans_refl Set.range_id Set.inter_univ fderivWithin_zero_of_not_differentiableWithinAt mdifferentiableWithinAt_iff_differentiableWithinAt
mfderiv_eq_fderiv 📖	mathematical	—	mfderiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	mfderivWithin_univ fderivWithin_univ mfderivWithin_eq_fderivWithin
uniqueMDiffOn_iff_uniqueDiffOn 📖	mathematical	—	UniqueMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	—
uniqueMDiffWithinAt_iff_uniqueDiffWithinAt 📖	mathematical	—	UniqueMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	PartialEquiv.trans_refl Set.range_id Set.inter_univ
writtenInExtChartAt_model_space 📖	mathematical	—	writtenInExtChartAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	—	—

---

← Back to Index