proposition: Lemma sqrt_continuity_pt_R1 : continuity_pt sqrt 1.
proof: Proof. unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. set (alpha := Rmin eps 1). exists alpha; intros. split. - unfold alpha; unfold Rmin; case (Rle_dec eps 1); intro. + assumption. + apply Rlt_0_1. - intros; elim H0; intros. rewrite sqrt_1; replace x with (1 + (x - 1)); [ idtac | ring ]; apply Rle_lt_trans with (Rabs (x - 1)). + apply sqrt_var_maj. apply Rle_trans with alpha. * left; apply H2. * unfold alpha; apply Rmin_r. + apply Rlt_le_trans with alpha; [ apply H2 | unfold alpha; apply Rmin_l ]. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra