Package set-finite-def: Definition of finite sets

Information

nameset-finite-def
version1.18
descriptionDefinition of finite sets
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-01-04
requiresbool
showData.Bool
Set

Files

Defined Constants

Theorems

finite

s. infinite s ¬finite s

x s. finite s finite (insert x s)

a. finite a a = x s. a = insert x s finite s

FINITE'.
    FINITE' (x s. FINITE' s FINITE' (insert x s))
    a. finite a FINITE' a

Input Type Operators

Input Constants

Assumptions

T

() = λp. p = λx. T

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

() = λp. q. (x. p x q) q

() = λp q. r. (p r) (q r) r

p q. (x. p x q x) (x. p x) x. q x

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2