proposition: Lemma compact_In0 : compact = [set A | forall (I : choiceType) (D : set I) (f : I -> set T), closed_fam_of A D f -> finI D f -> \bigcap_(i in D) f i !=set0].
proof: Proof. rewrite predeqE => A; split=> [Aco I D f [g gcl feAg] finIf|Aco F FF FA]. case: (pselect (exists i, D i)) => [[i Di] | /asboolP]; last first. by rewrite asbool_neg => /forallp_asboolPn D0; exists point => ? /D0. have [|p [Ap clfinIfp]] := Aco _ (finI_filter finIf). by exists (f i); [apply: finI_from1|rewrite feAg // => ? []]. exists p => j Dj; rewrite feAg //; split=> //; apply: gcl => // B. by apply: clfinIfp; exists (f j); [apply: finI_from1|rewrite feAg // => ? []]. have finIAclF : finI F (fun B => A `&` closure B). apply: (@filter_finI _ F) => B FB. by apply: filterI => //; apply: filterS FB; apply: subset_closure. have [|p AclFIp] := Aco _ _ _ _ finIAclF. by exists closure=> //; move=> ??; apply: closed_closure. exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA. by have /AclFIp [_] := FB; move=> /(_ _ p_C). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed