proposition: Lemma open_or : 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]. generalize (OD x Dx). apply filter_imp. intros y Dy. now left. generalize (OE x Ex). apply filter_imp. intros y Ey. now right. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub