Package set-finite-thm: Properties of finite sets

Information

nameset-finite-thm
version1.68
descriptionProperties of finite sets
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory exported on 2019-10-31
checksumd1c44780608e6904de387e5472013073d66c7c6f
requiresbool
function
natural
pair
set-def
set-finite-def
set-thm
showData.Bool
Data.Pair
Function
Number.Natural
Set

Files

Theorems

finite universe

infinite universe

finite universe finite universe

infinite universe infinite universe

a. finite (insert a )

finite universe finite universe finite universe

infinite universe infinite universe infinite universe

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

s t. infinite s s t infinite t

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. infinite s N. n. N n n s

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

s. finite { t. t | t s } finite 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 }

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

s t.
    infinite (cross s t) ¬(s = ) infinite t infinite s ¬(t = )

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. finite (image f s) t. finite t t s image f s = image f t

f s. finite s s bigUnion f g. finite g g f s bigUnion g

s. infinite s r. (m n. m < n r m < r n) image r universe = s

s. infinite s r. (m n. m < n r m < r n) image r universe = s

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 }

f.
    finite f
    bigUnion { t. t | t f u. u f ¬(t u) } = bigUnion f

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)

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 s.
    infinite s (x y. x s y s f x = f y x = y)
    infinite (image f s)

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

f.
    finite f ¬(f = ) (s t. s f t f s t t s)
    bigIntersect f f

f.
    finite f ¬(f = ) (s t. s f t f s t t s)
    bigUnion f f

f s.
    infinite s finite (image f s)
    a. a s infinite { x. x | x s f x = f 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 }

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

f s.
    finite s s bigUnion f ¬(f = )
    (t u. t f u f t u u t) t. t f s t

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

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

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

r s.
    finite s (x. ¬r x x) (x y z. r x y r y z r x z)
    (x. x s y. y s r x y) s =

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

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

External Type Operators

External Constants

Assumptions

finite

¬(universe = )

¬

¬

bigIntersect = universe

bigUnion =

x. x universe

t. t t

n. 0 n

s. s

s. s s

p. p

fromPredicate (λx. ) =

cross universe universe = universe

x. ¬(x )

x. id x = x

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. n < suc n

n. n suc n

s. ¬(s s)

(¬) = λp. 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

t. t t

t. t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t t

s. s universe = s

s. s = s

s. s = s

s. cross s =

s. cross s =

universe = insert (insert )

t. ( t) ¬t

t. (t ) ¬t

t. t ¬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 s t

s t. s t s

s t. s \ t s

s t. s t s

s t. t s s

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

s. s s =

a b. fst (a, b) = a

a b. snd (a, b) = b

x s. ¬(insert x s = )

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

x y. x = y y = x

x s. finite s finite (insert x s)

t1 t2. t1 t2 t2 t1

a b. (a b) a b

m n. m < n m n

s t. s t = t s

s t. s t = t s

s t. s t s t

p x. x fromPredicate p p x

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

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

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

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

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

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

x y. x insert y x = y

x s. x s insert x s = s

x s. insert x s = insert x s

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

s t. s t s t = s

s t. s t s t = t

s u. bigIntersect (insert s u) = s bigIntersect u

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

f g. f g bigUnion f bigUnion g

{ m. m | m < 0 } =

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

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

p. (x. p x) a b. p (a, b)

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

p a. (x. x = a p x) p a

p a. (x. a = x p x) p a

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

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

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

m n. m n n m m = n

s t. s t t s s = t

f. fn. a b. fn (a, b) = f a b

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

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

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

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

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

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

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

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

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

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

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

m n p. m < n n < p m < p

m n p. m < n n p m < p

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 u. s t t u s u

s t u. s t t u s 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)

r. (x. y. r x y) f. x. r x (f x)

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

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

p q r. p q r (p r) (q r)

s t x. x s t x s x t

(∃!) = λp. () p x y. p x p y x = y

s p. { x. x | x s p x } s

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

p. (n. (m. m < n p m) p n) n. p n

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

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

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

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

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

p. (n. p n) n. p n m. m < n ¬p m

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

a b a' b'. (a, b) = (a', b') a = a' b = b'

x y s t. (x, y) cross s t x s y t

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 } =

p. p (x s. p s p (insert x s)) a. finite a p a

s t. (x. x s y. y t x y) bigUnion s bigUnion t

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 }

f s. bigUnion (image f s) = { y. y | x. x s y f x }

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

p a s. (x. x insert a s p x) p a x. x s p x

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

p. (n. p n) (m. n. p n n m) m. p m n. p n n m

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

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

p f. bigUnion { x. f x | p x } = { a. a | x. p x a f x }

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)

f s t.
    s image f t
    u. u t (x y. x u y u f x = f y x = y) s = image f u

p f s.
    (t. t image f s p t)
    t. t s (x y. x t y t f x = f y x = y) p (image f t)

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

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