proposition: Lemma Im_Included_injective {X Y : Type} (f : X -> Y) : injective f <-> forall U V : Ensemble X, Included U V <-> Included (Im U f) (Im V f).
proof: Proof. split. - intros. split. { apply Im_monotonous. } intros. red; intros. specialize (H0 (f x)). unshelve epose proof (H0 _); [|clear H0]. { exists x; auto. } inversion H2; subst; clear H2. apply H in H3. subst. assumption. - intros. red; intros. specialize (H (Singleton x) (Singleton y)) as [_]. unshelve epose proof (H _); [|clear H]. { red; intros. inversion H1; subst; clear H1. inversion H2; subst; clear H2. exists y; auto with sets. } unshelve epose proof (H1 x _); [|clear H1]. { constructor. } inversion H; subst; clear H. reflexivity. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)