proposition: Lemma finite_indexed_union {A T : Type} {F : IndexedFamily A T} : FiniteT A -> (forall a, Finite (F a)) -> Finite (IndexedUnion F).
proof: Proof. intro H. induction H; intros. - replace (IndexedUnion F) with (@Empty_set T). + constructor. + extensionality_ensembles. destruct a. - replace (IndexedUnion F) with (Union (IndexedUnion (fun t => In (F (Some t)))) (F None)). + apply Union_preserves_Finite. * apply IHFiniteT. intro. apply H0. * apply H0. + extensionality_ensembles. * econstructor. eassumption. * econstructor. eassumption. * destruct a. ** left. econstructor. eassumption. ** now right. - replace (IndexedUnion F) with (IndexedUnion (fun x => F (f x))). + apply IHFiniteT. intro. apply H1. + extensionality_ensembles. * econstructor. eassumption. * destruct H0. rewrite <- (H3 a) in H2. econstructor. eassumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)