proposition: Lemma filterlimi_lim_ext_loc : forall {T U F G} {FF : Filter F} (f : T -> U) (g : T -> U -> Prop), F (fun x => g x (f x)) -> filterlim f F G -> filterlimi g F G.
proof: Proof. intros T U F G FF f g HF Hf P HP. generalize (filter_and (fun x => g x (f x)) _ HF (Hf P HP)). unfold filtermapi. apply: filter_imp. intros x [H1 H2]. now exists (f x). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub