proposition: Lemma pointwise_precompact_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} : fW @` W `<=` fV @` V -> pointwise_precompact V fV -> pointwise_precompact W fW.
proof: Proof. move=> WsubV + x => /(_ x) pcptV; apply: precompact_subset pcptV => y [i Wi <-]. by case: (WsubV (fW i)); [exists i | move=> j Vj <-; exists 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