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

[PVS-Help] Cardinality over strict subsets

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.