MeanValue

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

Statistics

Metric	Count
Definitions	0
Theorems image_sub_le_mul_sub_of_deriv_le, image_sub_lt_mul_sub_of_deriv_lt, mul_sub_le_image_sub_of_le_deriv, mul_sub_lt_image_sub_of_lt_deriv, antitoneOn_of_deriv_nonpos, antitoneOn_of_hasDerivWithinAt_nonpos, antitone_of_deriv_nonpos, antitone_of_hasDerivAt_nonpos, domain_mvt, exists_deriv_eq_slope, exists_deriv_eq_slope', exists_hasDerivAt_eq_slope, exists_ratio_deriv_eq_ratio_slope, exists_ratio_deriv_eq_ratio_slope', exists_ratio_hasDerivAt_eq_ratio_slope, exists_ratio_hasDerivAt_eq_ratio_slope', image_sub_le_mul_sub_of_deriv_le, image_sub_lt_mul_sub_of_deriv_lt, monotoneOn_of_deriv_nonneg, monotoneOn_of_hasDerivWithinAt_nonneg, monotone_of_deriv_nonneg, monotone_of_hasDerivAt_nonneg, mul_sub_le_image_sub_of_le_deriv, mul_sub_lt_image_sub_of_lt_deriv, not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio, not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi, not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio, not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi, strictAntiOn_of_deriv_neg, strictAntiOn_of_hasDerivWithinAt_neg, strictAnti_of_deriv_neg, strictAnti_of_hasDerivAt_neg, strictMonoOn_of_deriv_pos, strictMonoOn_of_hasDerivWithinAt_pos, strictMono_of_deriv_pos, strictMono_of_hasDerivAt_pos	36
Total	36

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_sub_le_mul_sub_of_deriv_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLE deriv Set Set.instMembership	Real.instSub Real.instMul	—	deriv.fun_neg neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_sub_le_image_sub_of_le_deriv ContinuousOn.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal DifferentiableOn.neg
image_sub_lt_mul_sub_of_deriv_lt 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLT deriv Set Set.instMembership	Real.instSub Real.instMul	—	deriv.fun_neg neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt mul_sub_lt_image_sub_of_lt_deriv ContinuousOn.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal DifferentiableOn.neg
mul_sub_le_image_sub_of_le_deriv 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLE deriv Set Set.instMembership	Real.instMul Real.instSub	—	eq_or_lt_of_le sub_self MulZeroClass.mul_zero le_refl Set.OrdConnected.out ordConnected Real.instIsStrictOrderedRing Set.subset_sUnion_of_mem isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasSubset.Subset.trans Set.instIsTransSubset Set.Ioo_subset_Icc_self exists_deriv_eq_slope ContinuousOn.mono DifferentiableOn.mono le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
mul_sub_lt_image_sub_of_lt_deriv 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLT deriv Set Set.instMembership	Real.instMul Real.instSub	—	Set.OrdConnected.out ordConnected Real.instIsStrictOrderedRing Set.subset_sUnion_of_mem isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasSubset.Subset.trans Set.instIsTransSubset Set.Ioo_subset_Icc_self exists_deriv_eq_slope ContinuousOn.mono DifferentiableOn.mono lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_of_deriv_nonpos 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLE deriv Real.instZero	AntitoneOn Real.instPreorder	—	MulZeroClass.zero_mul covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Convex.image_sub_le_mul_sub_of_deriv_le
antitoneOn_of_hasDerivWithinAt_nonpos 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal interior Real.instLE Real.instZero	AntitoneOn Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal antitoneOn_of_deriv_nonpos HasDerivWithinAt.differentiableWithinAt deriv_eqOn isOpen_interior
antitone_of_deriv_nonpos 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE deriv Real.instZero	Antitone Real.instPreorder	—	antitoneOn_univ antitoneOn_of_deriv_nonpos convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
antitone_of_hasDerivAt_nonpos 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Pi.hasLe Real.instLE Pi.instZero Real.instZero	Antitone Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal antitone_of_deriv_nonpos HasDerivAt.differentiableAt HasDerivAt.deriv
domain_mvt 📖	mathematical	HasFDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Convex Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership	segment Real.instSub DFunLike.coe StrongDual ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Set.Ioo_subset_Icc_self Convex.mapsTo_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasFDerivWithinAt.comp_hasDerivWithinAt AffineMap.hasDerivWithinAt_lineMap exists_hasDerivAt_eq_slope Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike HasDerivWithinAt.continuousWithinAt HasDerivWithinAt.hasDerivAt Icc_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal segment_eq_image_lineMap Set.exists_mem_image map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass AffineMap.lineMap_apply_one AffineMap.lineMap_apply_zero sub_zero div_one
exists_deriv_eq_slope 📖	mathematical	Real Real.instLT ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Set.Ioo	Set Set.instMembership deriv DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub	—	exists_hasDerivAt_eq_slope DifferentiableAt.hasDerivAt DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
exists_deriv_eq_slope' 📖	mathematical	Real Real.instLT ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Set.Ioo	Set Set.instMembership deriv slope Real.instField NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	slope_def_field exists_deriv_eq_slope
exists_hasDerivAt_eq_slope 📖	mathematical	Real Real.instLT ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	Set Set.instMembership Set.Ioo DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal exists_ratio_hasDerivAt_eq_ratio_slope continuousOn_id hasDerivAt_id eq_div_iff sub_ne_zero LT.lt.ne' mul_comm mul_one
exists_ratio_deriv_eq_ratio_slope 📖	mathematical	Real Real.instLT ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Set.Ioo	Set Set.instMembership Real.instMul Real.instSub deriv	—	exists_ratio_hasDerivAt_eq_ratio_slope DifferentiableAt.hasDerivAt DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
exists_ratio_deriv_eq_ratio_slope' 📖	mathematical	Real Real.instLT DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioo Real.instPreorder Filter.Tendsto nhdsWithin Set.Ioi nhds Set.Iio	Set Set.instMembership Real.instMul Real.instSub deriv	—	exists_ratio_hasDerivAt_eq_ratio_slope' DifferentiableAt.hasDerivAt DifferentiableWithinAt.differentiableAt Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
exists_ratio_hasDerivAt_eq_ratio_slope 📖	mathematical	Real Real.instLT ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	Set Set.instMembership Set.Ioo Real.instMul Real.instSub	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add HasDerivAt.sub HasDerivAt.const_mul ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal ContinuousOn.mul continuousOn_const exists_hasDerivAt_eq_zero sub_eq_zero
exists_ratio_hasDerivAt_eq_ratio_slope' 📖	mathematical	Real Real.instLT HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.Tendsto nhdsWithin Set.Ioi Real.instPreorder nhds Set.Iio	Set Set.instMembership Set.Ioo Real.instMul Real.instSub	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Tendsto.mul tendsto_const_nhds Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add HasDerivAt.sub HasDerivAt.const_mul exists_hasDerivAt_eq_zero' sub_eq_zero
image_sub_le_mul_sub_of_deriv_le 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE deriv	Real.instSub Real.instMul	—	Convex.image_sub_le_mul_sub_of_deriv_le convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
image_sub_lt_mul_sub_of_deriv_lt 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT deriv	Real.instSub Real.instMul	—	Convex.image_sub_lt_mul_sub_of_deriv_lt convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
monotoneOn_of_deriv_nonneg 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace interior Real.instLE Real.instZero deriv	MonotoneOn Real.instPreorder	—	MulZeroClass.zero_mul covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Convex.mul_sub_le_image_sub_of_le_deriv
monotoneOn_of_hasDerivWithinAt_nonneg 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal interior Real.instLE Real.instZero	MonotoneOn Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal monotoneOn_of_deriv_nonneg HasDerivWithinAt.differentiableWithinAt deriv_eqOn isOpen_interior
monotone_of_deriv_nonneg 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE Real.instZero deriv	Monotone Real.instPreorder	—	monotoneOn_univ monotoneOn_of_deriv_nonneg convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
monotone_of_hasDerivAt_nonneg 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Pi.hasLe Real.instLE Pi.instZero Real.instZero	Monotone Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal monotone_of_deriv_nonneg HasDerivAt.differentiableAt HasDerivAt.deriv
mul_sub_le_image_sub_of_le_deriv 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE deriv	Real.instMul Real.instSub	—	Convex.mul_sub_le_image_sub_of_le_deriv convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
mul_sub_lt_image_sub_of_lt_deriv 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT deriv	Real.instMul Real.instSub	—	Convex.mul_sub_lt_image_sub_of_lt_deriv convex_univ Continuous.continuousOn Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Differentiable.differentiableOn
not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio 📖	mathematical	Filter.Tendsto Real deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace nhdsWithin Set.Iio Real.instPreorder Filter.atBot	DifferentiableWithinAt	—	Filter.EventuallyEq.eq_1 Filter.HasBasis.eventually_iff nhdsGT_basis instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial nhdsLT_basis instNoMinOrderOfNontrivial Filter.HasBasis.tendsto_right_iff Filter.atBot_basis instIsCodirectedOrder Real.instArchimedean lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le deriv_comp differentiableAt_of_deriv_ne_zero Set.mem_Ioo ne_of_lt Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one DifferentiableAt.fun_neg differentiableAt_id deriv_neg'' mul_neg mul_one not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi Filter.Tendsto.congr' Filter.EventuallyEq.symm Filter.Tendsto.comp Filter.tendsto_neg_atBot_atTop tendsto_neg_nhdsGT_neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal DifferentiableWithinAt.comp neg_neg DifferentiableWithinAt.fun_neg differentiableWithinAt_id IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi 📖	mathematical	Filter.Tendsto Real deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace nhdsWithin Set.Ioi Real.instPreorder Filter.atBot	DifferentiableWithinAt	—	deriv.neg' Filter.Tendsto.comp Filter.tendsto_neg_atBot_atTop Real.instIsOrderedAddMonoid not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi DifferentiableWithinAt.neg
not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio 📖	mathematical	Filter.Tendsto Real deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace nhdsWithin Set.Iio Real.instPreorder Filter.atTop	DifferentiableWithinAt	—	deriv.neg' Filter.Tendsto.comp Filter.tendsto_neg_atTop_atBot Real.instIsOrderedAddMonoid not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio DifferentiableWithinAt.neg
not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi 📖	mathematical	Filter.Tendsto Real deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace nhdsWithin Set.Ioi Real.instPreorder Filter.atTop	DifferentiableWithinAt	—	Filter.Tendsto.congr' Filter.mp_mem eventually_mem_nhdsWithin Filter.univ_mem' interior_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid derivWithin_of_mem_nhds IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul DifferentiableWithinAt.hasDerivWithinAt Filter.HasBasis.eventually_iff nhdsGT_basis instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.HasBasis.tendsto_left_iff Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder LE.le.trans_lt Filter.HasBasis.tendsto_right_iff nhds_basis_Ioo instNoMinOrderOfNontrivial Set.diff_singleton_eq_self Set.self_notMem_Ioi hasDerivWithinAt_iff_tendsto_slope IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike contravariant_lt_of_covariant_le DifferentiableWithinAt.mono ne_of_gt differentiableWithinAt_of_derivWithin_ne_zero Set.Ioc_subset_Ioi_self ContinuousWithinAt.mono_of_mem_nhdsWithin DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul nhdsWithin_eq_nhdsWithin' Ioi_mem_nhds Set.Ioc_inter_Ioi sup_of_le_left Set.ext Set.mem_Icc_of_Ioc Set.mem_of_mem_inter_left self_mem_nhdsWithin ContinuousWithinAt.mono Set.Icc_subset_Ici_self lt_of_le_of_ne exists_deriv_eq_slope' DifferentiableOn.mono Set.Ioo_subset_Ioc_self Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt max_lt_iff le_of_lt closure_Ioi LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono DifferentiableWithinAt.continuousWithinAt Set.Ici_diff_Ioi_same ContinuousWithinAt.diff_iff
strictAntiOn_of_deriv_neg 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instZero	StrictAntiOn Real.instPreorder	—	MulZeroClass.zero_mul IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Convex.image_sub_lt_mul_sub_of_deriv_lt DifferentiableAt.differentiableWithinAt differentiableAt_of_deriv_ne_zero LT.lt.ne
strictAntiOn_of_hasDerivWithinAt_neg 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal interior Real.instLT Real.instZero	StrictAntiOn Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal strictAntiOn_of_deriv_neg deriv_eqOn isOpen_interior
strictAnti_of_deriv_neg 📖	mathematical	Real Real.instLT deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	StrictAnti Real.instPreorder	—	strictAntiOn_univ strictAntiOn_of_deriv_neg convex_univ DifferentiableWithinAt.continuousWithinAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul DifferentiableAt.differentiableWithinAt differentiableAt_of_deriv_ne_zero LT.lt.ne
strictAnti_of_hasDerivAt_neg 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instLT Real.instZero	StrictAnti Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal strictAnti_of_deriv_neg HasDerivAt.deriv
strictMonoOn_of_deriv_pos 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT Real.instZero deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace	StrictMonoOn Real.instPreorder	—	DifferentiableAt.differentiableWithinAt differentiableAt_of_deriv_ne_zero LT.lt.ne' MulZeroClass.zero_mul IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Convex.mul_sub_lt_image_sub_of_lt_deriv
strictMonoOn_of_hasDerivWithinAt_pos 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal interior Real.instLT Real.instZero	StrictMonoOn Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal strictMonoOn_of_deriv_pos deriv_eqOn isOpen_interior
strictMono_of_deriv_pos 📖	mathematical	Real Real.instLT Real.instZero deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	StrictMono Real.instPreorder	—	strictMonoOn_univ strictMonoOn_of_deriv_pos convex_univ DifferentiableWithinAt.continuousWithinAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul DifferentiableAt.differentiableWithinAt differentiableAt_of_deriv_ne_zero LT.lt.ne'
strictMono_of_hasDerivAt_pos 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instLT Real.instZero	StrictMono Real.instPreorder	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal strictMono_of_deriv_pos HasDerivAt.deriv

---

← Back to Index