proposition: Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) : (\forall x \near F, f x = l) -> lim (f @ F) = l.
proof: Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed