proposition: Lemma pointwise_cvgP F (f: U -> V): Filter F -> {ptws, F --> f} <-> forall (t : U), (fun g => g t) @ F --> f t.
proof: Proof. move=> Ff; rewrite pointwise_cvg_family_singleton; split. move/fam_cvgP => + t A At => /(_ [set t]); rewrite uniform_set1; apply => //. by exists t. by move=> pf; apply/fam_cvgP => ? [t _ <-]; rewrite uniform_set1; exact: pf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed