Package set-def: Definition of set types

Information

nameset-def
version1.37
descriptionDefinition of set types
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-06-16
requiresbool
showData.Bool
Data.Pair
Set

Files

Defined Type Operator

Defined Constants

Theorems

s. rest s = delete s (choice s)

p x. x fromPredicate p p x

= { x. x | }

universe = { x. x | }

s. ¬(s = ) choice s s

s. singleton s x. s = insert x

s t. disjoint s t s t =

s t. bijections s t = injections s t surjections s t

s t. s t s t ¬(s = t)

s t. s t x. x s x t

s t. (x. x s x t) s = t

s. bigIntersect s = { x. x | u. u s x u }

s. bigUnion s = { x. x | u. u s x u }

x s. insert x s = { y. y | y = x y s }

s t. s t = { x. x | x s x t }

s t. s t = { x. x | x s x t }

s x. delete s x = { y. y | y s ¬(y = x) }

s t. s \ t = { x. x | x s ¬(x t) }

f s. image f s = { y. y | x. x s y = f x }

s t. cross s t = { x y. x, y | x s y t }

s t.
    surjections s t =
    { f. f | (x. x s f x t) x. x t y. y s f y = x }

s t.
    injections s t =
    { f. f |
      (x. x s f x t) x y. x s y s f x = f y x = y }

Input Type Operators

Input Constants

Assumptions

() = λp. p ((select) p)

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. (t ) ¬t

() = λp q. p q p

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

p. ¬(x. p x) x. ¬p x

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

t1 t2. ¬t1 ¬t2 t2 t1

f g. (x. f x = g x) f = g