[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Cardinality over strict subsets



I'm happy to add this to the prelude for the next release.
Are there others like this that you know of belong in the
prelude (or, if more specialized, in the finite_sets
library)?

Sam Owre

Jerry James <loganjerry@xxxxxxxxx> wrote:

> 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/