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

Information

nameset-size-def
version1.31
descriptionDefinition of finite set cardinality
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-12-02
requiresbool
natural
set-fold
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

External Type Operators

External Constants

Assumptions

() = λp. p = λx.