proposition: Lemma lipschitz_locally (R : numFieldType) (V W : normedModType R) (A : set V) (f : V -> W) : [lipschitz f x | x in A] -> [locally [lipschitz f x | x in A]].
proof: Proof. by move=> + x Ax; apply: sub_lipschitz; apply: within_nbhsW. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule