proposition: Lemma precompact_pointwise_precompact (W : set {family compact, X -> Y}) : precompact W -> pointwise_precompact W id.
proof: Proof. move=> + x; rewrite ?precompactE => pcptW. have : compact (proj x @` (closure W)). apply: continuous_compact => //; apply: continuous_subspaceT=> g. move=> E nbhsE; have := (@proj_continuous _ _ x g E nbhsE). exact: (@pointwise_cvg_compact_family _ _ (nbhs g)). move=> /[dup]/(compact_closed hsdf)/closure_id -> /subclosed_compact. apply; first exact: closed_closure. by apply/closure_subset/image_subset; exact: (@subset_closure _ W). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed