Entry	Value
Package Name	set-size-def
Count	2
Theorems	CARD : CARD = ITSET (\x n. SUC n) 0 HAS_SIZE : !s n. s HAS_SIZE n <=> FINITE s /\ CARD s = n

Back to main package page