proposition: Lemma sqrt_continuous : continuous (@Num.sqrt R).
proof: Proof. move=> x; case: (ltrgtP x 0) => [xlt0 | xgt0 | ->]. - apply: (near_cst_continuous 0). by near do rewrite ltr0_sqrtr//; apply: (cvgr_lt x). pose I b : set R := [set` `]0 ^+ 2, b ^+ 2[]. suff main b : 0 <= b -> {in I b, continuous (@Num.sqrt R)}. near +oo_R => M; apply: (main M); rewrite // /I !inE/= in_itv/= expr0n xgt0. by rewrite -ltr_sqrt ?exprn_gt0// sqrtr_sqr gtr0_norm/=. move=> b0; rewrite -continuous_open_subspace; last exact: interval_open. apply: continuous_subspaceW; first exact: subset_itv_oo_cc. apply: (@segment_can_le_continuous _ _ _ (@GRing.exp _^~ _)) => //. by apply: continuous_subspaceT; exact: exprn_continuous. by move=> y y0b; rewrite sqrtr_sqr ger0_norm// (itvP y0b). - rewrite /continuous_at sqrtr0; apply/cvgr0Pnorm_lt => _ /posnumP[e]; near=> y. have [ylt0|yge0] := ltrP y 0; first by rewrite ltr0_sqrtr ?normr0. rewrite ger0_norm ?sqrtr_ge0//; have: `|y| < e%:num ^+ 2 by []. by rewrite -ltr_sqrt// ger0_norm// sqrtr_sqr ger0_norm. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)