proposition: Lemma injective_preserves_cardinal : forall (A:Ensemble U) (f:U -> V) (n:nat), injective f -> cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
proof: Proof. induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. - rewrite (image_empty f). intros n' CE. apply cardinal_unicity with V (Empty_set V); auto with sets. - intro n'. rewrite (Im_add A x f). intro H'3. elim cardinal_Im_intro with A f n; trivial with sets. intros i CI. lapply (H'1 i); trivial with sets. cut (~ In _ (Im A f) (f x)). + intros H0 H1. apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. apply card_add; auto with sets. rewrite <- H1; trivial with sets. + red; intro; apply H'2. apply In_Image_elim with f; trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts