Package set-finite-thm: Properties of finite sets

Information

nameset-finite-thm
version1.28
descriptionProperties of finite sets
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
requiresbool
function
pair
natural
set-def
set-thm
set-finite-def
showData.Bool
Data.Pair
Function
Number.Natural
Set

Files

Theorems

finite universe

infinite universe

a. finite (insert a )

s. infinite s ¬(s = )

s x. finite s finite (delete s x)

s x. finite (delete s x) finite s

s x. finite (insert x s) finite s

s t. finite s finite (s \ t)

s. finite s a. ¬(a s)

f s. finite s finite (image f s)

s t. finite t s t finite s

n. finite { m. m | m < n }

n. finite { m. m | m n }

s t. finite (s t) finite s finite t

s t. finite s finite t finite (s t)

s t. infinite s finite t infinite (s \ t)

s t. finite s finite t finite (s t)

s t. finite s finite t finite (cross s t)

s. finite s a. x. x s x a

s. finite s finite { t. t | t s }

s. finite s (finite (bigUnion s) t. t s finite t)

s. finite (bigUnion s) finite s t. t s finite t

s P. finite s finite { x. x | x s P x }

f s. (x y. f x = f y x = y) infinite s infinite (image f s)

f. (x y. f x = f y x = y) s. infinite (image f s) infinite s

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

f s t.
    finite t t image f s s'. finite s' s' s t = image f s'

f s t.
    finite t t image f s s'. finite s' s' s t image f s'

s t. finite s finite t finite { x y. x, y | x s y t }

P.
    P (x s. P s ¬(x s) finite s P (insert x s))
    s. finite s P s

P f s.
    (t. finite t t image f s P t)
    t. finite t t s P (image f t)

f s.
    (x y. x s y s f x = f y x = y)
    (finite (image f s) finite s)

f A. (x y. f x = f y x = y) finite A finite { x. x | f x A }

f t.
    finite t (y. y t finite { x. x | f x = y })
    finite { x. x | f x t }

f s t.
    finite s (x. x s finite (t x))
    finite { x y. f x y | x s y t x }

d s t.
    finite s finite t
    finite { f. f | (x. x s f x t) x. ¬(x s) f x = d }

f A s.
    (x y. x s y s f x = f y x = y) finite A
    finite { x. x | x s f x A }

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

Input Type Operators

Input Constants

Assumptions

T

finite

¬F T

¬T F

bigUnion =

x. x universe

t. t t

s. s s

F p. p

fromPredicate (λx. F) =

x. ¬(x )

t. t ¬t

(¬) = λp. p F

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) t

t. F t F

t. T t t

t. t F F

t. t T t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

universe = insert T (insert F )

t. (t F) ¬t

t. t F ¬t

s. infinite s ¬finite s

x s. delete s x s

m n. m max m n

m n. n max m n

s t. s \ t s

() = λp q. p q p

t. (t T) (t F)

s. s s =

p x. p x p ((select) p)

x y. x = y y = x

x s. finite s finite (insert x s)

a b. (a b) a b

p x. x fromPredicate p p x

m n. ¬(m n) n < m

m n. m < suc n m n

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

() = λP. q. (x. P x q) q

x s. x s insert x s = s

x s. insert x s = insert x s

t1 t2. ¬t1 ¬t2 t2 t1

s u. bigUnion (insert s u) = s bigUnion u

{ m. m | m < 0 } =

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

x s. delete s x = s ¬(x s)

P. (p. P p) p1 p2. P (p1, p2)

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

x s. x s insert x (delete s x) = s

PAIR'. fn. a0 a1. fn (a0, a1) = PAIR' a0 a1

(s. s = s) s. s = s

f s x. x s f x image f s

P. (x y. P x y) y x. P x y

P Q. (x. P Q x) P x. Q x

m n. m < suc n m = n m < n

x s t. s insert x t delete s x t

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m n n p m p

s t u. s t u s \ t u

s t u. s t u = s (t u)

s t. s t x. x s x t

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

f s t. s t image f s image f t

f g s. image (f g) s = image f (image g s)

P. P 0 (n. P n P (suc n)) n. P n

s x. x bigUnion s t. t s x t

p x. x { y. y | p y } p x

(s t. s s t) s t. s t s

(s t. s t s) s t. t s s

x y s. x insert y s x = y x s

s t x. x s t x s x t

y s f. y image f s x. y = f x x s

P c x y. P (if c then x else y) (c P x) (¬c P y)

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

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

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

P f s. (y. y image f s P y) x. x s P (f x)

P f s. (y. y image f s P y) x. x s P (f x)

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

n. { m. m | m < suc n } = insert n { m. m | m < n }

P a b. (a, b) { x y. x, y | P x y } P a b

d t.
    { f. f | (x. x f x t) x. ¬(x ) f x = d } =
    insert (λx. d)

p f q. (z. z { x y. f x y | p x y } q z) x y. p x y q (f x y)

s t a.
    { x y. x, y | x insert a s y t x } =
    image ((,) a) (t a) { x y. x, y | x s y t x }

s.
    { t. t | t s } =
    image (λp. { x. x | p x })
      { p. p | (x. x s p x universe) x. ¬(x s) (p x F) }

d a s t.
    { f. f |
      (x. x insert a s f x t) x. ¬(x insert a s) f x = d } =
    image (λ(b, g) x. if x = a then b else g x)
      (cross t { f. f | (x. x s f x t) x. ¬(x s) f x = d })