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