proposition: Lemma finite_prod: forall (X Y:Type), FiniteT X -> FiniteT Y -> FiniteT (X*Y).
proof: Proof. intros. induction H0. apply bij_finite with _ (False_rect _). constructor. exists (@snd X False). destruct x. destruct y. destruct f. pose (g := fun (x:X*T + X) => match x with | inl (pair x0 t) => pair x0 (Some t) | inr x0 => pair x0 None end). pose (ginv := fun (x:X * option T) => match x with | (x0, Some t) => inl _ (x0, t) | (x0, None) => inr _ x0 end). apply bij_finite with _ g. apply finite_sum. assumption. assumption. exists ginv. destruct x as [[x0 t]|x0]; trivial. destruct y as [x0 [t|]]; trivial. pose (g := fun (y:X*X0) => match y with | pair x x0 => pair x (f x0) end). destruct H1. pose (ginv := fun (y:X*Y) => let (x,y0) := y in (x, g0 y0)). apply bij_finite with _ g. assumption. exists ginv. destruct x as [x x0]; unfold ginv, g; try rewrite H1; trivial. destruct y as [x y]; unfold ginv, g; try rewrite H2; trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description