proposition: Lemma FiniteT_dec_Ensemble_has_cardinal {X : Type} (U : Ensemble X) : FiniteT X -> (forall x, In U x \/ ~ In U x) -> exists n, cardinal U n.
proof: Proof. intros. generalize dependent U. induction H. - intros. exists 0. pose proof (False_Ensembles_eq U Empty_set). subst. constructor. - intros. specialize (IHFiniteT (fun t : T => In U (Some t))). destruct IHFiniteT as [m]. { intros. unfold In at 1 3. apply H0. } specialize (H0 None) as [|]. + exists (S m). replace U with (Add (Im (fun t : T => In U (Some t)) Some) None). 1: constructor. 1: apply injection_preserves_cardinal. * assumption. * red; intros; congruence. * intros ?. inversion H2; subst; clear H2. congruence. * extensionality_ensembles; try (subst; assumption). destruct x. -- left. exists t; auto. -- right. constructor. + exists m. replace U with (Im (fun t : T => In U (Some t)) Some). 1: apply injection_preserves_cardinal. 1: assumption. 1: red; intros; congruence. extensionality_ensembles. * subst. assumption. * destruct x; try contradiction. exists t; auto. - intros. specialize (IHFiniteT (fun x : X => In U (f x))). destruct IHFiniteT as [m]. { intros. unfold In at 1 3. apply H1. } exists m. replace U with (Im (fun x : X => In U (f x)) f). 1: apply injection_preserves_cardinal. 1: assumption. + red; intros. apply invertible_impl_bijective in H0. destruct H0. apply H0 in H3. assumption. + extensionality_ensembles. * subst. assumption. * destruct H0. exists (g x); auto. unfold In at 1. rewrite H4. assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)