proposition: Lemma complete_cauchy_fct : forall (F : ((T -> U) -> Prop) -> Prop), ProperFilter F -> (forall eps : posreal, exists f : T -> U, F (ball f eps)) -> forall eps : posreal, F (ball (lim_fct F) eps).
proof: Proof. move => F FF HFc. set Fr := fun (t : T) (P : U -> Prop) => F (fun g => P (g t)). have FFr : forall t, ProperFilter (Fr t). case: FF => HF FF t. split. - move => P Hp. case: (HF _ Hp) => f Hf. by exists (f t). - split. + by apply FF. + move => P P' Hp Hp'. by apply FF. + move => P P' Hpp'. apply FF. move => f ; by apply Hpp'. assert (HFrc : forall t, forall eps : posreal, exists x : U, Fr t (ball x eps)). move => t eps. case: (HFc eps) => f Hf. exists (f t). move: Hf ; apply FF => g. by []. assert (forall t (eps : posreal), (Fr t) (fun x => ball (lim_fct F t) eps x)). move => t. apply complete_cauchy. apply FFr. exact (HFrc t). move => eps. generalize (proj1 cauchy_distance HFc) => {} HFc. case: (HFc (pos_div_2 eps)) => {HFc} P ; simpl ; case => HP H0. apply filter_imp with (2 := HP). move => g Hg t. move: (fun h => H0 g h Hg) => {} H0. move: (H t (pos_div_2 eps)) ; simpl => {} H. unfold Fr in H ; generalize (filter_and _ _ H HP) => {} H. apply filter_ex in H ; case: H => h H. rewrite (double_var eps). apply ball_triangle with (h t). by apply H. apply ball_sym, H0. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub