Documentation Verification Report

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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `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`	—	`hasFDerivAtFilter`

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` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`hasFDerivAtFilter`
`hasFDerivAtFilter` 📖	mathematical	`IsBoundedLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule`	`HasFDerivAtFilter` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`ContinuousLinearMap.hasFDerivAtFilter`
`hasFDerivWithinAt` 📖	mathematical	`IsBoundedLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule`	`HasFDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`hasFDerivAtFilter`

---

← Back to Index