Abs

📁 Source: Mathlib/Analysis/Calculus/Deriv/Abs.lean

Statistics

Metric	Count
Definitions	0
Theorems `abs`, `abs`, `abs`, `abs`, `abs`, `abs`, `abs_of_neg`, `abs_of_pos`, `abs`, `abs`, `abs_of_neg`, `abs_of_pos`, `abs`, `abs_of_neg`, `abs_of_pos`, `abs`, `abs_of_neg`, `abs_of_pos`, `abs`, `abs_of_neg`, `abs_of_pos`, `contDiffAt_abs`, `contDiffOn_abs`, `contDiffWithinAt_abs`, `deriv_abs`, `deriv_abs_neg`, `deriv_abs_pos`, `deriv_abs_zero`, `differentiableAt_abs`, `differentiableAt_abs_neg`, `differentiableAt_abs_pos`, `differentiableOn_abs`, `differentiableWithinAt_abs`, `differentiableWithinAt_abs_neg`, `differentiableWithinAt_abs_pos`, `hasDerivAt_abs`, `hasDerivAt_abs_neg`, `hasDerivAt_abs_pos`, `hasDerivWithinAt_abs`, `hasDerivWithinAt_abs_neg`, `hasDerivWithinAt_abs_pos`, `hasStrictDerivAt_abs`, `hasStrictDerivAt_abs_neg`, `hasStrictDerivAt_abs_pos`, `not_differentiableAt_abs_zero`	45
Total	45

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat`	`abs` `Real.lattice` `Real.instAddGroup`	—	`contDiff_iff_contDiffAt` `ContDiffAt.abs` `contDiffAt`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat`	`abs` `Real.lattice` `Real.instAddGroup`	—	`norm`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat`	`abs` `Real.lattice` `Real.instAddGroup`	—	`ContDiffWithinAt.abs`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat`	`abs` `Real.lattice` `Real.instAddGroup`	—	`ContDiffAt.comp_contDiffWithinAt` `contDiffAt_abs`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.abs`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup`	—	`comp` `differentiableAt_abs`
`abs_of_neg` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`comp` `differentiableAt_abs_neg`
`abs_of_pos` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`comp` `differentiableAt_abs_pos`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableWithinAt.abs`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.comp_differentiableWithinAt` `differentiableAt_abs`
`abs_of_neg` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.comp_differentiableWithinAt` `differentiableAt_abs_neg`
`abs_of_pos` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.comp_differentiableWithinAt` `differentiableAt_abs_pos`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `ContinuousLinearMap.ext` `mul_comm` `comp` `HasDerivAt.hasFDerivAt` `hasDerivAt_abs`
`abs_of_neg` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.neg` `Real.instRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instIsTopologicalAddGroupReal`	—	`instIsTopologicalAddGroupReal` `RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.ext` `mul_neg` `mul_one` `comp` `HasDerivAt.hasFDerivAt` `hasDerivAt_abs_neg`
`abs_of_pos` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.ext` `mul_one` `comp` `HasDerivAt.hasFDerivAt` `hasDerivAt_abs_pos`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`HasDerivAt.comp_hasFDerivWithinAt` `hasDerivAt_abs`
`abs_of_neg` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.neg` `Real.instRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instIsTopologicalAddGroupReal`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsUniformAddGroupReal` `instIsTopologicalRingReal` `neg_smul` `one_smul` `HasDerivAt.comp_hasFDerivWithinAt` `hasDerivAt_abs_neg`
`abs_of_pos` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `one_smul` `instIsUniformAddGroupReal` `instIsTopologicalRingReal` `HasDerivAt.comp_hasFDerivWithinAt` `hasDerivAt_abs_pos`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`HasStrictFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `ContinuousLinearMap.ext` `mul_comm` `comp` `HasStrictDerivAt.hasStrictFDerivAt` `hasStrictDerivAt_abs`
`abs_of_neg` 📖	mathematical	`HasStrictFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.neg` `Real.instRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instIsTopologicalAddGroupReal`	—	`instIsTopologicalAddGroupReal` `RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.ext` `mul_neg` `mul_one` `comp` `HasStrictDerivAt.hasStrictFDerivAt` `hasStrictDerivAt_abs_neg`
`abs_of_pos` 📖	mathematical	`HasStrictFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`abs` `Real.lattice` `Real.instAddGroup`	—	`RingHomCompTriple.ids` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.ext` `mul_one` `comp` `HasStrictDerivAt.hasStrictFDerivAt` `hasStrictDerivAt_abs_pos`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_abs` 📖	mathematical	—	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `abs` `Real.lattice` `Real.instAddGroup`	—	`contDiffAt_norm`
`contDiffOn_abs` 📖	mathematical	—	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `abs` `Real.lattice` `Real.instAddGroup`	—	`contDiffWithinAt_abs`
`contDiffWithinAt_abs` 📖	mathematical	—	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `abs` `Real.lattice` `Real.instAddGroup`	—	`ContDiffAt.contDiffWithinAt` `contDiffAt_abs`
`deriv_abs` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`eq_or_ne` `sign_zero` `deriv_abs_zero` `HasDerivAt.deriv` `hasDerivAt_abs`
`deriv_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `Real.instNeg` `Real.instOne`	—	`HasDerivAt.deriv` `hasDerivAt_abs_neg`
`deriv_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	—	`HasDerivAt.deriv` `hasDerivAt_abs_pos`
`deriv_abs_zero` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `Real.instZero`	—	`deriv_zero_of_not_differentiableAt` `not_differentiableAt_abs_zero`
`differentiableAt_abs` 📖	mathematical	—	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`HasDerivAt.differentiableAt` `hasDerivAt_abs`
`differentiableAt_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`HasDerivAt.differentiableAt` `hasDerivAt_abs_neg`
`differentiableAt_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`HasDerivAt.differentiableAt` `hasDerivAt_abs_pos`
`differentiableOn_abs` 📖	mathematical	—	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`differentiableWithinAt_abs`
`differentiableWithinAt_abs` 📖	mathematical	—	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt_abs`
`differentiableWithinAt_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt_abs_neg`
`differentiableWithinAt_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt_abs_pos`
`hasDerivAt_abs` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_abs`
`hasDerivAt_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instNeg` `Real.instOne`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_abs_neg`
`hasDerivAt_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_abs_pos`
`hasDerivWithinAt_abs` 📖	mathematical	—	`HasDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`HasDerivAt.hasDerivWithinAt` `hasDerivAt_abs`
`hasDerivWithinAt_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instNeg` `Real.instOne`	—	`HasDerivAt.hasDerivWithinAt` `hasDerivAt_abs_neg`
`hasDerivWithinAt_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	—	`HasDerivAt.hasDerivWithinAt` `hasDerivAt_abs_pos`
`hasStrictDerivAt_abs` 📖	mathematical	—	`HasStrictDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Ne.lt_or_gt` `HasStrictDerivAt.congr_simp` `sign_neg` `SignType.coe_neg` `hasStrictDerivAt_abs_neg` `sign_pos` `hasStrictDerivAt_abs_pos`
`hasStrictDerivAt_abs_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasStrictDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instNeg` `Real.instOne`	—	`HasStrictFDerivAt.congr_of_eventuallyEq` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `hasStrictDerivAt_neg` `Set.EqOn.eventuallyEq_of_mem` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.mem_Iio` `Iio_mem_nhds` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal`
`hasStrictDerivAt_abs_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasStrictDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	—	`HasStrictFDerivAt.congr_of_eventuallyEq` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `hasStrictDerivAt_id` `Set.EqOn.eventuallyEq_of_mem` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.mem_Iio` `Ioi_mem_nhds` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal`
`not_differentiableAt_abs_zero` 📖	mathematical	—	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `abs` `Real.lattice` `Real.instAddGroup` `Real.instZero`	—	`UniqueDiffWithinAt.eq_deriv` `uniqueDiffOn_Ici` `Set.self_mem_Ici` `HasDerivAt.hasDerivWithinAt` `DifferentiableAt.hasDerivAt` `HasDerivWithinAt.congr_of_mem` `hasDerivWithinAt_id` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `uniqueDiffOn_Iic` `Set.self_mem_Iic` `hasDerivWithinAt_neg` `abs_of_nonpos` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.mul_neg` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `neg_eq_zero` `sub_eq_zero_of_eq`

---

← Back to Index