proposition: Lemma filterlimi_locally_cauchy : forall {F} {FF : ProperFilter F} (f : T -> U -> Prop), F (fun x => (exists y, f x y) /\ (forall y1 y2, f x y1 -> f x y2 -> y1 = y2)) -> ((forall eps : posreal, exists P, F P /\ forall u v : T, P u -> P v -> forall u' v': U, f u u' -> f v v' -> ball u' eps v') <-> exists y, filterlimi f F (locally y)).
proof: Proof. intros F FF f Hf. assert (FF': ProperFilter (filtermapi f F)). apply filtermapi_proper_filter. exact: filter_imp Hf. exact FF. split. - intros H. exists (lim (filtermapi f F)). intros P [eps HP]. refine (_ (complete_cauchy (filtermapi f F) _ _ eps)). + now apply filter_imp. + clear eps P HP. intros eps. case: (H eps) => {H} [P [FP H]]. assert (FfP := filter_and _ _ Hf FP). destruct (filter_ex _ FfP) as [x [[[fx Hfx] _] Px]]. exists fx. unfold filtermapi. apply: filter_imp FfP. intros x' [[[fx' Hfx'] _] Px']. exists fx'. apply (conj Hfx'). exact: H Hfx Hfx'. - intros [y Hy] eps. exists (fun x => forall fx, f x fx -> ball y (pos_div_2 eps) fx). split. assert (Hb: locally y (ball y (pos_div_2 eps))). now exists (pos_div_2 eps). assert (H := filter_and _ _ Hf (Hy _ Hb)). apply: filter_imp H. intros x [[_ H] [fx2 [Hfx2 H']]] fx Hfx. now rewrite <- (H fx2). intros u v Hu Hv fu fv Hfu Hfv. rewrite (double_var eps). apply ball_triangle with y. apply ball_sym. now apply Hu. now apply Hv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub