proposition: Lemma pointwise_uniform_cvg (f : U -> V) (F : set_system (U -> V)) : Filter F -> {uniform, F --> f} -> {ptws, F --> f}.
proof: Proof. move=> FF; rewrite cvg_sup => + i; have isubT : [set i] `<=` setT by move=> ?. move=> /(uniform_subset_cvg _ isubT); rewrite uniform_set1. rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v). apply: cvg_trans => W /=; rewrite nbhs_simpl; exists (@^~ i @^-1` W) => //. by rewrite image_preimage // eqEsubset; split=> // j _; 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