proposition: Lemma continuity_pt_nbhs (f : R -> R) x : continuity_pt f x <-> forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num).
proof: Proof. split=> [fcont e|fcont _/RltP/posnumP[e]]; last first. have [_/posnumP[d] xd_fxe] := fcont e. exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num]. by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC. have /RltP egt0 := [gt0 of e%:num]. have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0. exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney]. by rewrite subrr normr0. apply/RltP/dx_fxe; split; first by split=> //; apply/eqP. by have /RltP := xyd; rewrite distrC. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures) mathcomp(boolp classical_sets) reals signed topology