proposition: Theorem Pigeonhole_bis : forall (A:Ensemble U) (f:U -> V), ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
proof: Proof. intros A f H'0 H'1; try assumption. elim (Image_set_continuous' A f (Im U V A f)); auto with sets. intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. elim (make_new_approximant A x); auto with sets. intros x0 H'2; elim H'2. intros H'5 H'6. elim (finite_cardinal V (Im U V A f)); auto with sets. intros n E. elim (finite_cardinal U x); auto with sets. - intros n0 E0. apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n). + apply card_add; auto with sets. + rewrite (Im_add U V x x0 f); auto with sets. cut (In V (Im U V x f) (f x0)). * intro H'8. rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets. rewrite H'4; auto with sets. * elim (Extension V (Im U V x f) (Im U V A f)); auto with sets. + apply Nat.lt_succ_r. apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f); auto with sets. rewrite H'4; auto with sets. - elim H'3; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image