proposition: Lemma filterlimi_ext : forall {T U F G} {FF : Filter F} (f g : T -> U -> Prop), (forall x 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. apply filterlimi_ext_loc. now apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub