proposition: Lemma closed_filterlim_loc : forall {T} {U : UniformSpace} {F} {FF : ProperFilter' F} (f : T -> U) (D : U -> Prop), forall y, filterlim f F (locally y) -> F (fun x => D (f x)) -> closed D -> D y.
proof: Proof. intros T U F FF f D y Ffy Df CD. apply CD. intros LD. apply filter_not_empty. specialize (Ffy _ LD). unfold filtermap in Ffy. apply: filter_imp (filter_and _ _ Df Ffy). intros x Dfx. now apply Dfx. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub