proposition: Lemma filterlimi_ext_loc : forall {T U F G} {FF : Filter F} (f g : T -> U -> Prop), F (fun x => forall y, f x y <-> g x y) -> filterlimi f F G -> filterlimi g F G.
proof: Proof. intros T U F G FF f g Efg Lf P GP. specialize (Lf P GP). generalize (filter_and _ _ Efg Lf). unfold filtermapi. apply filter_imp. intros x [H [y [Hy1 Hy2]]]. exists y. apply: conj Hy2. now apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub