proposition: Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) : {near F, f =1 g} -> g @ F `=>` f @ F.
proof: Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed