proposition: Lemma finite_intersections_countable {X : Type} (F : Family X) : Countable F -> Countable (finite_intersections F).
proof: Proof. intros [f Hf]. rewrite <- finite_intersections_len_union. apply countable_union. - apply nat_countable. - intro n. induction n. + apply intro_nat_injection with (fun x => 0). intros [U HU] [V HV] eq. apply proj1_sig_injective. simpl. now rewrite (finite_intersections_len_0_full_set HU), (finite_intersections_len_0_full_set HV). + destruct (finite_intersections_len_S_choice F n) as [g Hg], IHn as [fn Hfn]. refine (inj_countable (fun U => (fn (fst (g U)), f (exist _ (proj1_sig (snd (g U))) _))) countable_nat_product _). intros [U HU] [V HV] eq. injection eq as eq1 eq2. apply Hfn, proj1_sig_eq in eq1. apply Hf, proj1_sig_eq in eq2. apply Proj1SigInjective.proj1_sig_injective. now rewrite Hg, Hg, eq1, eq2. Unshelve. destruct (snd (g U)). now apply finite_intersections_len_1_in. Qed.
imports: Coq(Program.Equality) Coq(Lia) Coq(ClassicalChoice) Ensembles EnsemblesImplicit Families FiniteTypes IndexedFamilies CountableTypes Proj1SigInjective Powerset_facts