proposition: Lemma continuous_shift (f : U -> V) u : {for u, continuous f} = {for 0, continuous (f \o shift u)}.
proof: Proof. by rewrite [in RHS]forE /continuous_at/= add0r cvg_comp_shift 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