proposition: Theorem Image_set_continuous' : forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), Approximant V (Im U V A f) X -> exists Y : _, Approximant U A Y /\ Im U V Y f = X.
proof: Proof. intros A f X H'; try assumption. cut (exists n : _, (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)). - intro H'0; elim H'0; intros n E; elim E; clear H'0. intros x H'0; try assumption. elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3; clear H'1 H'0; auto with sets. exists x. split; [ idtac | try assumption ]. apply Defn_of_Approximant; auto with sets. apply cardinal_finite with (n := n); auto with sets. - apply Image_set_continuous; auto with sets. + elim H'; auto with sets. + elim H'; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image