proposition: Lemma pointwise_cvgE {U : Type} {V : topologicalType} (F : set_system (U -> V)) (A : set U) (f : U -> V) : {ptws, F --> f} = (F --> (f : {ptws U -> V})).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed