[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Cardinality over strict subsets
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.
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.