proposition: Lemma types_comparable: (exists f:X->Y, injective f) \/ (exists f:Y->X, injective f).
proof: Proof. pose proof premaximal_partial_injection. destruct H. apply premaximal_pi_is_full_or_surj in H. case H. left. assert (forall x0:X, In (pi_dom x) x0). rewrite H0. constructor. exists (fun x0:X => pi_func x x0 (H1 x0)). red; intros. apply pi_inj in H2. assumption. right. assert (forall y:Y, { x0:X | exists i:In (pi_dom x) x0, pi_func x x0 i = y }). intro. apply constructive_definite_description. pose proof (H0 y). destruct H1. exists x0. red; split. assumption. intros. destruct H1. destruct H2. destruct H2. apply pi_inj in H1. assumption. exists (fun y:Y => proj1_sig (X0 y)). red; intros. destruct X0 in H1; destruct X0 in H1; simpl in H1. destruct e; destruct e0. destruct H1. assert (x3 = x4). apply proof_irrelevance. now destruct H1, H2. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice ZornsLemma EnsemblesImplicit ProofIrrelevance FunctionalExtensionality Description