proposition: Lemma continuous_withinNshiftx (f : U -> V) u : f \o shift u @ 0^' --> f u <-> {for u, continuous f}.
proof: Proof. rewrite continuous_shift; split=> [cfu|]. by apply/(continuous_withinNx _ _).2/(cvg_trans cfu); rewrite /= add0r. by move/(continuous_withinNx _ _).1/cvg_trans; apply; rewrite /= add0r. 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