MeanValue

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

Statistics

Metric	Count
Definitions	0
Theorems eqOn_of_fderivWithin_eq, exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt, exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt, instPathConnectedSpace, isLittleO_pow_succ, isLittleO_pow_succ_real, is_const_of_fderivWithin_eq_zero, lipschitzOnWith_of_nnnorm_derivWithin_le, lipschitzOnWith_of_nnnorm_deriv_le, lipschitzOnWith_of_nnnorm_fderivWithin_le, lipschitzOnWith_of_nnnorm_fderiv_le, lipschitzOnWith_of_nnnorm_hasDerivWithin_le, lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, norm_image_sub_le_of_norm_derivWithin_le, norm_image_sub_le_of_norm_deriv_le, norm_image_sub_le_of_norm_fderivWithin_le, norm_image_sub_le_of_norm_fderivWithin_le', norm_image_sub_le_of_norm_fderiv_le, norm_image_sub_le_of_norm_fderiv_le', norm_image_sub_le_of_norm_hasDerivWithin_le, norm_image_sub_le_of_norm_hasFDerivWithin_le, norm_image_sub_le_of_norm_hasFDerivWithin_le', eqOn_of_deriv_eq, eqOn_of_fderiv_eq, exists_eq_add_of_deriv_eq, exists_eq_add_of_fderiv_eq, exists_is_const_of_deriv_eq_zero, exists_is_const_of_fderiv_eq_zero, isOpen_inter_preimage_of_deriv_eq_zero, isOpen_inter_preimage_of_fderiv_eq_zero, is_const_of_deriv_eq_zero, is_const_of_fderiv_eq_zero, constant_of_derivWithin_zero, constant_of_has_deriv_right_zero, eq_of_derivWithin_eq, eq_of_fderiv_eq, eq_of_has_deriv_right_eq, hasStrictDerivAt_of_hasDerivAt_of_continuousAt, hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt, image_le_of_deriv_right_le_deriv_boundary, image_le_of_deriv_right_lt_deriv_boundary, image_le_of_deriv_right_lt_deriv_boundary', image_le_of_liminf_slope_right_le_deriv_boundary, image_le_of_liminf_slope_right_lt_deriv_boundary, image_le_of_liminf_slope_right_lt_deriv_boundary', image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary, image_norm_le_of_norm_deriv_right_le_deriv_boundary, image_norm_le_of_norm_deriv_right_le_deriv_boundary', image_norm_le_of_norm_deriv_right_lt_deriv_boundary, image_norm_le_of_norm_deriv_right_lt_deriv_boundary', isLocallyConstant_of_fderiv_eq_zero, is_const_of_deriv_eq_zero, is_const_of_fderiv_eq_zero, lipschitzWith_of_nnnorm_deriv_le, lipschitzWith_of_nnnorm_fderiv_le, norm_image_sub_le_of_norm_deriv_le_segment, norm_image_sub_le_of_norm_deriv_le_segment', norm_image_sub_le_of_norm_deriv_le_segment_01, norm_image_sub_le_of_norm_deriv_le_segment_01', norm_image_sub_le_of_norm_deriv_right_le_segment	60
Total	60

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_of_fderivWithin_eq 📖	—	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField DifferentiableOn NormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set.EqOn ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderivWithin SeminormedAddCommGroup.toAddCommGroup Set Set.instMembership	—	—	is_const_of_fderivWithin_eq_zero DifferentiableOn.sub SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin_sub RingHomIsometric.ids sub_eq_zero sub_self
exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Filter.Eventually HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField nhdsWithin ContinuousWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup	Set Filter Filter.instMembership LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt NoMaxOrder.exists_gt IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing
exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Filter.Eventually HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField nhdsWithin ContinuousWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	Set Filter Filter.instMembership LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids Metric.mem_nhdsWithin_iff Filter.Eventually.and Filter.Tendsto.eventually ContinuousWithinAt.nnnorm gt_mem_nhds NNReal.instOrderTopology inter_mem_nhdsWithin Metric.ball_mem_nhds lipschitzOnWith_of_nnnorm_hasFDerivWithin_le HasFDerivWithinAt.mono Set.inter_comm Set.inter_subset_left LT.lt.le inter convex_ball
instPathConnectedSpace 📖	mathematical	—	PathConnectedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	NormedSpace.instPathConnectedSpace
isLittleO_pow_succ 📖	—	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Set Set.instMembership HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField Asymptotics.IsLittleO ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.hasOpNorm Real.norm nhdsWithin Monoid.toNatPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—	Asymptotics.isLittleO_iff norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass pow_succ norm_norm eventually_mem_nhdsWithin Filter.mp_mem eventually_nhdsWithin_segment NormedSpace.toLocallyConvexSpace Filter.univ_mem' segment_subset LE.le.trans mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono norm_nonneg norm_sub_le_of_mem_segment le_of_lt sub_self sub_zero norm_image_sub_le_of_norm_hasFDerivWithin_le HasFDerivWithinAt.mono convex_segment left_mem_segment Real.instZeroLEOneClass right_mem_segment
isLittleO_pow_succ_real 📖	mathematical	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Asymptotics.IsLittleO NormedAddCommGroup.toNorm Real.norm nhdsWithin Monoid.toNatPow Real.instMonoid Real.instSub	SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul isLittleO_pow_succ instIsRCLikeNormedField Asymptotics.isLittleO_iff ContinuousLinearMap.norm_toSpanSingleton norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass abs_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
is_const_of_fderivWithin_eq_zero 📖	—	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField DifferentiableOn NormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField fderivWithin ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero Set Set.instMembership	—	—	norm_zero RingHomIsometric.ids dist_eq_norm MulZeroClass.zero_mul norm_image_sub_le_of_norm_fderivWithin_le
lipschitzOnWith_of_nnnorm_derivWithin_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup derivWithin	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace NormedAddCommGroup.toMetricSpace	—	lipschitzOnWith_of_nnnorm_hasDerivWithin_le DifferentiableWithinAt.hasDerivWithinAt
lipschitzOnWith_of_nnnorm_deriv_le 📖	mathematical	DifferentiableAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup deriv Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace NormedAddCommGroup.toMetricSpace	—	lipschitzOnWith_of_nnnorm_hasDerivWithin_le HasDerivAt.hasDerivWithinAt DifferentiableAt.hasDerivAt
lipschitzOnWith_of_nnnorm_fderivWithin_le 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing fderivWithin Convex Real Real.semiring 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 Real.normedField	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	RingHomIsometric.ids lipschitzOnWith_of_nnnorm_hasFDerivWithin_le DifferentiableWithinAt.hasFDerivWithinAt
lipschitzOnWith_of_nnnorm_fderiv_le 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing fderiv Convex Real Real.semiring 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 Real.normedField	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	RingHomIsometric.ids lipschitzOnWith_of_nnnorm_hasFDerivWithin_le HasFDerivAt.hasFDerivWithinAt DifferentiableAt.hasFDerivAt
lipschitzOnWith_of_nnnorm_hasDerivWithin_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace NormedAddCommGroup.toMetricSpace	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul lipschitzOnWith_of_nnnorm_hasFDerivWithin_le instIsRCLikeNormedField HasDerivWithinAt.hasFDerivWithinAt le_trans RingHomIsometric.ids ContinuousLinearMap.nnnorm_toSpanSingleton
lipschitzOnWith_of_nnnorm_hasFDerivWithin_le 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE 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 Convex Real Real.semiring Real.partialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	RingHomIsometric.ids lipschitzOnWith_iff_norm_sub_le norm_image_sub_le_of_norm_hasFDerivWithin_le
norm_image_sub_le_of_norm_derivWithin_le 📖	mathematical	DifferentiableOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm NormedAddCommGroup.toNorm derivWithin Convex Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Set Set.instMembership	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul NormedField.toNorm	—	norm_image_sub_le_of_norm_hasDerivWithin_le DifferentiableWithinAt.hasDerivWithinAt
norm_image_sub_le_of_norm_deriv_le 📖	mathematical	DifferentiableAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm NormedAddCommGroup.toNorm deriv Convex Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Set Set.instMembership	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul NormedField.toNorm	—	norm_image_sub_le_of_norm_hasDerivWithin_le HasDerivAt.hasDerivWithinAt DifferentiableAt.hasDerivAt
norm_image_sub_le_of_norm_fderivWithin_le 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm fderivWithin Convex Real.semiring 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 Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul	—	norm_image_sub_le_of_norm_hasFDerivWithin_le DifferentiableWithinAt.hasFDerivWithinAt
norm_image_sub_le_of_norm_fderivWithin_le' 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin Convex Real.semiring Real.partialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap.funLike Real.instMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup norm_image_sub_le_of_norm_hasFDerivWithin_le' DifferentiableWithinAt.hasFDerivWithinAt
norm_image_sub_le_of_norm_fderiv_le 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm fderiv Convex Real.semiring 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 Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul	—	norm_image_sub_le_of_norm_hasFDerivWithin_le HasFDerivAt.hasFDerivWithinAt DifferentiableAt.hasFDerivAt
norm_image_sub_le_of_norm_fderiv_le' 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv Convex Real.semiring Real.partialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap.funLike Real.instMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup norm_image_sub_le_of_norm_hasFDerivWithin_le' HasFDerivAt.hasFDerivWithinAt DifferentiableAt.hasFDerivAt
norm_image_sub_le_of_norm_hasDerivWithin_le 📖	mathematical	HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Convex Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Algebra.toSMul Semifield.toCommSemiring Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Set Set.instMembership	SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul NormedField.toNorm	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul norm_image_sub_le_of_norm_hasFDerivWithin_le instIsRCLikeNormedField HasDerivWithinAt.hasFDerivWithinAt le_trans ContinuousLinearMap.norm_toSpanSingleton
norm_image_sub_le_of_norm_hasFDerivWithin_le 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 Convex Real.semiring Real.partialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul	—	mapsTo_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.congr_simp map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass LinearMap.IsScalarTower.compatibleSMul Real.isScalarTower TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivWithinAt.comp_hasDerivWithinAt HasFDerivWithinAt.restrictScalars AffineMap.hasDerivWithinAt_lineMap ContinuousLinearMap.le_of_opNorm_le RingHomIsometric.ids Set.Ico_subset_Icc_self AffineMap.lineMap_apply_one AffineMap.lineMap_apply_zero norm_image_sub_le_of_norm_deriv_le_segment_01'
norm_image_sub_le_of_norm_hasFDerivWithin_le' 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup Convex Real.semiring Real.partialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField Set Set.instMembership	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap.funLike Real.instMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivWithinAt.sub ContinuousLinearMap.hasFDerivWithinAt map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg norm_image_sub_le_of_norm_hasFDerivWithin_le

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_of_deriv_eq 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsPreconnected DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn deriv Set Set.instMembership	—	—	eqOn_of_fderiv_eq instIsRCLikeNormedField ContinuousLinearMap.ext_ring
eqOn_of_fderiv_eq 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsPreconnected DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField fderiv Set Set.instMembership	Set.EqOn	—	exists_eq_add_of_fderiv_eq add_zero left_eq_add AddLeftCancelSemigroup.toIsLeftCancelAdd
exists_eq_add_of_deriv_eq 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsPreconnected DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn deriv	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	exists_eq_add_of_fderiv_eq instIsRCLikeNormedField IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.toSpanSingleton.congr_simp
exists_eq_add_of_fderiv_eq 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsPreconnected DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField Set.EqOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv SeminormedAddCommGroup.toAddCommGroup	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	exists_is_const_of_fderiv_eq_zero DifferentiableOn.sub SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv_fun_sub DifferentiableOn.differentiableAt mem_nhds RingHomIsometric.ids sub_self Pi.zero_apply
exists_is_const_of_deriv_eq_zero 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsPreconnected DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn deriv Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	exists_is_const_of_fderiv_eq_zero instIsRCLikeNormedField ContinuousLinearMap.ext_ring IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.toSpanSingleton.congr_simp ContinuousLinearMap.toSpanSingleton_zero
exists_is_const_of_fderiv_eq_zero 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsPreconnected DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField Set.EqOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv Pi.instZero ContinuousLinearMap.zero	—	—	Set.eq_empty_or_nonempty instIsEmptyFalse isOpen_inter_preimage_of_fderiv_eq_zero ContinuousOn.comp_continuous DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuous_subtype_val IsClosed.preimage isClosed_singleton T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
isOpen_inter_preimage_of_deriv_eq_zero 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn deriv Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set Set.instInter Set.preimage	—	isOpen_inter_preimage_of_fderiv_eq_zero instIsRCLikeNormedField ContinuousLinearMap.ext_ring IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.toSpanSingleton.congr_simp ContinuousLinearMap.toSpanSingleton_zero
isOpen_inter_preimage_of_fderiv_eq_zero 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField Set.EqOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv Pi.instZero ContinuousLinearMap.zero	Set Set.instInter Set.preimage	—	Metric.isOpen_iff Set.subset_inter Convex.is_const_of_fderivWithin_eq_zero convex_ball DifferentiableOn.mono fderivWithin_of_isOpen Metric.isOpen_ball Metric.mem_ball_self
is_const_of_deriv_eq_zero 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsPreconnected DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn deriv Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Set.instMembership	—	—	is_const_of_fderiv_eq_zero instIsRCLikeNormedField ContinuousLinearMap.ext_ring IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.toSpanSingleton.congr_simp ContinuousLinearMap.toSpanSingleton_zero
is_const_of_fderiv_eq_zero 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsPreconnected DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField Set.EqOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv Pi.instZero ContinuousLinearMap.zero Set Set.instMembership	—	—	exists_is_const_of_fderiv_eq_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constant_of_derivWithin_zero 📖	—	DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Icc Real.instPreorder derivWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Set.instMembership	—	—	MulZeroClass.zero_mul norm_image_sub_le_of_norm_deriv_le_segment
constant_of_has_deriv_right_zero 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul norm_image_sub_le_of_norm_deriv_right_le_segment Eq.le norm_zero MulZeroClass.zero_mul
eq_of_derivWithin_eq 📖	—	DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Icc Real.instPreorder Set.EqOn derivWithin Set.Ico Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.mono_of_mem_nhdsWithin DifferentiableWithinAt.hasDerivWithinAt Set.mem_Icc_of_Ico Icc_mem_nhdsGE_of_mem instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid eq_of_has_deriv_right_eq DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
eq_of_fderiv_eq 📖	—	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace fderiv	—	—	Convex.eqOn_of_fderivWithin_eq convex_univ Differentiable.differentiableOn uniqueDiffOn_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul fderivWithin_univ Set.mem_univ
eq_of_has_deriv_right_eq 📖	—	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instPreorder ContinuousOn Set.Icc Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul sub_eq_zero constant_of_has_deriv_right_zero ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup HasDerivWithinAt.congr_simp sub_self HasDerivWithinAt.sub
hasStrictDerivAt_of_hasDerivAt_of_continuousAt 📖	mathematical	Filter.Eventually HasDerivAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul nhds ContinuousAt	HasStrictDerivAt	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt Filter.Eventually.mono HasDerivAt.hasFDerivAt ContinuousAt.comp SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.topologicalAddGroup RingHomIsometric.ids Algebra.to_smulCommClass Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul Continuous.continuousAt ContinuousLinearMap.continuous
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt 📖	mathematical	Filter.Eventually HasFDerivAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds ContinuousAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup	HasStrictFDerivAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup hasStrictFDerivAt_iff_isLittleO Asymptotics.isLittleO_iff Metric.eventually_nhds_iff_ball RingHomIsometric.ids Metric.mem_nhds_iff Filter.inter_mem Metric.ball_mem_nhds dist_eq_norm le_of_lt Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le' instIsRCLikeNormedField HasFDerivAt.hasFDerivWithinAt convex_ball Set.prodMk_mem_set_prod_eq ball_prod_same
image_le_of_deriv_right_le_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder 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 Set.Ici Real.instLE Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_le_deriv_boundary HasDerivWithinAt.liminf_right_slope_le lt_of_le_of_lt
image_le_of_deriv_right_lt_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder 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 Set.Ici Real.instLE HasDerivAt Real.instLT Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_deriv_right_lt_deriv_boundary' ContinuousAt.continuousWithinAt HasDerivAt.continuousAt HasDerivAt.hasDerivWithinAt
image_le_of_deriv_right_lt_deriv_boundary' 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder 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 Set.Ici Real.instLE Real.instLT Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_lt_deriv_boundary' HasDerivWithinAt.liminf_right_slope_le
image_le_of_liminf_slope_right_le_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Real.instLE 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 Set.Ici Filter.Frequently Real.instLT slope Real.instField NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor nhdsWithin Set.Ioi Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_lt_deriv_boundary' sub_self MulZeroClass.mul_zero add_zero ContinuousOn.add IsTopologicalSemiring.toContinuousAdd ContinuousOn.mul continuousOn_const ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuousOn_id HasDerivWithinAt.add HasDerivWithinAt.const_mul HasDerivWithinAt.sub_const hasDerivWithinAt_id mul_one lt_add_iff_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le ContinuousWithinAt.fun_add continuousWithinAt_const ContinuousAt.continuousWithinAt ContinuousAt.fun_mul continuousAt_id' continuousAt_const MulZeroClass.zero_mul ContinuousWithinAt.closure_le HasSolidNorm.orderClosedTopology instHasSolidNormReal closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial
image_le_of_liminf_slope_right_lt_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Filter.Frequently Real.instLT slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor nhdsWithin Set.Ioi Real.instLE HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField 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	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_lt_deriv_boundary' ContinuousAt.continuousWithinAt HasDerivAt.continuousAt HasDerivAt.hasDerivWithinAt
image_le_of_liminf_slope_right_lt_deriv_boundary' 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Filter.Frequently Real.instLT slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor nhdsWithin Set.Ioi Real.instLE HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField 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.Ici Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.prodMk Set.inter_comm ContinuousOn.preimage_isClosed_of_isClosed isClosed_Icc HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid OrderClosedTopology.isClosed_le' IsClosed.Icc_subset_of_forall_exists_gt instOrderTopologyReal LE.le.lt_or_eq Filter.nonempty_of_mem nhdsGT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.inter_mem Set.Ico_subset_Icc_self IsOpen.mem_nhds isOpen_lt continuous_fst continuous_snd nhdsWithin_le_of_mem Icc_mem_nhdsGT_of_mem instClosedIciTopology Filter.Eventually.mono le_of_lt Ioc_mem_nhdsGT exists_between IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivWithinAt_iff_tendsto_slope' lt_irrefl HasDerivWithinAt.Ioi_of_Ici Ioi_mem_nhds instClosedIicTopology Filter.Frequently.exists Filter.Frequently.and_eventually Filter.Eventually.and LT.lt.le LT.lt.trans sub_le_sub_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd slope_def_field
image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder Filter.Frequently Real.instLT slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Norm.norm NormedAddCommGroup.toNorm nhdsWithin Set.Ioi Real.instLE HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField 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.Ici Set Set.instMembership	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_lt_deriv_boundary' Continuous.comp_continuousOn continuous_norm
image_norm_le_of_norm_deriv_right_le_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instLE Norm.norm NormedAddCommGroup.toNorm HasDerivAt Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_norm_le_of_norm_deriv_right_le_deriv_boundary' ContinuousAt.continuousWithinAt HasDerivAt.continuousAt HasDerivAt.hasDerivWithinAt
image_norm_le_of_norm_deriv_right_le_deriv_boundary' 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_le_of_liminf_slope_right_le_deriv_boundary Continuous.comp_continuousOn continuous_norm HasDerivWithinAt.liminf_right_slope_norm_le LE.le.trans_lt
image_norm_le_of_norm_deriv_right_lt_deriv_boundary 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instLE Norm.norm NormedAddCommGroup.toNorm HasDerivAt Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instLT Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_norm_le_of_norm_deriv_right_lt_deriv_boundary' ContinuousAt.continuousWithinAt HasDerivAt.continuousAt HasDerivAt.hasDerivWithinAt
image_norm_le_of_norm_deriv_right_lt_deriv_boundary' 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instLT Set Set.instMembership	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary HasDerivWithinAt.liminf_right_slope_norm_le
isLocallyConstant_of_fderiv_eq_zero 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace fderiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	IsLocallyConstant	—	Set.univ_inter IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero isOpen_univ Differentiable.differentiableOn
is_const_of_deriv_eq_zero 📖	—	Differentiable DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace deriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	is_const_of_fderiv_eq_zero instIsRCLikeNormedField ContinuousLinearMap.ext_ring IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.toSpanSingleton.congr_simp ContinuousLinearMap.toSpanSingleton_zero
is_const_of_fderiv_eq_zero 📖	—	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace fderiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	—	Convex.is_const_of_fderivWithin_eq_zero convex_univ Differentiable.differentiableOn fderivWithin_univ
lipschitzWith_of_nnnorm_deriv_le 📖	mathematical	Differentiable DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup deriv	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace NormedAddCommGroup.toMetricSpace	—	lipschitzOnWith_univ Convex.lipschitzOnWith_of_nnnorm_deriv_le convex_univ
lipschitzWith_of_nnnorm_fderiv_le 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing fderiv	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	RingHomIsometric.ids lipschitzOnWith_univ Convex.lipschitzOnWith_of_nnnorm_fderiv_le convex_univ
norm_image_sub_le_of_norm_deriv_le_segment 📖	mathematical	DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Icc Real.instPreorder Real.instLE Norm.norm NormedAddCommGroup.toNorm derivWithin Set Set.instMembership	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul Real.instSub	—	norm_image_sub_le_of_norm_deriv_le_segment' DifferentiableWithinAt.hasDerivWithinAt
norm_image_sub_le_of_norm_deriv_le_segment' 📖	mathematical	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Icc Real.instPreorder Real.instLE Norm.norm NormedAddCommGroup.toNorm Set Set.instMembership	SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul Real.instSub	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul norm_image_sub_le_of_norm_deriv_right_le_segment HasDerivWithinAt.continuousWithinAt HasDerivWithinAt.mono_of_mem_nhdsWithin Set.Ico_subset_Icc_self Icc_mem_nhdsGE_of_mem instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
norm_image_sub_le_of_norm_deriv_le_segment_01 📖	mathematical	DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Icc Real.instPreorder Real.instZero Real.instOne Real.instLE Norm.norm NormedAddCommGroup.toNorm derivWithin	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_zero mul_one norm_image_sub_le_of_norm_deriv_le_segment Set.right_mem_Icc zero_le_one Real.instZeroLEOneClass
norm_image_sub_le_of_norm_deriv_le_segment_01' 📖	mathematical	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Icc Real.instPreorder Real.instOne Real.instLE Norm.norm NormedAddCommGroup.toNorm	SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul sub_zero mul_one norm_image_sub_le_of_norm_deriv_le_segment' Set.right_mem_Icc zero_le_one Real.instZeroLEOneClass
norm_image_sub_le_of_norm_deriv_right_le_segment 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero 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 NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici Real.instLE Norm.norm NormedAddCommGroup.toNorm Set Set.instMembership	SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul Real.instSub	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn_const ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp MulZeroClass.zero_mul sub_zero mul_one zero_add HasDerivAt.mul hasDerivAt_const HasDerivAt.sub hasDerivAt_id image_norm_le_of_norm_deriv_right_le_deriv_boundary sub_self norm_zero MulZeroClass.mul_zero le_refl

---

← Back to Index