proposition: Lemma pointwise_cvg_compact_family F (f : U -> V) : Filter F -> {family compact, F --> f} -> {ptws, F --> f}.
proof: Proof. move=> PF; rewrite pointwise_cvg_family_singleton; apply: family_cvg_subset. by move=> A [x _ <-]; exact: compact_set1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed