add fiberwise_{finite,countable}_preimage

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- in file `cardinality.v`,
+  + lemmas `fiberwise_finite_preimage`, `fiberwise_countable_preimage`
+
 - file `Rstruct_topology.v`
 
 - package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`

classical/cardinality.v

@@ -840,6 +840,15 @@ have Gy : y \in G k by rewrite in_fset_set ?inE//; apply: Ffin.
 by exists (Tagged G [` Gy]%fset).
 Qed.
 
+Lemma fiberwise_finite_preimage {T U} (B : set U) (f : T -> U) :
+  finite_set B -> (forall b, B b -> finite_set (f @^-1` [set b])) ->
+  finite_set (f @^-1` B).
+Proof.
+move=> *.
+rewrite -(image_id B) -bigcup_imset1 preimage_bigcup.
+exact: bigcup_finite.
+Qed.
+
 Lemma trivIset_sum_card (T : choiceType) (F : nat -> set T) n :
   (forall n, finite_set (F n)) -> trivIset [set: nat] F ->
   (\sum_(i < n) #|` fset_set (F i)| =
@@ -1143,6 +1152,15 @@ apply/pcard_geP/surjPex; exists (fun (k : {i & G i}) => val (projT2 k)).
 by move=> x [i _] Gix/=; exists (Tagged G (SigSub (mem_set Gix))).
 Qed.
 
+Lemma fiberwise_countable_preimage {T U} (B : set U) (f : T -> U) :
+  countable B -> (forall b, B b -> countable (f @^-1` [set b])) ->
+  countable (f @^-1` B).
+Proof.
+move=> *.
+rewrite -(image_id B) -bigcup_imset1 preimage_bigcup.
+exact: bigcup_countable.
+Qed.
+
 Lemma countableXR T T' (A : set T) (B : T -> set T') :
   countable A -> (forall i, A i -> countable (B i)) -> countable (A `*`` B).
 Proof.