proposition: Lemma cvgr_norm_lt {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : f @ F --> y -> forall u, `|y| < u -> \forall t \near F, `|f t| < u.
proof: Proof. move=> Fy z zy; near (0:R)^'+ => k; near=> x; have : `|f x - y| < k. by near: x; apply: cvgr_distC_lt => //; near: k; apply: nbhs_right_gt. move=> /(le_lt_trans (ler_dist_dist _ _)) /real_ltr_normlW. rewrite realB// ltrBlDl => /(_ _)/lt_le_trans; apply => //. by rewrite -lerBrDl; near: k; apply: nbhs_right_le; rewrite subr_gt0. Unshelve. all: by end_near. 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