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 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	—	instIsTopologicalAddTorsor_1 DifferentiableAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace differentiableAt fderiv
hasFDerivAt 📖	mathematical	—	HasFDerivAt 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	—	hasFDerivAtFilter
hasFDerivAtFilter 📖	mathematical	—	HasFDerivAtFilter 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	—	instIsTopologicalAddTorsor_1 Asymptotics.IsLittleOTVS.congr_left Asymptotics.IsLittleOTVS.zero vsub_eq_sub contLinear_map_vsub map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self
hasFDerivWithinAt 📖	mathematical	—	HasFDerivWithinAt 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	—	hasFDerivAtFilter
hasStrictFDerivAt 📖	mathematical	—	HasStrictFDerivAt 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	—	hasFDerivAtFilter

---

← Back to Index