proposition: Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : compact P -> compact Q -> compact (P `*` Q).
proof: Proof. rewrite !compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. have := cptP I F (fun i u => forall q, Q q -> Pr i (u, q)) Ff. set R := (R in (R -> _) -> _); suff R' : R. by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv. case: (cvfPQ (x, v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. exists (N2, N1`*`G); first by split => //; exists (N1, G). case=> a [b i] /= [N2a [N1b]] Gi. by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed