proposition: Lemma open_comp : forall {T U : UniformSpace} (f : T -> U) (D : U -> Prop), (forall x, D (f x) -> filterlim f (locally x) (locally (f x))) -> open D -> open (fun x : T => D (f x)).
proof: Proof. intros T U f D Cf OD x Dfx. apply Cf. exact Dfx. now apply OD. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub