proposition: Lemma locally_open : forall (D E : T -> Prop), open D -> (forall x : T, D x -> E x) -> forall x : T, D x -> locally x E.
proof: Proof. intros D E OD H x Dx. apply filter_imp with (1 := H). now apply OD. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub