proposition: Lemma cvg_abse0P f : abse \o f @ F --> 0 <-> f @ F --> 0.
proof: Proof. split; last by move=> /cvg_abse; rewrite abse0. move=> /cvg_ballP f0; apply/cvg_ballP => _/posnumP[e]. have := !! f0 _ (gt0 e); rewrite !near_simpl => absf0; rewrite near_simpl. apply: filterS absf0 => x /=; rewrite /ball/= /ereal_ball !contract0 !sub0r !normrN. have [fx0|fx0] := leP 0 (f x); first by rewrite gee0_abs. by rewrite (lte0_abs fx0) contractN normrN. 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