proposition: Lemma subclosed_compact (A B : set T) : closed A -> compact B -> A `<=` B -> compact A.
proof: Proof. move=> Acl Bco sAB F Fproper FA. have [|p [Bp Fp]] := Bco F; first exact: filterS FA. by exists p; split=> //; apply: Acl=> C Cp; apply: Fp. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed