proposition: Lemma eqolim (F : filter_on T) (f : T -> V) (l : V) e : f = cst l + [o_F (cst (1 : K^o)) of e] -> f @ F --> l.
proof: Proof. by move=> /eqaddoE /eqolimP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule