Re: [PVS-Help] Cardinality over strict subsets

["Jerry James" <loganjerry@xxxxxxxxx>]

On Wed, Aug 13, 2008 at 3:46 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> I'd like to prove for all non-empty finite sets, A and B, that:
>
>  strict_subset?(A, B) => card(A) < card(B)
>
> I've searched the prelude, and extended prelude, to find several other
> cardinality lemmas, but not this specific one. I'm wondering whether
> I'm missing something, or in fact this particular lemma has yet to be
> shown/included. Thanks.
>
> jerome

That follows immediately from card_subset and same_card_subset.  I
agree, it would be nice to have it as a separate theorem somewhere.
I've needed that result many times myself, but have always used
card_subset + same_card_subset instead of figuring out where
"somewhere" should be.
-- 
Jerry James
http://loganjerry.googlepages.com/