proposition: Lemma filterdiff_comp'_2 : forall (f : T -> U) (g : T -> V) (h : U -> V -> W) x (lf : T -> U) (lg : T -> V) (lh : U -> V -> W), filterdiff f (locally x) lf -> filterdiff g (locally x) lg -> filterdiff (fun t => h (fst t) (snd t)) (locally (f x,g x)) (fun t => lh (fst t) (snd t)) -> filterdiff (fun y : T => h (f y) (g y)) (locally x) (fun y : T => lh (lf y) (lg y)).
proof: Proof. intros. apply filterdiff_comp_2. by []. by []. apply filterdiff_locally with (f x, g x). apply (is_filter_lim_filtermap _ _ (fun t : T => (f t, g t))) => //. apply (filterdiff_continuous (fun t : T => (f t, g t))) => //. apply ex_filterdiff_comp_2. by exists lf. by exists lg. apply ex_filterdiff_linear. apply is_linear_prod. apply is_linear_fst. by apply is_linear_snd. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv