proposition: Lemma le_cardinal_ens_Empty_set (X : Type) {Y : Type} (U : Ensemble Y) : le_cardinal_ens (@Empty_set X) U.
proof: Proof. destruct (classic (inhabited Y)). - destruct H as [y]. right. exists (fun _ => y). firstorder. - left. 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)