Basic

📁 Source: Mathlib/Analysis/Calculus/LineDeriv/Basic.lean

Statistics

Metric	Count
Definitions `HasLineDerivAt`, `HasLineDerivWithinAt`, `LineDifferentiableAt`, `LineDifferentiableWithinAt`, `lineDeriv`, `lineDerivWithin`	6
Theorems `lineDeriv_eq_fderiv`, `lineDifferentiableAt`, `lineDifferentiableWithinAt`, `hasLineDerivAt_iff`, `hasLineDerivWithinAt_iff`, `hasLineDerivWithinAt_iff_of_mem`, `lineDerivWithin_eq`, `lineDerivWithin_eq_nhds`, `lineDeriv_eq`, `lineDifferentiableAt_iff`, `lineDifferentiableWithinAt_iff`, `lineDifferentiableWithinAt_iff_of_mem`, `hasLineDerivAt`, `hasLineDerivWithinAt`, `congr_of_eventuallyEq`, `hasLineDerivWithinAt`, `le_of_lip'`, `le_of_lipschitz`, `le_of_lipschitzOn`, `lineDeriv`, `lineDifferentiableAt`, `of_comp`, `smul`, `tendsto_slope_zero`, `tendsto_slope_zero_left`, `tendsto_slope_zero_right`, `unique`, `congr'`, `congr_mono`, `congr_of_eventuallyEq`, `hasLineDerivAt`, `hasLineDerivAt'`, `lineDifferentiableWithinAt`, `mono`, `mono_of_mem_nhdsWithin`, `smul`, `congr_of_eventuallyEq`, `hasLineDerivAt`, `lineDifferentiableWithinAt`, `of_comp`, `smul`, `congr_mono`, `congr_of_eventuallyEq`, `hasLineDerivWithinAt`, `lineDifferentiableAt`, `mono`, `mono_of_mem_nhdsWithin`, `smul`, `hasLineDerivAt_iff_isLittleO_nhds_zero`, `hasLineDerivAt_iff_tendsto_slope_zero`, `hasLineDerivAt_smul_iff`, `hasLineDerivAt_zero`, `hasLineDerivWithinAt_congr_set`, `hasLineDerivWithinAt_smul_iff`, `hasLineDerivWithinAt_univ`, `hasLineDerivWithinAt_zero`, `lineDerivWithin_congr`, `lineDerivWithin_congr'`, `lineDerivWithin_congr_set`, `lineDerivWithin_of_isOpen`, `lineDerivWithin_of_mem_nhds`, `lineDerivWithin_univ`, `lineDerivWithin_zero_of_not_lineDifferentiableWithinAt`, `lineDeriv_neg`, `lineDeriv_smul`, `lineDeriv_zero`, `lineDeriv_zero_of_not_lineDifferentiableAt`, `lineDifferentiableAt_smul_iff`, `lineDifferentiableAt_zero`, `lineDifferentiableWithinAt_congr_set`, `lineDifferentiableWithinAt_smul_iff`, `lineDifferentiableWithinAt_univ`, `lineDifferentiableWithinAt_zero`, `norm_lineDeriv_le_of_lip'`, `norm_lineDeriv_le_of_lipschitz`, `norm_lineDeriv_le_of_lipschitzOn`	76
Total	82

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineDeriv_eq_fderiv` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`lineDeriv` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv`	—	`HasLineDerivAt.lineDeriv` `HasFDerivAt.hasLineDerivAt` `hasFDerivAt`
`lineDifferentiableAt` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`LineDifferentiableAt`	—	`HasLineDerivAt.lineDifferentiableAt` `HasFDerivAt.hasLineDerivAt` `hasFDerivAt`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineDifferentiableWithinAt` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`LineDifferentiableWithinAt`	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `HasFDerivWithinAt.hasLineDerivWithinAt` `hasFDerivWithinAt`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLineDerivAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`hasDerivAt_iff` `Continuous.continuousAt` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero` `ContinuousAt.preimage_mem_nhds`
`hasLineDerivWithinAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`hasDerivWithinAt_iff` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `ContinuousWithinAt.preimage_mem_nhdsWithin''` `Continuous.continuousWithinAt` `zero_smul` `add_zero`
`hasLineDerivWithinAt_iff_of_mem` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`hasLineDerivWithinAt_iff` `eq_of_nhdsWithin`
`lineDerivWithin_eq` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDerivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`derivWithin_eq` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `ContinuousWithinAt.preimage_mem_nhdsWithin''` `Continuous.continuousWithinAt` `zero_smul` `add_zero`
`lineDerivWithin_eq_nhds` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDerivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`lineDerivWithin_eq` `filter_mono` `nhdsWithin_le_nhds` `Filter.Eventually.self_of_nhds`
`lineDeriv_eq` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDeriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`lineDerivWithin_univ` `lineDerivWithin_eq_nhds`
`lineDifferentiableAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LineDifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`HasLineDerivAt.lineDifferentiableAt` `hasLineDerivAt_iff` `LineDifferentiableAt.hasLineDerivAt`
`lineDifferentiableWithinAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `hasLineDerivWithinAt_iff` `LineDifferentiableWithinAt.hasLineDerivWithinAt`
`lineDifferentiableWithinAt_iff_of_mem` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`lineDifferentiableWithinAt_iff` `eq_of_nhdsWithin`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLineDerivAt` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	—	`hasLineDerivWithinAt_univ` `HasFDerivWithinAt.hasLineDerivWithinAt` `hasFDerivWithinAt`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLineDerivWithinAt` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.hasDerivWithinAt` `HasDerivAt.add` `hasDerivAt_const` `HasDerivAt.smul_const` `IsScalarTower.left` `hasDerivAt_id'` `comp_hasDerivWithinAt` `zero_smul` `add_zero` `HasDerivWithinAt.congr_simp` `one_smul` `zero_add` `Set.mapsTo_preimage`

HasLineDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_of_eventuallyEq` 📖	—	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`Filter.EventuallyEq.hasLineDerivAt_iff` `Filter.EventuallyEq.symm`
`hasLineDerivWithinAt` 📖	mathematical	`HasLineDerivAt`	`HasLineDerivWithinAt`	—	`HasDerivAt.hasDerivWithinAt`
`le_of_lip'` 📖	—	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLE` `Real.instZero` `Filter.Eventually` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instMul` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasDerivAt.le_of_lip'` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero` `Filter.mp_mem` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `Filter.univ_mem'` `sub_zero` `mul_assoc` `add_sub_cancel_left` `norm_smul` `NormedSpace.toNormSMulClass` `mul_comm`
`le_of_lipschitz` 📖	mathematical	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal`	—	`le_of_lipschitzOn` `Filter.univ_mem` `lipschitzOnWith_univ`
`le_of_lipschitzOn` 📖	mathematical	`HasLineDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal`	—	`le_of_lip'` `NNReal.coe_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `LipschitzOnWith.norm_sub_le` `mem_of_mem_nhds`
`lineDeriv` 📖	mathematical	`HasLineDerivAt`	`lineDeriv`	—	`unique` `LineDifferentiableAt.hasLineDerivAt` `lineDifferentiableAt`
`lineDifferentiableAt` 📖	mathematical	`HasLineDerivAt`	`LineDifferentiableAt`	—	`HasDerivAt.differentiableAt`
`of_comp` 📖	—	`HasLineDerivAt` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`HasDerivAt.congr_simp` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`smul` 📖	mathematical	`HasLineDerivAt`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.toAddCommMonoid`	—	`HasLineDerivWithinAt.smul`
`tendsto_slope_zero` 📖	mathematical	`HasLineDerivAt`	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddCommGroup.toAddGroup` `nhdsWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`hasLineDerivAt_iff_tendsto_slope_zero`
`tendsto_slope_zero_left` 📖	mathematical	`HasLineDerivAt`	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddCommGroup.toAddGroup` `nhdsWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Set.Iio` `nhds`	—	`Filter.Tendsto.mono_left` `tendsto_slope_zero` `nhdsLT_le_nhdsNE`
`tendsto_slope_zero_right` 📖	mathematical	`HasLineDerivAt`	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddCommGroup.toAddGroup` `nhdsWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Set.Ioi` `nhds`	—	`Filter.Tendsto.mono_left` `tendsto_slope_zero` `nhdsGT_le_nhdsNE`
`unique` 📖	—	`HasLineDerivAt`	—	—	`HasDerivAt.unique`

HasLineDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr'` 📖	—	`HasLineDerivWithinAt` `Set.EqOn` `Set` `Set.instMembership`	—	—	`congr`
`congr_mono` 📖	—	`HasLineDerivWithinAt` `Set.EqOn` `Set` `Set.instHasSubset`	—	—	`HasDerivWithinAt.congr_mono` `zero_smul` `add_zero` `Set.preimage_mono`
`congr_of_eventuallyEq` 📖	—	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`Filter.EventuallyEq.hasLineDerivWithinAt_iff` `Filter.EventuallyEq.symm`
`hasLineDerivAt` 📖	mathematical	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`HasLineDerivAt`	—	`hasLineDerivAt'` `Filter.Tendsto.eventually` `Continuous.tendsto'` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero`
`hasLineDerivAt'` 📖	mathematical	`HasLineDerivWithinAt` `Filter.Eventually` `Set` `Set.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	`HasLineDerivAt`	—	`HasDerivWithinAt.hasDerivAt`
`lineDifferentiableWithinAt` 📖	mathematical	`HasLineDerivWithinAt`	`LineDifferentiableWithinAt`	—	`HasDerivWithinAt.differentiableWithinAt`
`mono` 📖	—	`HasLineDerivWithinAt` `Set` `Set.instHasSubset`	—	—	`HasDerivWithinAt.mono` `Set.preimage_mono`
`mono_of_mem_nhdsWithin` 📖	—	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasDerivWithinAt.mono_of_mem_nhdsWithin` `ContinuousWithinAt.preimage_mem_nhdsWithin''` `Continuous.continuousWithinAt` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero`
`smul` 📖	mathematical	`HasLineDerivWithinAt`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.toAddCommMonoid`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.congr_simp` `mul_one` `HasDerivAt.const_smul` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `hasDerivAt_id` `HasDerivWithinAt.congr_simp` `MulZeroClass.mul_zero` `HasDerivWithinAt.scomp` `IsScalarTower.left` `HasDerivAt.hasDerivWithinAt` `Set.mapsTo_preimage` `Set.ext` `mul_comm`

LineDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_of_eventuallyEq` 📖	—	`LineDifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`Filter.EventuallyEq.lineDifferentiableAt_iff` `Filter.EventuallyEq.symm`
`hasLineDerivAt` 📖	mathematical	`LineDifferentiableAt`	`HasLineDerivAt` `lineDeriv`	—	`DifferentiableAt.hasDerivAt`
`lineDifferentiableWithinAt` 📖	mathematical	`LineDifferentiableAt`	`LineDifferentiableWithinAt`	—	`DifferentiableWithinAt.mono` `differentiableWithinAt_univ` `Set.subset_univ`
`of_comp` 📖	—	`LineDifferentiableAt` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`HasLineDerivAt.lineDifferentiableAt` `HasLineDerivAt.of_comp` `hasLineDerivAt`
`smul` 📖	mathematical	`LineDifferentiableAt`	`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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`HasLineDerivAt.lineDifferentiableAt` `HasLineDerivAt.smul` `hasLineDerivAt`

LineDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_mono` 📖	—	`LineDifferentiableWithinAt` `Set.EqOn` `Set` `Set.instHasSubset`	—	—	`HasDerivWithinAt.differentiableWithinAt` `HasLineDerivWithinAt.congr_mono` `hasLineDerivWithinAt`
`congr_of_eventuallyEq` 📖	—	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasDerivWithinAt.differentiableWithinAt` `HasLineDerivWithinAt.congr_of_eventuallyEq` `hasLineDerivWithinAt`
`hasLineDerivWithinAt` 📖	mathematical	`LineDifferentiableWithinAt`	`HasLineDerivWithinAt` `lineDerivWithin`	—	`DifferentiableWithinAt.hasDerivWithinAt`
`lineDifferentiableAt` 📖	mathematical	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`LineDifferentiableAt`	—	`HasLineDerivAt.lineDifferentiableAt` `HasLineDerivWithinAt.hasLineDerivAt` `hasLineDerivWithinAt`
`mono` 📖	—	`LineDifferentiableWithinAt` `Set` `Set.instHasSubset`	—	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `HasLineDerivWithinAt.mono` `hasLineDerivWithinAt`
`mono_of_mem_nhdsWithin` 📖	—	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `HasLineDerivWithinAt.mono_of_mem_nhdsWithin` `hasLineDerivWithinAt`
`smul` 📖	mathematical	`LineDifferentiableWithinAt`	`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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `HasLineDerivWithinAt.smul` `hasLineDerivWithinAt`

(root)

Definitions

Name	Category	Theorems
`HasLineDerivAt` 📖	MathDef	11 math math: `hasLineDerivAt_iff_isLittleO_nhds_zero`, `hasLineDerivWithinAt_univ`, `hasLineDerivAt_smul_iff`, `HasLineDerivWithinAt.hasLineDerivAt`, `HasFDerivAt.hasLineDerivAt`, `hasLineDerivAt_iff_tendsto_slope_zero`, `HasLineDerivWithinAt.hasLineDerivAt'`, `hasLineDerivAt_zero`, `LineDifferentiableAt.hasLineDerivAt`, `Filter.EventuallyEq.hasLineDerivAt_iff`, `QuadraticMap.hasLineDerivAt`
`HasLineDerivWithinAt` 📖	MathDef	9 math math: `HasFDerivWithinAt.hasLineDerivWithinAt`, `LineDifferentiableWithinAt.hasLineDerivWithinAt`, `hasLineDerivWithinAt_zero`, `hasLineDerivWithinAt_smul_iff`, `hasLineDerivWithinAt_univ`, `HasLineDerivAt.hasLineDerivWithinAt`, `Filter.EventuallyEq.hasLineDerivWithinAt_iff_of_mem`, `hasLineDerivWithinAt_congr_set`, `Filter.EventuallyEq.hasLineDerivWithinAt_iff`
`LineDifferentiableAt` 📖	MathDef	11 math math: `LineDifferentiableWithinAt.lineDifferentiableAt`, `lineDifferentiableAt_smul_iff`, `HasLineDerivAt.lineDifferentiableAt`, `LipschitzWith.ae_lineDifferentiableAt`, `lineDifferentiableWithinAt_univ`, `DifferentiableAt.lineDifferentiableAt`, `QuadraticMap.lineDifferentiableAt`, `measurableSet_lineDifferentiableAt_uncurry`, `measurableSet_lineDifferentiableAt`, `lineDifferentiableAt_zero`, `Filter.EventuallyEq.lineDifferentiableAt_iff`
`LineDifferentiableWithinAt` 📖	MathDef	9 math math: `LineDifferentiableAt.lineDifferentiableWithinAt`, `lineDifferentiableWithinAt_congr_set`, `DifferentiableWithinAt.lineDifferentiableWithinAt`, `HasLineDerivWithinAt.lineDifferentiableWithinAt`, `lineDifferentiableWithinAt_univ`, `lineDifferentiableWithinAt_zero`, `Filter.EventuallyEq.lineDifferentiableWithinAt_iff_of_mem`, `lineDifferentiableWithinAt_smul_iff`, `Filter.EventuallyEq.lineDifferentiableWithinAt_iff`
`lineDeriv` 📖	CompOp	38 math math: `QuadraticMap.lineDeriv`, `measurable_lineDeriv`, `LipschitzWith.memLp_lineDeriv`, `LipschitzWith.ae_lineDeriv_sum_eq`, `Filter.EventuallyEq.lineDeriv_eq`, `lineDerivWithin_univ`, `IsLocalExtr.lineDeriv_eq_zero`, `aemeasurable_lineDeriv_uncurry`, `norm_sub_le_mul_volume_of_norm_lineDeriv_le`, `aestronglyMeasurable_lineDeriv`, `norm_lineDeriv_le_of_lipschitz`, `stronglyMeasurable_lineDeriv`, `lineDerivWithin_of_isOpen`, `IsExtrOn.lineDeriv_eq_zero`, `stronglyMeasurable_lineDeriv_uncurry`, `IsMinOn.lineDeriv_eq_zero`, `aestronglyMeasurable_lineDeriv_uncurry`, `HasLineDerivAt.lineDeriv`, `lineDeriv_zero`, `norm_lineDeriv_le_of_lipschitzOn`, `measurable_lineDeriv_uncurry`, `lineDeriv_zero_of_not_lineDifferentiableAt`, `IsLocalMax.lineDeriv_eq_zero`, `LipschitzWith.locallyIntegrable_lineDeriv`, `aemeasurable_lineDeriv`, `lineDerivWithin_of_mem_nhds`, `LineDifferentiableAt.hasLineDerivAt`, `lineDeriv_smul`, `IsMaxOn.lineDeriv_eq_zero`, `LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul`, `SchwartzMap.lineDerivOp_apply`, `IsLocalMin.lineDeriv_eq_zero`, `IsExtrFilter.lineDeriv_eq_zero`, `LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'`, `norm_lineDeriv_le_of_lip'`, `lineDeriv_neg`, `DifferentiableAt.lineDeriv_eq_fderiv`, `LipschitzWith.integral_lineDeriv_mul_eq`
`lineDerivWithin` 📖	CompOp	13 math math: `lineDerivWithin_congr`, `lineDerivWithin_zero_of_not_lineDifferentiableWithinAt`, `Filter.EventuallyEq.lineDerivWithin_eq`, `LineDifferentiableWithinAt.hasLineDerivWithinAt`, `lineDerivWithin_univ`, `IsExtrOn.lineDerivWithin_eq_zero`, `lineDerivWithin_of_isOpen`, `Filter.EventuallyEq.lineDerivWithin_eq_nhds`, `IsMinOn.lineDerivWithin_eq_zero`, `lineDerivWithin_congr'`, `IsMaxOn.lineDerivWithin_eq_zero`, `lineDerivWithin_congr_set`, `lineDerivWithin_of_mem_nhds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLineDerivAt_iff_isLittleO_nhds_zero` 📖	mathematical	—	`HasLineDerivAt` `Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `zero_add` `zero_smul` `add_zero`
`hasLineDerivAt_iff_tendsto_slope_zero` 📖	mathematical	—	`HasLineDerivAt` `Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddCommGroup.toAddGroup` `nhdsWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `zero_add` `zero_smul` `add_zero`
`hasLineDerivAt_smul_iff` 📖	mathematical	—	`HasLineDerivAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.toAddCommMonoid`	—	`smul_smul` `inv_mul_cancel₀` `one_smul` `HasLineDerivAt.smul`
`hasLineDerivAt_zero` 📖	mathematical	—	`HasLineDerivAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasDerivAt.congr_simp` `smul_zero` `add_zero`
`hasLineDerivWithinAt_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasLineDerivWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`hasDerivWithinAt_congr_set` `Continuous.continuousAt` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero` `ContinuousAt.preimage_mem_nhds`
`hasLineDerivWithinAt_smul_iff` 📖	mathematical	—	`HasLineDerivWithinAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.toAddCommMonoid`	—	`smul_smul` `inv_mul_cancel₀` `one_smul` `HasLineDerivWithinAt.smul`
`hasLineDerivWithinAt_univ` 📖	mathematical	—	`HasLineDerivWithinAt` `Set.univ` `HasLineDerivAt`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`hasLineDerivWithinAt_zero` 📖	mathematical	—	`HasLineDerivWithinAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasDerivWithinAt.congr_simp` `smul_zero` `add_zero`
`lineDerivWithin_congr` 📖	mathematical	`Set.EqOn`	`lineDerivWithin`	—	`derivWithin_congr` `zero_smul` `add_zero`
`lineDerivWithin_congr'` 📖	mathematical	`Set.EqOn` `Set` `Set.instMembership`	`lineDerivWithin`	—	`lineDerivWithin_congr`
`lineDerivWithin_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDerivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`derivWithin_congr_set` `Continuous.continuousAt` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero` `ContinuousAt.preimage_mem_nhds`
`lineDerivWithin_of_isOpen` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`lineDerivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `lineDeriv`	—	`lineDerivWithin_of_mem_nhds` `IsOpen.mem_nhds`
`lineDerivWithin_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDerivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `lineDeriv`	—	`derivWithin_of_mem_nhds` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero`
`lineDerivWithin_univ` 📖	mathematical	—	`lineDerivWithin` `Set.univ` `lineDeriv`	—	`derivWithin_univ`
`lineDerivWithin_zero_of_not_lineDifferentiableWithinAt` 📖	mathematical	`LineDifferentiableWithinAt`	`lineDerivWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`derivWithin_zero_of_not_differentiableWithinAt`
`lineDeriv_neg` 📖	mathematical	—	`lineDeriv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg_one_smul` `lineDeriv_smul`
`lineDeriv_smul` 📖	mathematical	—	`lineDeriv` `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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`eq_or_ne` `zero_smul` `lineDeriv_zero` `HasLineDerivAt.lineDeriv` `HasLineDerivAt.smul` `LineDifferentiableAt.hasLineDerivAt` `lineDifferentiableAt_smul_iff` `lineDeriv_zero_of_not_lineDifferentiableAt` `smul_zero`
`lineDeriv_zero` 📖	mathematical	—	`lineDeriv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasLineDerivAt.lineDeriv` `hasLineDerivAt_zero`
`lineDeriv_zero_of_not_lineDifferentiableAt` 📖	mathematical	`LineDifferentiableAt`	`lineDeriv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`deriv_zero_of_not_differentiableAt`
`lineDifferentiableAt_smul_iff` 📖	mathematical	—	`LineDifferentiableAt` `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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_smul` `inv_mul_cancel₀` `one_smul` `LineDifferentiableAt.smul`
`lineDifferentiableAt_zero` 📖	mathematical	—	`LineDifferentiableAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`HasLineDerivAt.lineDifferentiableAt` `hasLineDerivAt_zero`
`lineDifferentiableWithinAt_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LineDifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `hasLineDerivWithinAt_congr_set` `LineDifferentiableWithinAt.hasLineDerivWithinAt` `Filter.EventuallyEq.symm`
`lineDifferentiableWithinAt_smul_iff` 📖	mathematical	—	`LineDifferentiableWithinAt` `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` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_smul` `inv_mul_cancel₀` `one_smul` `LineDifferentiableWithinAt.smul`
`lineDifferentiableWithinAt_univ` 📖	mathematical	—	`LineDifferentiableWithinAt` `Set.univ` `LineDifferentiableAt`	—	—
`lineDifferentiableWithinAt_zero` 📖	mathematical	—	`LineDifferentiableWithinAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`HasLineDerivWithinAt.lineDifferentiableWithinAt` `hasLineDerivWithinAt_zero`
`norm_lineDeriv_le_of_lip'` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Filter.Eventually` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instMul` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`lineDeriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField`	—	`norm_deriv_le_of_lip'` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `zero_smul` `add_zero` `Filter.mp_mem` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `Filter.univ_mem'` `sub_zero` `mul_assoc` `add_sub_cancel_left` `norm_smul` `NormedSpace.toNormSMulClass` `mul_comm`
`norm_lineDeriv_le_of_lipschitz` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `lineDeriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instMul` `NNReal.toReal`	—	`norm_lineDeriv_le_of_lipschitzOn` `Filter.univ_mem` `lipschitzOnWith_univ`
`norm_lineDeriv_le_of_lipschitzOn` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `lineDeriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `Real.instMul` `NNReal.toReal`	—	`norm_lineDeriv_le_of_lip'` `NNReal.coe_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `LipschitzOnWith.norm_sub_le` `mem_of_mem_nhds`

---

← Back to Index