proposition: Lemma filterlim_pair : forall {T U V F G H} {FF : Filter F}, forall (f : T -> U) (g : T -> V), filterlim f F G -> filterlim g F H -> filterlim (fun x => (f x, g x)) F (filter_prod G H).
proof: Proof. intros T U V F G H FF f g Cf Cg P [A B GA HB HP]. unfold filtermap. apply (filter_imp (fun x => A (f x) /\ B (g x))). intros x [Af Bg]. now apply HP. apply filter_and. now apply Cf. now apply Cg. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub