proposition: Theorem Image_set_continuous : forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), Finite V X -> Included V X (Im U V A f) -> exists n : _, (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
proof: Proof. intros A f X H'; elim H'. - intro H'0; exists 0. exists (Empty_set U); auto with sets. - intros A0 H'0 H'1 x H'2 H'3; try assumption. lapply H'1; [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ]; auto with sets. intros x0 H'1; try assumption. exists (S n); try assumption. elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6; clear H'4 H'1. clear E. generalize H'2. rewrite <- H'5. intro H'1; try assumption. red in H'3. generalize (H'3 x). intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ]; auto with sets. specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x); intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ]; auto with sets. intros x1 H'4; try assumption. apply ex_intro with (x := Add U x0 x1). split; [ split; [ try assumption | idtac ] | idtac ]. + apply card_add; auto with sets. red; intro H'9; try exact H'9. apply H'1. elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets. + elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets. red; auto with sets. intros x2 H'4; elim H'4; auto with sets. intros x3 H'11; elim H'11; auto with sets. + elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets. apply Im_add; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image