Affine

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

Statistics

Metric	Count
Definitions	0
Theorems differentiable, differentiableAt, differentiableOn, differentiableWithinAt, fderiv, fderivWithin, hasFDerivAt, hasFDerivAtFilter, hasFDerivWithinAt, hasStrictFDerivAt	10
Total	10

ContinuousAffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiable 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike	—	differentiableAt
differentiableAt 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike	—	HasFDerivAt.differentiableAt instIsTopologicalAddTorsor_1 hasFDerivAt
differentiableOn 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike	—	Differentiable.differentiableOn differentiable
differentiableWithinAt 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike	—	DifferentiableAt.differentiableWithinAt differentiableAt
fderiv 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	HasFDerivAt.fderiv instIsTopologicalAddTorsor_1 IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt
fderivWithin 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	fderivWithin DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	instIsTopologicalAddTorsor_1 DifferentiableAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace differentiableAt fderiv
hasFDerivAt 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	hasFDerivAtFilter
hasFDerivAtFilter 📖	mathematical	—	HasFDerivAtFilter SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	instIsTopologicalAddTorsor_1 instIsTopologicalAddTorsor SeminormedAddCommGroup.toIsTopologicalAddGroup decomp IsTopologicalAddGroup.toContinuousAdd add_zero RingHomIsometric.ids HasFDerivAtFilter.add ContinuousLinearMap.hasFDerivAtFilter hasFDerivAtFilter_const
hasFDerivWithinAt 📖	mathematical	—	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	hasFDerivAtFilter
hasStrictFDerivAt 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousAffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor instFunLike contLinear instIsTopologicalAddTorsor_1	—	instIsTopologicalAddTorsor_1 instIsTopologicalAddTorsor SeminormedAddCommGroup.toIsTopologicalAddGroup decomp IsTopologicalAddGroup.toContinuousAdd add_zero RingHomIsometric.ids HasStrictFDerivAt.add ContinuousLinearMap.hasStrictFDerivAt hasStrictFDerivAt_const

---

← Back to Index