proposition: Lemma closed_filterlim : forall {T} {U : UniformSpace} {F} {FF : ProperFilter' F} (f : T -> U) (D : U -> Prop), forall y, filterlim f F (locally y) -> (forall x, D (f x)) -> closed D -> D y.
proof: Proof. intros T U F FF f D y Ffy Df. apply: closed_filterlim_loc Ffy _. now apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub