proposition: Lemma cover_compactE : cover_compact = [set A | forall (I : choiceType) (D : set I) (f : I -> set T), open_fam_of A D f -> A `<=` cover D f -> finite_subset_cover D f A].
proof: Proof. rewrite predeqE => A; split=> [Aco I D f [g gop feAg] fcov|Aco I D f fop fcov]. have gcov : A `<=` \bigcup_(i in D) g i. by move=> p /fcov [i Di]; rewrite feAg // => - []; exists i. have [D' sD sgcov] := Aco _ _ _ gop gcov. exists D' => // p Ap; have /sgcov [i D'i gip] := Ap. by exists i => //; rewrite feAg //; have /sD := D'i; rewrite inE. have Afcov : A `<=` \bigcup_(i in D) (A `&` f i). by move=> p Ap; have /fcov [i ??] := Ap; exists i. have Afop : open_fam_of A D (fun i => A `&` f i) by exists f. have [D' sD sAfcov] := Aco _ _ _ Afop Afcov. by exists D' => // p /sAfcov [i ? []]; exists i. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed