proposition: Lemma open_ext : forall D E : T -> Prop, (forall x, D x <-> E x) -> open D -> open E.
proof: Proof. intros D E H OD x Ex. generalize (OD x (proj2 (H x) Ex)). apply filter_imp. intros y. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub