proposition: Lemma filtermap_prod_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G} (f1 : T1 -> U1) (f2 : T2 -> U2) : filter_le (filtermap (fun x => (f1 (fst x), f2 (snd x))) (filter_prod F G)) (filter_prod (filtermap f1 F) (filtermap f2 G)).
proof: Proof. intros P [Q1 Q2 H1 H2 H]. unfold filtermap. split with (fun x => Q1 (f1 x)) (fun x => Q2 (f2 x)). now apply: filter_imp H1. now apply: filter_imp H2. intros x1 x2 Qx1 Qx2. now apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub