proposition: Lemma least_cardinal_ext_subset {X : Type} (P : Family X) (U : Ensemble X) : least_cardinal_subset P U -> least_cardinal_ext P U.
proof: Proof. intros [HU0 HU1]. split. - exists U; split; auto. reflexivity. - intros Y V [U' [HU'0 HU'1]]. specialize (HU1 U' HU'0). eapply le_cardinal_ens_Proper_r; eauto. 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)