proposition: Lemma eqolimP (F : filter_on T) (f : T -> V) (l : V) : f @ F --> l <-> f = cst l +o_F (cst (1 : K^o)).
proof: Proof. split=> fFl. apply/eqaddoP => _/posnumP[eps]; near do rewrite /cst ltW//. by apply: cvgr_distC_lt; rewrite // mulr_gt0 // normr1. apply/cvgrPdist_lt=> _/posnumP[eps]. have lt_eps x : x <= (eps%:num / 2%:R) * `|1 : K^o|%real -> x < eps%:num. rewrite normr1 mulr1 => /le_lt_trans; apply. by rewrite ltr_pdivrMr // ltr_pMr // ltr1n. near=> x do rewrite [X in X x]fFl opprD addNKr normrN lt_eps //. by apply: littleoP; rewrite divr_gt0. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule