proposition: Lemma filterlim_locally_closely : forall {F} {FF : ProperFilter F} (f : T -> U), filterlim (fun x => (f (fst x), f (snd x))) (filter_prod F F) closely <-> exists y, filterlim f F (locally y).
proof: Proof. intros F FF f. split. - intros H. exists (lim (filtermap f F)). intros P [eps HP]. refine (_ (complete_cauchy (filtermap f F) _ _ eps)). + now apply filter_imp. + apply cauchy_distance'. apply filter_le_trans with (2 := H). apply prod_filtermap_le. - intros [y Hy] P [eps HP]. split with (fun x => ball y (pos_div_2 eps) (f x)) (fun x => ball y (pos_div_2 eps) (f x)). apply Hy, locally_ball. apply Hy, locally_ball. intros u v Hu Hv. apply HP. rewrite (double_var eps). apply ball_triangle with (2 := Hv). now apply ball_sym. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub