proposition: Lemma covered_by_countable P : (forall I (D : set I) A, (forall i, D i -> A i = set0) -> P I D A) -> (forall (I : choiceType) (D : set I) (A : I -> set T) (f : nat -> I), set_surj [set: nat] D f -> P I D A -> P nat [set: nat] (A \o f)) -> covered_by (@countable) P = [set X : set T | exists A, [/\ P nat [set: nat] A & X = \bigcup_i A i]].
proof: Proof. move=> P0 Pc; apply/predeqP=> X; rewrite /covered_by /cover/=; split; last first. by move=> [A [Am ->]]; exists nat, [set: nat], A; split. case; elim/Ppointed=> I [D [A [Dcnt Am ->]]]. exists (fun=> set0); split; first exact: P0. by rewrite emptyE bigcup_set0 bigcup0. have /pfcard_geP[->|[f]] := Dcnt. exists (fun=> set0); split; first exact: P0. by rewrite !bigcup_set0 bigcup0. pose g := [splitsurjfun of split f]. exists (A \o g); split=> /=; first exact: Pc Am. apply/predeqP=> x; split=> [[i Di Aix]|[n _ Afnx]]. by exists (g^-1%FUN i) => //=; rewrite invK// inE. by exists (g n) => //; apply: funS. 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)