proposition: Lemma open_and : forall D E : T -> Prop, open D -> open E -> open (fun x => D x /\ E x).
proof: Proof. intros D E OD OE x [Dx Ex]. apply filter_and. now apply OD. now apply OE. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub