proposition: Lemma filterlim_comp_2 : forall {T U V W F G H I} {FF : Filter F}, forall (f : T -> U) (g : T -> V) (h : U -> V -> W), filterlim f F G -> filterlim g F H -> filterlim (fun x => h (fst x) (snd x)) (filter_prod G H) I -> filterlim (fun x => h (f x) (g x)) F I.
proof: Proof. intros T U V W F G H I FF f g h Cf Cg Ch. change (fun x => h (f x) (g x)) with (fun x => h (fst (f x, g x)) (snd (f x, g x))). apply: filterlim_comp Ch. now apply filterlim_pair. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub