proposition: Lemma SFL_continuity_pt : forall (fn:nat -> R -> R) (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) (r:posreal), CVN_r fn r -> (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) -> forall y:R, Boule 0 r y -> continuity_pt (SFL fn cv) y.
proof: Proof. intros; eapply CVU_continuity. - apply CVN_CVU. apply X. - intros; unfold SP; apply continuity_pt_finite_SF. intros; apply H. apply H1. - apply H0. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra