proposition: Lemma FiniteT_img: forall (X Y:Type) (f:X->Y), FiniteT X -> (forall y1 y2:Y, y1=y2 \/ y1<>y2) -> Finite (Im Full_set f).
proof: Proof. intros. induction H. - replace (Im Full_set f) with (@Empty_set Y). { constructor. } apply Extensionality_Ensembles; split; red; intros. + destruct H. + destruct H. destruct x. - assert ((exists x:T, f (Some x) = f None) \/ (forall x:T, f (Some x) <> f None)). { apply finite_dec_exists. { assumption. } intro. apply H0. } case H1. + intro. pose (g := fun (x:T) => f (Some x)). replace (Im Full_set f) with (Im Full_set g). { apply IHFiniteT. } apply Extensionality_Ensembles; split; red; intros. * destruct H3. subst. exists (Some x). -- constructor. -- reflexivity. * destruct H3. subst. destruct x. -- exists t. ++ constructor. ++ reflexivity. -- destruct H2. exists x. ++ constructor. ++ destruct H3. subst. symmetry. assumption. + intros. pose (g := fun x:T => f (Some x)). replace (Im Full_set f) with (Add (Im Full_set g) (f None)). { constructor. - apply IHFiniteT. - red; intro. destruct H3. contradiction (H2 x). symmetry; assumption. } apply Extensionality_Ensembles; split; red; intros. * red; intros. destruct H3, H3. -- exists (Some x). ++ constructor. ++ assumption. -- exists None. ++ constructor. ++ reflexivity. * red; intros. destruct H3. destruct x. -- left. exists t. ++ constructor. ++ assumption. -- right. auto with sets. - pose (g := fun (x:X) => f (f0 x)). replace (Im Full_set f) with (Im Full_set g). { apply IHFiniteT. } apply Extensionality_Ensembles; split; red; intros. + destruct H2. exists (f0 x). * constructor. * assumption. + destruct H2, H1. subst. rewrite <- H4 with x. exists (g0 x). * constructor. * reflexivity. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)