proposition: Lemma is_filter_lim_filtermap {T: UniformSpace} {U : UniformSpace} : forall F x (f : T -> U), filterlim f (locally x) (locally (f x)) -> is_filter_lim F x -> is_filter_lim (filtermap f F) (f x).
proof: Proof. intros F x f Cf Fx P HP. apply Cf in HP. now apply Fx. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub