proposition: Lemma filterdiff_comp_2 {F : (T -> Prop) -> Prop} {FF : Filter F} : forall (f : T -> U) (g : T -> V) (h : U -> V -> W) (lf : T -> U) (lg : T -> V) (lh : U -> V -> W), filterdiff f F lf -> filterdiff g F lg -> filterdiff (fun t => h (fst t) (snd t)) (filtermap (fun t => (f t,g t)) F) (fun t => lh (fst t) (snd t)) -> filterdiff (fun y : T => h (f y) (g y)) F (fun y : T => lh (lf y) (lg y)).
proof: Proof. intros f g h lf lg lh [Hf Df] [Hg Dg] Dh. apply (filterdiff_comp (fun t => (f t, g t)) _ (fun t => (lf t, lg t)) _) in Dh. by []. split. by apply is_linear_prod. intros x Hx eps. assert (0 < eps / sqrt 2). apply Rdiv_lt_0_compat. by apply eps. apply Rlt_sqrt2_0. generalize (filter_and _ _ (Df x Hx (mkposreal _ H)) (Dg x Hx (mkposreal _ H))). simpl pos. apply filter_imp ; intros y [Hnf Hng]. eapply Rle_trans. apply norm_prod. simpl fst ; simpl snd. eapply Rle_trans. apply Rmult_le_compat_l. by apply sqrt_pos. apply Rmax_case. apply Hnf. apply Hng. apply Req_le ; field. apply Rgt_not_eq, Rlt_sqrt2_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv