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