proposition: Lemma ex_filterdiff_comp_2 {F : (T -> Prop) -> Prop} {FF : Filter F} : forall (f : T -> U) (g : T -> V) (h : U -> V -> W), ex_filterdiff f F -> ex_filterdiff g F -> ex_filterdiff (fun t => h (fst t) (snd t)) (filtermap (fun t => (f t,g t)) F) -> ex_filterdiff (fun y : T => h (f y) (g y)) F.
proof: Proof. intros f g h [lf Df] [lg Dg] [lh Dh]. set lh' := fun x y => lh (x,y). eexists ; eapply (filterdiff_comp_2 _ _ _ _ _ lh') ; try eassumption. eapply filterdiff_ext_lin. by apply Dh. by case. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv