Package set-size-def: Definition of finite set cardinality

Information

nameset-size-def
version1.18
descriptionDefinition of finite set cardinality
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-02-07
requiresbool
showData.Bool
Number.Natural
Set

Files

Defined Constants

Theorems

size = fold (λx n. suc n) 0

s n. hasSize s n finite s size s = n

Input Type Operators

Input Constants

Assumptions

() = λp. p = λx.