proposition: Lemma compact_cover : compact = cover_compact.
proof: Proof. rewrite compact_In0 cover_compactE predeqE => A. split=> [Aco I D f [g gop feAg] fcov|Aco I D f [g gcl feAg]]. case: (pselect (exists i, D i)) => [[j Dj] | /asboolP]; last first. rewrite asbool_neg => /forallp_asboolPn D0. by exists fset0 => // ? /fcov [? /D0]. apply/exists2P; apply: contrapT. move=> /asboolP; rewrite asbool_neg => /forallp_asboolPn sfncov. suff [p IAnfp] : \bigcap_(i in D) (A `\` f i) !=set0. by have /IAnfp [Ap _] := Dj; have /fcov [k /IAnfp [_]] := Ap. apply: Aco. exists (fun i => ~` g i) => i Di; first exact/open_closedC/gop. rewrite predeqE => p; split=> [[Ap nfip] | [Ap ngip]]; split=> //. by move=> gip; apply: nfip; rewrite feAg. by rewrite feAg // => - []. move=> D' sD. have /asboolP : ~ A `<=` cover [set` D'] f by move=> sAIf; exact: (sfncov D'). rewrite asbool_neg => /existsp_asboolPn [p /asboolP]. rewrite asbool_neg => /imply_asboolPn [Ap nUfp]. by exists p => i D'i; split=> // fip; apply: nUfp; exists i. case: (pselect (exists i, D i)) => [[j Dj] | /asboolP]; last first. by rewrite asbool_neg => /forallp_asboolPn D0 => _; exists point => ? /D0. apply: contraPP => /asboolP; rewrite asbool_neg => /forallp_asboolPn If0. apply/asboolP; rewrite asbool_neg; apply/existsp_asboolPn. have Anfcov : A `<=` \bigcup_(i in D) (A `\` f i). move=> p Ap; have /asboolP := If0 p; rewrite asbool_neg => /existsp_asboolPn. move=> [i /asboolP]; rewrite asbool_neg => /imply_asboolPn [Di nfip]. by exists i. have Anfop : open_fam_of A D (fun i => A `\` f i). exists (fun i => ~` g i) => i Di; first exact/closed_openC/gcl. rewrite predeqE => p; split=> [[Ap nfip] | [Ap ngip]]; split=> //. by move=> gip; apply: nfip; rewrite feAg. by rewrite feAg // => - []. have [D' sD sAnfcov] := Aco _ _ _ Anfop Anfcov. wlog [k D'k] : D' sD sAnfcov / exists i, i \in D'. move=> /(_ (D' `|` [fset j])%fset); apply. - by move=> k; rewrite !inE => /orP [/sD|/eqP->] //; rewrite inE. - by move=> p /sAnfcov [i D'i Anfip]; exists i => //=; rewrite !inE D'i. - by exists j; rewrite !inE orbC eq_refl. exists D' => /(_ sD) [p Ifp]. have /Ifp := D'k; rewrite feAg; last by have /sD := D'k; rewrite inE. by move=> [/sAnfcov [i D'i [_ nfip]] _]; have /Ifp := D'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