proposition: Lemma injective_inverse_image_Singleton {X Y : Type} (f : X -> Y) : injective f <-> forall x, inverse_image f (Singleton (f x)) = Singleton x.
proof: Proof. split. - intros Hf x. apply Extensionality_Ensembles; split. + intros x0 Hx0. destruct Hx0. apply Singleton_inv in H. apply Hf in H. subst. constructor. + intros x0 Hx0. destruct Hx0. constructor. constructor. - intros Hf x0 x1 Hx. apply Singleton_inv. rewrite <- Hf. constructor. apply Singleton_intro. assumption. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)