proposition: Lemma llip `{!ExtMetricSpaceClass X} (f : X -> Y) `{IsLocallyLipschitz f L} (r e : Q) (a x y : X) : ball r a x -> ball r a y -> ball e x y -> ball (L a r * e) (f x) (f y).
proof: Proof. intros A1 A2 A3. change (f x) with (restrict f a r (exist _ x A1)). change (f y) with (restrict f a r (exist _ y A2)). assert (0 ≤ r) by now apply (radius_nonneg a x). apply (lip_prf _ (L a r)); trivial. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.theory.setoids MathClasses.theory.products MathClasses.implementations.stdlib_rationals MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum