proposition: Lemma eq_cardinal_ens_sym_dec {A B : Type} (HA : inhabited A \/ ~ inhabited A) (U : Ensemble A) (V : Ensemble B) (HVdec : forall b : B, In V b \/ ~ In V b) : eq_cardinal_ens U V -> eq_cardinal_ens V U.
proof: Proof. intros [[H0 H1]|[f [Hf0 Hf1]]]. - right. exists (fun b : B => False_rect A (H0 b)). split; [|split]; intros ? ?; try contradiction. firstorder. - destruct HA. 2: { left. split. { intros a; apply H; constructor; auto. } intros b Hb. destruct Hf1 as [_ Hf1]. specialize (Hf1 b Hb) as [a [Ha0 Ha1]]. apply H. constructor; auto. } right. destruct H as [a0]. pose proof (bijective_impl_invertible_ens_dec f U V a0 HVdec Hf0 Hf1) as [g Hfg]. exists g. split. + apply (inverse_map_ens_surjective_ens_range f); auto. apply Hf1. + apply (inverse_map_ens_range_bijective_ens f); auto. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)