Linear

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

Statistics

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

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiable 📖	mathematical	—	Differentiable DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	differentiableAt
differentiableAt 📖	mathematical	—	DifferentiableAt DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	HasFDerivAt.differentiableAt hasFDerivAt
differentiableOn 📖	mathematical	—	DifferentiableOn DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	Differentiable.differentiableOn differentiable
differentiableWithinAt 📖	mathematical	—	DifferentiableWithinAt DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	DifferentiableAt.differentiableWithinAt differentiableAt
fderiv 📖	mathematical	—	fderiv DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	HasFDerivAt.fderiv hasFDerivAt
fderivWithin 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField	fderivWithin DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	DifferentiableAt.fderivWithin differentiableAt fderiv
hasFDerivAt 📖	mathematical	—	HasFDerivAt DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	hasFDerivAtFilter
hasFDerivAtFilter 📖	mathematical	—	HasFDerivAtFilter DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	Asymptotics.IsLittleOTVS.congr_left Asymptotics.IsLittleOTVS.zero map_sub sub_self
hasFDerivWithinAt 📖	mathematical	—	HasFDerivWithinAt DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	hasFDerivAtFilter
hasStrictFDerivAt 📖	mathematical	—	HasStrictFDerivAt DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	—	Asymptotics.IsLittleOTVS.congr_left Asymptotics.IsLittleOTVS.zero map_sub sub_self

IsBoundedLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiable 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	Differentiable NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	differentiableAt
differentiableAt 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	DifferentiableAt NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	HasFDerivAt.differentiableAt hasFDerivAt
differentiableOn 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	DifferentiableOn NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	Differentiable.differentiableOn differentiable
differentiableWithinAt 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	DifferentiableAt.differentiableWithinAt differentiableAt
fderiv 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	fderiv NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toContinuousLinearMap	—	HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt
fderivWithin 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule UniqueDiffWithinAt NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	fderivWithin toContinuousLinearMap	—	DifferentiableAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace differentiableAt fderiv
hasFDerivAt 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toContinuousLinearMap	—	hasFDerivAtFilter
hasFDerivAtFilter 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	HasFDerivAtFilter SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toContinuousLinearMap	—	ContinuousLinearMap.hasFDerivAtFilter
hasFDerivWithinAt 📖	mathematical	IsBoundedLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toContinuousLinearMap	—	hasFDerivAtFilter

---

← Back to Index