proposition: Lemma continuity_pt_cvg (f : R -> R) (x : R) : Ranalysis1.continuity_pt f x <-> {for x, continuous f}.
proof: Proof. eapply iff_trans; first exact: continuity_pt_nbhs. apply iff_sym. have FF : Filter (f @ x). by typeclasses eauto. case: (@fcvg_ballP _ _ (f @ x) FF (f x)) => {FF}H1 H2. split => [{H2} - /H1 {}H1 eps|{H1} H]. - have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num. exists x0%:num => //= Hx0' /Hx0 /=. by rewrite /= distrC; apply. - apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0]. exists x0%:num => //= y /Hx0 /= {}Hx0. by rewrite /ball /= distrC. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule