proposition: Lemma pointwise_precompact_precompact {I} (W : set I) (fW : I -> (X -> Y)) : pointwise_precompact W fW -> precompact ((fW @` W) : set {ptws X -> Y}).
proof: Proof. rewrite precompactE => ptwsPreW. pose K := fun x => closure [set fW i x | i in W]. set R := [set f : {ptws X -> Y} | forall x : X, K x (f x)]. have C : compact R. by apply: tychonoff => x; rewrite -precompactE; move: ptwsPreW; exact. apply: (subclosed_compact _ C); first exact: closed_closure. have WsubR : (fW @` W) `<=` R. move=> f Wf x; rewrite /R /K closure_limit_point; left. by case: Wf => i ? <-; exists i. rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR. exact: hausdorff_product. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed