proposition: Lemma eq_cardinal_ens_empty {X Y : Type} (U : Ensemble Y) : eq_cardinal_ens (@Empty_set X) U <-> (forall y : Y, ~ In U y).
proof: Proof. split. - intros [|[f [Hf0 [Hf1 Hf2]]]] y Hy. + tauto. + specialize (Hf2 y Hy) as [x [Hx Hxy]]. contradiction. - intros HU. destruct (classic (inhabited Y)). 2: { left; auto with sets. } right. destruct H as [y0]. exists (fun _ => y0). split; firstorder. 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)