proposition: Lemma compact_closedI {T : topologicalType} (A B : set T) : compact A -> closed B -> compact (A `&` B).
proof: Proof. move=> cptA clB F PF FAB; have FA : F A by move: FAB; exact: filterS. (have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed