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: Families Image ImageImplicit FiniteTypes EnsemblesTactics