proposition: Lemma pointwise_cvg_family_singleton F (f: U -> V): Filter F -> {ptws, F --> f} = {family @singletons U, F --> f}.
proof: Proof. move=> FF; apply/propext. rewrite (@fam_cvgP _ _ singletons). rewrite cvg_sup; split. move=> + A [x _ <-] => /(_ x); rewrite uniform_set1. rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v). apply: cvg_trans => W /=; rewrite ?nbhs_simpl /fmap /= => [[W' + <-]]. by apply: filterS => g W'g /=; exists g. move=> + i; have /[swap] /[apply] : singletons [set i] by exists i. rewrite uniform_set1. rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v). move=> + W //=; rewrite ?nbhs_simpl => Q => /Q Q'; exists (@^~ i @^-1` W) => //. by rewrite eqEsubset; split => [j [? + <-//]|j Wj]; exists (fun _ => j). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed