proposition: Fact dpair (U V' W' : normedModType R) (f : U -> V') (g : U -> W') x : differentiable f x -> differentiable g x -> continuous (fun y => ('d f x y, 'd g x y)) /\ (fun y => (f y, g y)) \o shift x = cst (f x, g x) + (fun y => ('d f x y, 'd g x y)) +o_ (0 : U) id.
proof: Proof. move=> df dg; split=> [?|]; first by apply: cvg_pair; apply: diff_continuous. apply/eqaddoE; rewrite funeqE => y /=. rewrite ![_ (_ + x)]diff_locallyx//. have -> : forall h e, (f x + 'd f x y + [o_ (0 : U) id of h] y, g x + 'd g x y + [o_ (0 : U) id of e] y) = (f x, g x) + ('d f x y, 'd g x y) + ([o_ (0 : U) id of h] y, [o_ (0 : U) id of e] y) by []. by congr (_ + _); rewrite -[LHS]/((fun y => (_ y, _ y)) y) eqo_pair. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms