Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `hasFDerivAt`, `hasFDerivWithinAt`, `continuous`, `differentiableAt`, `differentiableOn`, `comp_semilinear₂`, `continuousAt`, `differentiableWithinAt`, `fderivWithin`, `hasFDerivAt`, `isBigOTVS_sub`, `isBigO_sub`, `continuousOn`, `differentiableAt`, `eventually_differentiableAt`, `hasFDerivAt`, `iUnion_of_isOpen`, `mono`, `union_of_isOpen`, `congr_nhds`, `continuousWithinAt`, `differentiableAt`, `empty`, `hasFDerivWithinAt`, `insert`, `insert'`, `isBigOTVS_sub`, `isBigO_sub`, `mono`, `mono_of_mem_nhdsWithin`, `of_finite`, `of_insert`, `of_subsingleton`, `singleton`, `comp_semilinear`, `continuousAt`, `differentiableAt`, `fderiv`, `hasFDerivAtFilter`, `hasFDerivWithinAt`, `isBigOTVS_sub`, `isBigO_sub`, `le_of_lip'`, `le_of_lipschitz`, `le_of_lipschitzOn`, `lim`, `unique`, `isBigOTVS_sub`, `isBigO_sub`, `isEquivalent_sub`, `isThetaTVS_sub`, `isTheta_sub`, `mono`, `tendsto_nhds`, `continuousWithinAt`, `differentiableWithinAt`, `empty`, `fderivWithin`, `hasFDerivAt`, `hasFDerivAt_of_univ`, `insert`, `insert'`, `isBigOTVS_sub`, `isBigO_sub`, `lim`, `mono`, `mono_of_mem_nhdsWithin`, `of_finite`, `of_insert`, `of_notMem_closure`, `of_not_accPt`, `of_subsingleton`, `singleton`, `union`, `unique_on`, `continuousAt`, `differentiableAt`, `exists_lipschitzOnWith`, `exists_lipschitzOnWith_of_nnnorm_lt`, `hasFDerivAt`, `isBigOTVS_sub`, `isBigO_sub`, `isEquivalent_sub`, `isThetaTVS_sub`, `isTheta_sub`, `eq`, `eq`, `differentiableAt_fun_id`, `differentiableAt_id`, `differentiableOn_empty`, `differentiableOn_iUnion_iff_of_isOpen`, `differentiableOn_id`, `differentiableOn_of_locally_differentiableOn`, `differentiableOn_union_iff_of_isOpen`, `differentiableOn_univ`, `differentiableWithinAt_congr_nhds`, `differentiableWithinAt_id`, `differentiableWithinAt_id'`, `differentiableWithinAt_insert`, `differentiableWithinAt_insert_self`, `differentiableWithinAt_inter`, `differentiableWithinAt_inter'`, `differentiableWithinAt_univ`, `differentiable_fun_id`, `differentiable_id`, `differentiable_of_differentiableOn_iUnion_of_isOpen`, `differentiable_of_differentiableOn_union_of_isOpen`, `fderivWithin_eq_fderiv`, `fderivWithin_id`, `fderivWithin_id'`, `fderivWithin_inter`, `fderivWithin_mem_iff`, `fderivWithin_of_isOpen`, `fderivWithin_of_mem_nhds`, `fderivWithin_of_mem_nhdsWithin`, `fderivWithin_subset`, `fderivWithin_zero_of_notMem_closure`, `fderivWithin_zero_of_not_accPt`, `fderiv_eq`, `fderiv_id`, `fderiv_id'`, `fderiv_mem_iff`, `fderiv_zero_of_not_differentiableAt`, `hasFDerivAtFilter_id`, `hasFDerivAtFilter_iff_tendsto`, `hasFDerivAt_id`, `hasFDerivAt_iff_isLittleO_nhds_zero`, `hasFDerivAt_iff_tendsto`, `hasFDerivWithinAt_diff_singleton`, `hasFDerivWithinAt_diff_singleton_self`, `hasFDerivWithinAt_id`, `hasFDerivWithinAt_iff_tendsto`, `hasFDerivWithinAt_insert`, `hasFDerivWithinAt_insert_self`, `hasFDerivWithinAt_inter`, `hasFDerivWithinAt_inter'`, `hasFDerivWithinAt_of_isOpen`, `hasFDerivWithinAt_of_mem_nhds`, `hasFDerivWithinAt_univ`, `hasStrictFDerivAt_id`, `norm_fderiv_le_of_lip'`, `norm_fderiv_le_of_lipschitz`, `norm_fderiv_le_of_lipschitzOn`	143
Total	143

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFDerivAt` 📖	mathematical	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.zero`	—	`HasFDerivWithinAt.hasFDerivAt_of_univ` `hasFDerivWithinAt` `nhdsWithin_univ` `Set.mem_univ`
`hasFDerivWithinAt` 📖	mathematical	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.instMembership`	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.zero`	—	`eq_zero_of_norm_pow_within` `LT.lt.ne_bot` `sub_zero` `trans_isLittleO` `Asymptotics.IsLittleO.mono` `Asymptotics.isLittleO_pow_sub_sub` `nhdsWithin_le_nhds`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	`Differentiable`	`Continuous`	—	`continuous_iff_continuousAt` `DifferentiableAt.continuousAt`
`differentiableAt` 📖	mathematical	`Differentiable`	`DifferentiableAt`	—	—
`differentiableOn` 📖	mathematical	`Differentiable`	`DifferentiableOn`	—	`DifferentiableOn.mono` `differentiableOn_univ` `Set.subset_univ`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_semilinear₂` 📖	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	—	—	`HasFDerivAt.differentiableAt` `RingHomInvPair.triples₂` `RingHomCompTriple.right_ids` `HasFDerivAt.comp_semilinear` `hasFDerivAt`
`continuousAt` 📖	mathematical	`DifferentiableAt`	`ContinuousAt`	—	`HasFDerivAt.continuousAt`
`differentiableWithinAt` 📖	mathematical	`DifferentiableAt`	`DifferentiableWithinAt`	—	`DifferentiableWithinAt.mono` `differentiableWithinAt_univ` `Set.subset_univ`
`fderivWithin` 📖	mathematical	`DifferentiableAt` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField`	`fderivWithin` `fderiv`	—	`HasFDerivWithinAt.fderivWithin` `HasFDerivAt.hasFDerivWithinAt` `hasFDerivAt`
`hasFDerivAt` 📖	mathematical	`DifferentiableAt`	`HasFDerivAt` `fderiv`	—	`fderiv_def` `hasFDerivWithinAt_univ` `DifferentiableWithinAt.hasFDerivWithinAt` `differentiableWithinAt_univ`
`isBigOTVS_sub` 📖	mathematical	`DifferentiableAt`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `nhds` `SubNegMonoid.toSub`	—	`HasFDerivAt.isBigOTVS_sub` `hasFDerivAt`
`isBigO_sub` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhds` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`HasFDerivAt.isBigO_sub` `hasFDerivAt`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	`DifferentiableOn`	`ContinuousOn`	—	`DifferentiableWithinAt.continuousWithinAt`
`differentiableAt` 📖	mathematical	`DifferentiableOn` `Set` `Filter` `Filter.instMembership` `nhds`	`DifferentiableAt`	—	`HasFDerivAt.differentiableAt` `hasFDerivAt`
`eventually_differentiableAt` 📖	mathematical	`DifferentiableOn` `Set` `Filter` `Filter.instMembership` `nhds`	`Filter.Eventually` `DifferentiableAt`	—	`Filter.Eventually.mono` `eventually_eventually_nhds` `differentiableAt`
`hasFDerivAt` 📖	mathematical	`DifferentiableOn` `Set` `Filter` `Filter.instMembership` `nhds`	`HasFDerivAt` `fderiv`	—	`DifferentiableAt.hasFDerivAt` `DifferentiableWithinAt.differentiableAt` `mem_of_mem_nhds`
`iUnion_of_isOpen` 📖	mathematical	`DifferentiableOn` `IsOpen`	`Set.iUnion`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt` `IsOpen.mem_nhds`
`mono` 📖	—	`DifferentiableOn` `Set` `Set.instHasSubset`	—	—	`DifferentiableWithinAt.mono`
`union_of_isOpen` 📖	mathematical	`DifferentiableOn` `IsOpen`	`Set` `Set.instUnion`	—	`DifferentiableAt.differentiableWithinAt` `DifferentiableWithinAt.differentiableAt` `IsOpen.mem_nhds`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_nhds` 📖	—	`DifferentiableWithinAt` `nhdsWithin`	—	—	`mono_of_mem_nhdsWithin` `self_mem_nhdsWithin`
`continuousWithinAt` 📖	mathematical	`DifferentiableWithinAt`	`ContinuousWithinAt`	—	`HasFDerivWithinAt.continuousWithinAt`
`differentiableAt` 📖	mathematical	`DifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`DifferentiableAt`	—	`HasFDerivWithinAt.hasFDerivAt`
`empty` 📖	mathematical	—	`DifferentiableWithinAt` `Set` `Set.instEmptyCollection`	—	`HasFDerivWithinAt.empty`
`hasFDerivWithinAt` 📖	mathematical	`DifferentiableWithinAt`	`HasFDerivWithinAt` `fderivWithin`	—	`fderivWithin_def`
`insert` 📖	mathematical	`DifferentiableWithinAt`	`Set` `Set.instInsert`	—	`differentiableWithinAt_insert_self`
`insert'` 📖	mathematical	`DifferentiableWithinAt`	`Set` `Set.instInsert`	—	`differentiableWithinAt_insert`
`isBigOTVS_sub` 📖	mathematical	`DifferentiableWithinAt`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `nhdsWithin` `SubNegMonoid.toSub`	—	`HasFDerivWithinAt.isBigOTVS_sub` `hasFDerivWithinAt`
`isBigO_sub` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhdsWithin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`HasFDerivWithinAt.isBigO_sub` `hasFDerivWithinAt`
`mono` 📖	—	`DifferentiableWithinAt` `Set` `Set.instHasSubset`	—	—	`HasFDerivWithinAt.mono`
`mono_of_mem_nhdsWithin` 📖	—	`DifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`HasFDerivWithinAt.differentiableWithinAt` `HasFDerivWithinAt.mono_of_mem_nhdsWithin` `hasFDerivWithinAt`
`of_finite` 📖	mathematical	—	`DifferentiableWithinAt`	—	`HasFDerivWithinAt.of_finite`
`of_insert` 📖	—	`DifferentiableWithinAt` `Set` `Set.instInsert`	—	—	`mono` `Set.subset_insert`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`DifferentiableWithinAt`	—	`of_finite` `Set.Subsingleton.finite`
`singleton` 📖	mathematical	—	`DifferentiableWithinAt` `Set` `Set.instSingletonSet`	—	`HasFDerivWithinAt.singleton`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_semilinear` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `RingHomInvPair.triples₂` `RingHomCompTriple.right_ids`	—	`RingHomIsometric.inv` `RingHomInvPair.triples₂` `RingHomCompTriple.right_ids` `hasFDerivAt_iff_isLittleO_nhds_zero` `Asymptotics.IsLittleO.comp_tendsto` `ContinuousAt.tendsto` `Continuous.continuousAt` `ContinuousLinearMap.continuous` `ContinuousLinearMap.map_zero` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Asymptotics.IsLittleO.trans_isBigO` `Asymptotics.IsBigO.trans_isLittleO` `ContinuousLinearMap.isBigO_comp` `ContinuousLinearMap.isBigO_id`
`continuousAt` 📖	mathematical	`HasFDerivAt`	`ContinuousAt`	—	`HasFDerivAtFilter.tendsto_nhds` `le_rfl`
`differentiableAt` 📖	mathematical	`HasFDerivAt`	`DifferentiableAt`	—	—
`fderiv` 📖	mathematical	`HasFDerivAt`	`fderiv`	—	`ContinuousLinearMap.ext` `unique` `DifferentiableAt.hasFDerivAt` `differentiableAt`
`hasFDerivAtFilter` 📖	mathematical	`HasFDerivAt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`HasFDerivAtFilter`	—	`HasFDerivAtFilter.mono`
`hasFDerivWithinAt` 📖	mathematical	`HasFDerivAt`	`HasFDerivWithinAt`	—	`hasFDerivAtFilter` `inf_le_left`
`isBigOTVS_sub` 📖	mathematical	`HasFDerivAt`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `nhds` `SubNegMonoid.toSub`	—	`HasFDerivAtFilter.isBigOTVS_sub`
`isBigO_sub` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhds` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsBigOTVS.isBigO` `isBigOTVS_sub` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`le_of_lip'` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Filter.Eventually` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instMul` `nhds`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.hasOpNorm`	—	`le_of_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ContinuousLinearMap.opNorm_le_of_nhds_zero` `RingHomIsometric.ids` `add_nonneg` `LT.lt.le` `Filter.mp_mem` `Filter.eventually_map` `map_add_left_nhds_zero` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Asymptotics.isLittleO_iff` `hasFDerivAt_iff_isLittleO_nhds_zero` `Filter.univ_mem'` `norm_le_insert` `add_le_add` `covariant_swap_add_of_covariant_add` `add_sub_cancel_left` `add_mul` `Distrib.rightDistribClass`
`le_of_lipschitz` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `NNReal.toReal`	—	`le_of_lipschitzOn` `Filter.univ_mem` `lipschitzOnWith_univ`
`le_of_lipschitzOn` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhds` `LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `NNReal.toReal`	—	`le_of_lip'` `NNReal.coe_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `LipschitzOnWith.norm_sub_le` `mem_of_mem_nhds`
`lim` 📖	mathematical	`HasFDerivAt` `Filter.Tendsto` `Real` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `Filter.atTop` `Real.instPreorder`	`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` `SubNegMonoid.toSub` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `nhds` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`HasFDerivWithinAt.lim` `hasFDerivWithinAt_univ` `zero_smul` `Filter.Tendsto.smul` `Filter.Tendsto.comp` `Filter.tendsto_inv₀_cobounded` `tendsto_norm_atTop_iff_cobounded` `tendsto_const_nhds` `Filter.Eventually.of_forall` `Set.mem_univ` `tendsto_nhds_of_eventually_eq` `Filter.Eventually.mono` `eventually_ne_of_tendsto_norm_atTop` `smul_inv_smul₀`
`unique` 📖	—	`HasFDerivAt`	—	—	`UniqueDiffWithinAt.eq` `uniqueDiffWithinAt_univ` `NormedField.nhdsNE_neBot` `nhdsWithin_univ` `eq_1`

HasFDerivAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigOTVS_sub` 📖	mathematical	`HasFDerivAtFilter`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `SubNegMonoid.toSub`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `sub_add_cancel` `Asymptotics.IsBigOTVS.fun_add` `Asymptotics.IsLittleOTVS.isBigOTVS` `isLittleOTVS` `ContinuousLinearMap.isBigOTVS_comp`
`isBigO_sub` 📖	mathematical	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsBigOTVS.isBigO` `isBigOTVS_sub` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`isEquivalent_sub` 📖	mathematical	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsEquivalent` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommGroup.toAddGroup`	—	`Asymptotics.IsEquivalent.eq_1` `Asymptotics.isLittleOTVS_iff_isLittleO` `Asymptotics.IsLittleOTVS.trans_isBigOTVS` `isLittleOTVS` `Asymptotics.IsThetaTVS.isBigOTVS` `Asymptotics.IsThetaTVS.symm` `ContinuousLinearMap.isThetaTVS_comp`
`isThetaTVS_sub` 📖	mathematical	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsThetaTVS` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsThetaTVS.trans` `Asymptotics.IsTheta.isThetaTVS` `Asymptotics.IsEquivalent.isTheta` `isEquivalent_sub` `ContinuousLinearMap.isThetaTVS_comp`
`isTheta_sub` 📖	mathematical	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsThetaTVS.isTheta` `isThetaTVS_sub`
`mono` 📖	—	`HasFDerivAtFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`Asymptotics.IsLittleOTVS.mono` `isLittleOTVS`
`tendsto_nhds` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `HasFDerivAtFilter`	`Filter.Tendsto`	—	`Asymptotics.IsBigOTVS.trans_isLittleOTVS` `isBigOTVS_sub` `Asymptotics.isLittleOTVS_one` `sub_eq_add_neg` `add_neg_cancel` `Filter.Tendsto.add_const` `Filter.tendsto_id'` `sub_add_cancel` `zero_add`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousWithinAt` 📖	mathematical	`HasFDerivWithinAt`	`ContinuousWithinAt`	—	`HasFDerivAtFilter.tendsto_nhds` `inf_le_left`
`differentiableWithinAt` 📖	mathematical	`HasFDerivWithinAt`	`DifferentiableWithinAt`	—	—
`empty` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instEmptyCollection`	—	`nhdsWithin_empty` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`fderivWithin` 📖	mathematical	`HasFDerivWithinAt` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField`	`fderivWithin`	—	`UniqueDiffWithinAt.eq` `DifferentiableWithinAt.hasFDerivWithinAt` `differentiableWithinAt`
`hasFDerivAt` 📖	mathematical	`HasFDerivWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`HasFDerivAt`	—	`hasFDerivWithinAt_univ` `hasFDerivWithinAt_inter` `Set.univ_inter`
`hasFDerivAt_of_univ` 📖	mathematical	`HasFDerivWithinAt` `Set.univ`	`HasFDerivAt`	—	`hasFDerivWithinAt_univ`
`insert` 📖	mathematical	`HasFDerivWithinAt`	`Set` `Set.instInsert`	—	`hasFDerivWithinAt_insert_self`
`insert'` 📖	mathematical	`HasFDerivWithinAt`	`Set` `Set.instInsert`	—	`hasFDerivWithinAt_insert`
`isBigOTVS_sub` 📖	mathematical	`HasFDerivWithinAt`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `nhdsWithin` `SubNegMonoid.toSub`	—	`HasFDerivAtFilter.isBigOTVS_sub`
`isBigO_sub` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhdsWithin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsBigOTVS.isBigO` `isBigOTVS_sub` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`lim` 📖	mathematical	`HasFDerivWithinAt` `Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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`	`SubNegMonoid.toSub` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`tendsto_nhdsWithin_iff` `add_zero` `Filter.Tendsto.add` `tendsto_const_nhds` `smul_sub` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_sub_cancel_left` `Asymptotics.IsLittleOTVS.smul_left` `Asymptotics.IsLittleOTVS.comp_tendsto` `HasFDerivAtFilter.isLittleOTVS` `Asymptotics.Filter.Tendsto.isBigOTVS_one` `sub_add_cancel` `zero_add` `Asymptotics.isLittleOTVS_one` `Filter.Tendsto.comp` `Continuous.tendsto` `ContinuousMapClass.map_continuous` `ContinuousSemilinearMapClass.toContinuousMapClass`
`mono` 📖	—	`HasFDerivWithinAt` `Set` `Set.instHasSubset`	—	—	`HasFDerivAtFilter.mono` `nhdsWithin_mono`
`mono_of_mem_nhdsWithin` 📖	—	`HasFDerivWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`HasFDerivAtFilter.mono` `nhdsWithin_le_iff`
`of_finite` 📖	mathematical	—	`HasFDerivWithinAt`	—	`Set.Finite.induction_on` `empty` `insert'`
`of_insert` 📖	—	`HasFDerivWithinAt` `Set` `Set.instInsert`	—	—	`mono` `Set.subset_insert`
`of_notMem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`HasFDerivWithinAt`	—	`of_not_accPt` `ClusterPt.mem_closure` `AccPt.clusterPt`
`of_not_accPt` 📖	mathematical	`AccPt` `Filter.principal`	`HasFDerivWithinAt`	—	`hasFDerivWithinAt_diff_singleton_self` `eq_1` `Filter.not_neBot` `accPt_principal_iff_nhdsWithin` `hasFDerivAtFilter_iff_isLittleOTVS` `Asymptotics.IsLittleOTVS.bot`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`HasFDerivWithinAt`	—	`of_finite` `Set.Subsingleton.finite`
`singleton` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instSingletonSet`	—	`of_finite` `Set.finite_singleton`
`union` 📖	mathematical	`HasFDerivWithinAt`	`Set` `Set.instUnion`	—	`nhdsWithin_union` `Asymptotics.IsLittleOTVS.sup` `HasFDerivAtFilter.isLittleOTVS`
`unique_on` 📖	mathematical	`HasFDerivWithinAt`	`Set.EqOn` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `tangentConeAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`exists_fun_of_mem_tangentConeAt` `tendsto_nhds_unique` `lim`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt` 📖	mathematical	`HasStrictFDerivAt`	`ContinuousAt`	—	`HasFDerivAt.continuousAt` `hasFDerivAt`
`differentiableAt` 📖	mathematical	`HasStrictFDerivAt`	`DifferentiableAt`	—	`HasFDerivAt.differentiableAt` `hasFDerivAt`
`exists_lipschitzOnWith` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set` `Filter` `Filter.instMembership` `nhds` `LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`RingHomIsometric.ids` `exists_lipschitzOnWith_of_nnnorm_lt` `NoMaxOrder.exists_gt` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing`
`exists_lipschitzOnWith_of_nnnorm_lt` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Set` `Filter` `Filter.instMembership` `nhds` `LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`RingHomIsometric.ids` `Asymptotics.IsLittleO.add_isBigOWith` `isLittleO` `ContinuousLinearMap.isBigOWith_comp` `exists_nhds_square` `sub_add_cancel` `Asymptotics.IsBigOWith_def` `IsOpen.mem_nhds` `lipschitzOnWith_iff_norm_sub_le` `Set.mk_mem_prod`
`hasFDerivAt` 📖	mathematical	`HasStrictFDerivAt`	`HasFDerivAt`	—	`Asymptotics.IsLittleOTVS.comp_tendsto` `isLittleOTVS` `Filter.Tendsto.prodMk_nhds` `Filter.tendsto_id` `tendsto_const_nhds`
`isBigOTVS_sub` 📖	mathematical	`HasStrictFDerivAt`	`Asymptotics.IsBigOTVS` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `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` `nhds` `instTopologicalSpaceProd` `SubNegMonoid.toSub`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `sub_add_cancel` `Asymptotics.IsBigOTVS.fun_add` `Asymptotics.IsLittleOTVS.isBigOTVS` `isLittleOTVS` `ContinuousLinearMap.isBigOTVS_comp`
`isBigO_sub` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhds` `instTopologicalSpaceProd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsBigOTVS.isBigO` `isBigOTVS_sub` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`isEquivalent_sub` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsEquivalent` `nhds` `instTopologicalSpaceProd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommGroup.toAddGroup`	—	`Asymptotics.IsEquivalent.eq_1` `Asymptotics.isLittleOTVS_iff_isLittleO` `Asymptotics.IsLittleOTVS.trans_isBigOTVS` `isLittleOTVS` `Asymptotics.IsThetaTVS.isBigOTVS` `Asymptotics.IsThetaTVS.symm` `ContinuousLinearMap.isThetaTVS_comp`
`isThetaTVS_sub` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsThetaTVS` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddGroup.toContinuousENorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `nhds` `instTopologicalSpaceProd` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsThetaTVS.trans` `Asymptotics.IsTheta.isThetaTVS` `Asymptotics.IsEquivalent.isTheta` `isEquivalent_sub` `ContinuousLinearMap.isThetaTVS_comp`
`isTheta_sub` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Topology.IsInducing` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm` `nhds` `instTopologicalSpaceProd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Asymptotics.IsThetaTVS.isTheta` `isThetaTVS_sub`

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Set` `Set.instMembership` `HasFDerivWithinAt`	—	—	`UniqueDiffWithinAt.eq`

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `HasFDerivWithinAt`	—	—	`ContinuousLinearMap.ext_on` `dense_tangentConeAt` `HasFDerivWithinAt.unique_on`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableAt_fun_id` 📖	mathematical	—	`DifferentiableAt`	—	`HasFDerivAt.differentiableAt` `hasFDerivAt_id`
`differentiableAt_id` 📖	mathematical	—	`DifferentiableAt`	—	`HasFDerivAt.differentiableAt` `hasFDerivAt_id`
`differentiableOn_empty` 📖	mathematical	—	`DifferentiableOn` `Set` `Set.instEmptyCollection`	—	—
`differentiableOn_iUnion_iff_of_isOpen` 📖	mathematical	`IsOpen`	`DifferentiableOn` `Set.iUnion`	—	`DifferentiableOn.mono` `Set.subset_iUnion_of_subset` `DifferentiableOn.iUnion_of_isOpen`
`differentiableOn_id` 📖	mathematical	—	`DifferentiableOn`	—	`Differentiable.differentiableOn` `differentiable_id`
`differentiableOn_of_locally_differentiableOn` 📖	—	`IsOpen` `Set` `Set.instMembership` `DifferentiableOn` `Set.instInter`	—	—	`differentiableWithinAt_inter` `IsOpen.mem_nhds`
`differentiableOn_union_iff_of_isOpen` 📖	mathematical	`IsOpen`	`DifferentiableOn` `Set` `Set.instUnion`	—	`DifferentiableOn.mono` `Set.subset_union_left` `Set.subset_union_right` `DifferentiableOn.union_of_isOpen`
`differentiableOn_univ` 📖	mathematical	—	`DifferentiableOn` `Set.univ` `Differentiable`	—	—
`differentiableWithinAt_congr_nhds` 📖	mathematical	`nhdsWithin`	`DifferentiableWithinAt`	—	`DifferentiableWithinAt.congr_nhds`
`differentiableWithinAt_id` 📖	mathematical	—	`DifferentiableWithinAt`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt_id`
`differentiableWithinAt_id'` 📖	mathematical	—	`DifferentiableWithinAt`	—	`differentiableWithinAt_id`
`differentiableWithinAt_insert` 📖	mathematical	—	`DifferentiableWithinAt` `Set` `Set.instInsert`	—	—
`differentiableWithinAt_insert_self` 📖	mathematical	—	`DifferentiableWithinAt` `Set` `Set.instInsert`	—	`DifferentiableWithinAt.mono` `Set.subset_insert` `HasFDerivWithinAt.differentiableWithinAt` `HasFDerivWithinAt.insert` `DifferentiableWithinAt.hasFDerivWithinAt`
`differentiableWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`DifferentiableWithinAt` `Set.instInter`	—	`hasFDerivWithinAt_inter`
`differentiableWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`DifferentiableWithinAt` `Set.instInter`	—	`hasFDerivWithinAt_inter'`
`differentiableWithinAt_univ` 📖	mathematical	—	`DifferentiableWithinAt` `Set.univ` `DifferentiableAt`	—	—
`differentiable_fun_id` 📖	mathematical	—	`Differentiable`	—	`differentiableAt_id`
`differentiable_id` 📖	mathematical	—	`Differentiable`	—	`differentiableAt_id`
`differentiable_of_differentiableOn_iUnion_of_isOpen` 📖	mathematical	`DifferentiableOn` `IsOpen` `Set.iUnion` `Set.univ`	`Differentiable`	—	`differentiableOn_univ` `DifferentiableOn.iUnion_of_isOpen`
`differentiable_of_differentiableOn_union_of_isOpen` 📖	mathematical	`DifferentiableOn` `Set` `Set.instUnion` `Set.univ` `IsOpen`	`Differentiable`	—	`differentiableOn_univ` `DifferentiableOn.union_of_isOpen`
`fderivWithin_eq_fderiv` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DifferentiableAt`	`fderivWithin` `fderiv`	—	`fderivWithin_univ` `fderivWithin_subset` `Set.subset_univ` `DifferentiableAt.differentiableWithinAt`
`fderivWithin_id` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField`	`fderivWithin` `ContinuousLinearMap.id` `AddCommGroup.toAddCommMonoid`	—	`DifferentiableAt.fderivWithin` `differentiableAt_id` `fderiv_id`
`fderivWithin_id'` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField`	`fderivWithin` `ContinuousLinearMap.id` `AddCommGroup.toAddCommMonoid`	—	`fderivWithin_id`
`fderivWithin_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`fderivWithin` `Set.instInter`	—	`hasFDerivWithinAt_inter` `fderivWithin_def`
`fderivWithin_mem_iff` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `fderivWithin` `DifferentiableWithinAt` `ContinuousLinearMap.zero`	—	`fderivWithin_zero_of_not_differentiableWithinAt`
`fderivWithin_of_isOpen` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`fderivWithin` `fderiv`	—	`fderivWithin_of_mem_nhds` `IsOpen.mem_nhds`
`fderivWithin_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`fderivWithin` `fderiv`	—	`fderivWithin_univ` `Set.univ_inter` `fderivWithin_inter`
`fderivWithin_of_mem_nhdsWithin` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DifferentiableWithinAt`	`fderivWithin`	—	`HasFDerivWithinAt.fderivWithin` `HasFDerivWithinAt.mono_of_mem_nhdsWithin` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderivWithin_subset` 📖	mathematical	`Set` `Set.instHasSubset` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DifferentiableWithinAt`	`fderivWithin`	—	`fderivWithin_of_mem_nhdsWithin` `nhdsWithin_mono` `self_mem_nhdsWithin`
`fderivWithin_zero_of_notMem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`fderivWithin` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero`	—	`fderivWithin_zero_of_not_accPt` `ClusterPt.mem_closure` `AccPt.clusterPt`
`fderivWithin_zero_of_not_accPt` 📖	mathematical	`AccPt` `Filter.principal`	`fderivWithin` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero`	—	`fderivWithin_def` `HasFDerivWithinAt.of_not_accPt`
`fderiv_eq` 📖	mathematical	`HasFDerivAt`	`fderiv`	—	`HasFDerivAt.fderiv`
`fderiv_id` 📖	mathematical	—	`fderiv` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`HasFDerivAt.fderiv` `hasFDerivAt_id`
`fderiv_id'` 📖	mathematical	—	`fderiv` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`fderiv_id`
`fderiv_mem_iff` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `fderiv` `DifferentiableAt` `ContinuousLinearMap.zero`	—	`fderiv_zero_of_not_differentiableAt`
`fderiv_zero_of_not_differentiableAt` 📖	mathematical	`DifferentiableAt`	`fderiv` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero`	—	`fderiv_def` `fderivWithin_zero_of_not_differentiableWithinAt` `differentiableWithinAt_univ`
`hasFDerivAtFilter_id` 📖	mathematical	—	`HasFDerivAtFilter` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`Asymptotics.IsLittleOTVS.congr_left` `Asymptotics.IsLittleOTVS.zero` `sub_self`
`hasFDerivAtFilter_iff_tendsto` 📖	mathematical	—	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`sub_eq_zero` `norm_eq_zero` `sub_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `norm_zero` `hasFDerivAtFilter_iff_isLittleO` `Asymptotics.isLittleO_norm_left` `Asymptotics.isLittleO_norm_right` `Asymptotics.isLittleO_iff_tendsto` `Filter.tendsto_congr` `div_eq_inv_mul`
`hasFDerivAt_id` 📖	mathematical	—	`HasFDerivAt` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`hasFDerivAtFilter_id`
`hasFDerivAt_iff_isLittleO_nhds_zero` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`HasFDerivAt.eq_1` `hasFDerivAtFilter_iff_isLittleO` `map_add_left_nhds_zero` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Asymptotics.isLittleO_map` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_sub_cancel_left`
`hasFDerivAt_iff_tendsto` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`hasFDerivAtFilter_iff_tendsto`
`hasFDerivWithinAt_diff_singleton` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`hasFDerivWithinAt_insert` `Set.insert_diff_singleton`
`hasFDerivWithinAt_diff_singleton_self` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`hasFDerivWithinAt_insert_self` `Set.insert_diff_singleton`
`hasFDerivWithinAt_id` 📖	mathematical	—	`HasFDerivWithinAt` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`hasFDerivAtFilter_id`
`hasFDerivWithinAt_iff_tendsto` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `nhdsWithin` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`hasFDerivAtFilter_iff_tendsto`
`hasFDerivWithinAt_insert` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instInsert`	—	`eq_or_ne` `hasFDerivWithinAt_insert_self` `HasFDerivWithinAt.of_insert` `HasFDerivWithinAt.mono_of_mem_nhdsWithin` `nhdsWithin_insert_of_ne`
`hasFDerivWithinAt_insert_self` 📖	mathematical	—	`HasFDerivWithinAt` `Set` `Set.instInsert`	—	`Asymptotics.isLittleOTVS_insert` `sub_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`hasFDerivWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`HasFDerivWithinAt` `Set.instInter`	—	`nhdsWithin_restrict'`
`hasFDerivWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`HasFDerivWithinAt` `Set.instInter`	—	`nhdsWithin_restrict''`
`hasFDerivWithinAt_of_isOpen` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`HasFDerivWithinAt` `HasFDerivAt`	—	`hasFDerivWithinAt_of_mem_nhds` `IsOpen.mem_nhds`
`hasFDerivWithinAt_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`HasFDerivWithinAt` `HasFDerivAt`	—	`HasFDerivAt.eq_1` `HasFDerivWithinAt.eq_1` `nhdsWithin_eq_nhds`
`hasFDerivWithinAt_univ` 📖	mathematical	—	`HasFDerivWithinAt` `Set.univ` `HasFDerivAt`	—	`nhdsWithin_univ`
`hasStrictFDerivAt_id` 📖	mathematical	—	`HasStrictFDerivAt` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`Asymptotics.IsLittleOTVS.congr_left` `Asymptotics.IsLittleOTVS.zero` `sub_self`
`norm_fderiv_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`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `fderiv`	—	`HasFDerivAt.le_of_lip'` `DifferentiableAt.hasFDerivAt` `fderiv_zero_of_not_differentiableAt` `norm_zero` `RingHomIsometric.ids`
`norm_fderiv_le_of_lipschitz` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `fderiv` `NNReal.toReal`	—	`norm_fderiv_le_of_lipschitzOn` `Filter.univ_mem` `lipschitzOnWith_univ`
`norm_fderiv_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` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `fderiv` `NNReal.toReal`	—	`norm_fderiv_le_of_lip'` `NNReal.coe_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `LipschitzOnWith.norm_sub_le` `mem_of_mem_nhds`

---

← Back to Index