proposition: Lemma SFL_continuity : forall (fn:nat -> R -> R) (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }), CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).
proof: Proof. intros; unfold continuity; intro. cut (0 < Rabs x + 1); [ intro | apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ] ]. cut (Boule 0 (mkposreal _ H0) x). - intro; eapply SFL_continuity_pt with (mkposreal _ H0). + apply X. + intros; apply (H n y). + apply H1. - unfold Boule; simpl; rewrite Rminus_0_r; pattern (Rabs x) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra