Package set-def: Definition of set types

Information

nameset-def
version1.26
descriptionDefinition of set types
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
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 | F }

universe = { x. x | T }

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

T

() = λ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 F F

t. (t F) ¬t

() = λp q. p q p

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

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