proposition: Lemma CVU_continuity : forall (fn:nat -> R -> R) (f:R -> R) (x:R) (r:posreal), CVU fn f x r -> (forall (n:nat) (y:R), Boule x r y -> continuity_pt (fn n) y) -> forall y:R, Boule x r y -> continuity_pt f y.
proof: Proof. intros; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros. unfold CVU in H. cut (0 < eps / 3); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H _ H3); intros N0 H4. assert (H5 := H0 N0 y H1). assert (exists del : posreal, (forall h:R, Rabs h < del -> Boule x r (y + h))). { assert (0 < r - Rabs (x - y)). { unfold Boule in H1; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr; apply Rplus_lt_reg_l with (Rabs (y - x)). rewrite Rplus_0_r; replace (Rabs (y - x) + (r - Rabs (y - x))) with (pos r); [ apply H1 | ring ]. } exists (mkposreal _ H6). simpl; intros. unfold Boule; replace (y + h - x) with (h + (y - x)); [ idtac | ring ]; apply Rle_lt_trans with (Rabs h + Rabs (y - x)). { apply Rabs_triang. } apply Rplus_lt_reg_l with (- Rabs (x - y)). rewrite <- (Rabs_Ropp (y - x)); rewrite Ropp_minus_distr. replace (- Rabs (x - y) + r) with (r - Rabs (x - y)) by ring. replace (- Rabs (x - y) + (Rabs h + Rabs (x - y))) with (Rabs h) by ring. apply H7. } elim H6; intros del1 H7. unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5; unfold limit_in in H5; simpl in H5; unfold Rdist in H5. elim (H5 _ H3); intros del2 H8. set (del := Rmin del1 del2). exists del; intros. split. { unfold del; unfold Rmin; case (Rle_dec del1 del2); intro. - apply (cond_pos del1). - elim H8; intros; assumption. } intros; apply Rle_lt_trans with (Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - f y)). { replace (f x0 - f y) with (f x0 - fn N0 x0 + (fn N0 x0 - f y)); [ apply Rabs_triang | ring ]. } apply Rle_lt_trans with (Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - fn N0 y) + Rabs (fn N0 y - f y)). { rewrite Rplus_assoc; apply Rplus_le_compat_l. replace (fn N0 x0 - f y) with (fn N0 x0 - fn N0 y + (fn N0 y - f y)); [ apply Rabs_triang | ring ]. } replace eps with (eps / 3 + eps / 3 + eps / 3) by field. repeat apply Rplus_lt_compat. - apply H4. + apply le_n. + replace x0 with (y + (x0 - y)); [ idtac | ring ]; apply H7. elim H9; intros. apply Rlt_le_trans with del. * assumption. * unfold del; apply Rmin_l. - elim H8; intros. apply H11. split. + elim H9; intros; assumption. + elim H9; intros; apply Rlt_le_trans with del. * assumption. * unfold del; apply Rmin_r. - rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H4. + apply le_n. + assumption. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra