proposition: Lemma klipschitz_locally (R : numFieldType) (V W : normedModType R) (k : R) (f : V -> W) (A : set V) : k.-lipschitz_A f -> [locally k.-lipschitz_A f].
proof: Proof. by move=> + x Ax; apply: sub_klipschitz; 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