proposition: Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : {within A, continuous f} -> compact A -> compact (f @` A).
proof: Proof. move=> fcont Aco F FF FfA; set G := filter_from F (fun C => A `&` f @^-1` C). have GF : ProperFilter G. apply: (filter_from_proper (filter_from_filter _ _)). - by exists (f @` A). - by move=> C1 C2 F1 F2; exists (C1 `&` C2); [exact: filterI|move=> ? [? []]]. - by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; exists p. move: Aco; rewrite -[A]setIid => /compact_subspaceIP; rewrite setIid. case /(_ G); first by exists (f @` A) => // ? []. move=> p [Ap clsGp]; exists (f p); split; first exact/imageP. move=> B C FB /fcont p_Cf. have : G (A `&` f @^-1` B) by exists B. by move=> /clsGp /(_ p_Cf) [q [[]]]; exists (f q). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed