proposition: Lemma covered_by_finite P : (forall I (D : set I) A, (forall i, D i -> A i = set0) -> P I D A) -> (forall (I : pointedType) D A, finite_set D -> P I D A -> P nat `I_#|` fset_set D| (A \o nth point (fset_set D))) -> covered_by (@finite_set) P = [set X : set T | exists n A, [/\ P nat `I_n A & X = \bigcup_(i < n) A i]].
proof: Proof. move=> P0 Pc; apply/predeqP=> X; rewrite /covered_by /cover/=; split; last first. by move=> [n [A [Am ->]]]; exists nat, `I_n, A; split. case; elim/Ppointed=> I [D [A [Dfin Am ->]]]. exists 0%N, (fun=> set0); split; first by rewrite II0; apply: P0. by rewrite //= emptyE II0 !bigcup0. exists #|`fset_set D|, (A \o nth point (fset_set D)). split; first exact: Pc. by rewrite -bigsetU_fset_set// (big_nth point) big_mkord bigcup_mkord. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)