proposition: Lemma compactU (A B : set X) : compact A -> compact B -> compact (A `|` B).
proof: Proof. rewrite compact_ultra => cptA cptB F UF FAB; rewrite setIUl. have [/cptA[x AFx]|] := in_ultra_setVsetC A UF; first by exists x; left. move=> /(filterI FAB); rewrite setIUl setICr set0U => FBA. have /cptB[x BFx] : F B by apply: filterS FBA; exact: subIsetr. by exists x; right. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed