proposition: Lemma cvg_near_const (T U : Type) (f : T -> U) (F : set_system T) (G : set_system U) : Filter F -> ProperFilter G -> (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G.
proof: Proof. move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G). by apply: filter_app fFG; near do apply: filterS => x /= ->. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed