Package set-size-thm: Properties of finite set cardinality

Information

nameset-size-thm
version1.62
descriptionProperties of finite set cardinality
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-11-01
checksum991eeb63589e6778f7794277e2205194afe11ae8
requiresbool
natural
pair
set-def
set-finite
set-fold
set-size-def
set-thm
showData.Bool
Data.Pair
Number.Natural
Set

Files

Theorems

size = 0

hasSize universe 2

x. hasSize (insert x ) 1

finite universe finite universe finite universe

x. size (insert x ) = 1

s. finite s hasSize s (size s)

s. hasSize s 0 s =

s n. hasSize s n size s = n

s. finite s (size s = 0 s = )

f s. finite s size (image f s) size s

n. hasSize { m. m | m < n } n

finite universe finite universe
  size universe = size universe size universe

n. size { m. m | m < n } = n

a b. a b finite b size a < size b

a b. a b finite b size a size b

m n. hasSize universe m hasSize universe n hasSize universe (n m)

n. hasSize { m. m | m n } (n + 1)

n. size { m. m | m n } = n + 1

f s t. finite t s image f t size s size t

s t. finite s finite t size (s t) size s + size t

s t. finite t s t (size s = size t s = t)

a b. finite b a b size a = size b a = b

a b. finite b a b size b size a a = b

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

s n. finite s n size s t. t s hasSize t n

s n. (finite s n size s) t. t s hasSize t n

x s.
    finite s size (insert x s) = if x s then size s else suc (size s)

s t. finite s t s size (s \ t) = size s - size t

s t. finite s finite t size (s t) = size s + size (t \ s)

s t m n. hasSize s m hasSize t n hasSize (cross s t) (m * n)

x s. finite s size (delete s x) = if x s then size s - 1 else size s

s. finite s size { t. t | t s } = 2 size s

s n. hasSize s n hasSize { t. t | t s } (2 n)

s t.
    finite s finite t (size (s t) = size s + size t disjoint s t)

s t. finite s finite t disjoint s t size (s t) = size s + size t

s n. hasSize s (suc n) ¬(s = ) a. a s hasSize (delete s a) n

s t. finite s finite t size (s t) = size s + size t - size (s t)

s t. finite s finite t size (s t) + size (s t) = size s + size t

s t.
    finite s finite t size (s t) < size s + size t ¬disjoint s t

s n. hasSize s (suc n) a t. hasSize t n ¬(a t) s = insert a t

s t m n.
    hasSize s m hasSize t n disjoint s t hasSize (s t) (m + n)

s t m n. hasSize s m hasSize t n t s hasSize (s \ t) (m - n)

s t u. finite u disjoint s t s t = u size s + size t = size u

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

s t.
    finite s finite t
    size { x y. (x, y) | x s y t } = size s * size t

s n.
    hasSize s n
    f. (m. m < n f m s) x. x s ∃!m. m < n f m = x

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

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

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

f s n.
    (x y. x s y s f x = f y x = y)
    (hasSize (image f s) n hasSize s n)

f s n.
    (x y. x s y s f x = f y x = y) hasSize s n
    hasSize (image f s) n

s t m n.
    hasSize s m hasSize t n
    hasSize { x y. (x, y) | x s y t } (m * n)

n s u.
    s u finite s size s n (finite u n size u)
    t. s t t u hasSize t n

f s t.
    finite s (x. x s f x t) (y. y t ∃!x. x s f x = y)
    size t = size s

s t f.
    finite s size s = size t image f s = t
    x y. x s y s f x = f y x = y

s t.
    finite s finite t size s size t
    f. image f s t x y. x s y s f x = f y x = y

s t m n.
    hasSize s m (x. x s finite (t x) size (t x) n)
    size (bigUnion { x. t x | x s }) m * n

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    hasSize { x y. (x, y) | x s y t x } (m * n)

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

d s t m n.
    hasSize s m hasSize t n
    hasSize { f. f | (x. x s f x t) x. ¬(x s) f x = d }
      (n m)

s t f g n.
    (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) hasSize s n hasSize t n

s t f g.
    (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) n. hasSize s n hasSize t n

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

s t f g.
    (finite s finite t) (x. x s f x t g (f x) = x)
    (y. y t g y s f (g y) = y) size s = size t

s t.
    finite s finite t size s = size t
    f g.
      (x. x s f x t g (f x) = x)
      y. y t g y s f (g y) = y

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

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    (x y. x s y s ¬(x = y) disjoint (t x) (t y))
    hasSize (bigUnion { x. t x | x s }) (m * n)

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

External Type Operators

External Constants

Assumptions

finite

¬

¬

bit0 0 = 0

bigUnion =

x. x universe

t. t t

n. 0 n

n. n n

s. s

s. s s

p. p

x. ¬(x )

a. finite (insert a )

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. n < suc n

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

n. ¬(suc n = 0)

n. 0 * n = 0

n. 0 + n = n

m. m - 0 = m

n. n - n = 0

s. s = s

f. image f =

universe = insert (insert )

size = fold (λx n. suc n) 0

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m 0 = 1

s. infinite s ¬finite s

x s. delete s x s

m n. n m + n

s t. disjoint s (t \ s)

s t. s s t

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

m. m 0 m = 0

n. suc n - 1 = n

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

x s. ¬(insert x s = )

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

n. bit0 (suc n) = suc (suc (bit0 n))

f y. (let x y in f x) = f y

x. a b. x = (a, b)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

m n. m * n = n * m

m n. m + n = n + m

m n. m = n m n

m n. m < n m n

m n. m + n - n = m

s x. finite (delete s x) finite s

s x. finite (insert x s) finite s

s t. finite s finite (s \ t)

s t. s t = t s

f s. finite s finite (image f s)

p x. x fromPredicate p p x

universe = { x. x | }

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc 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

t1 t2. ¬t1 ¬t2 t2 t1

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

m n. suc m suc n m n

m n. m + n = m n = 0

s t. disjoint s t s t =

s t. s t s t = t

s t. s \ t = s t

s t. s \ t = s disjoint s t

s t. s \ t \ t = s \ t

s t. s \ t t = s t

s t. finite t s t finite s

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

{ m. m | m < 0 } =

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

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. m * suc n = m + m * n

m n. m suc n = m * m n

m n. suc m * n = m * n + n

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

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

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

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

m n. m n d. n = m + d

s t x. s t s insert x t

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

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

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

m n. n m m - n + n = m

m n. m n n m m = n

s n. hasSize s n finite s size s = n

s t. s (t \ s) = t s t

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

m n. m < n m n ¬(m = n)

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

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

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

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

s. bigUnion s = t. t s t =

x y z. x = y y = z x = z

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 + p) = m + n + p

m n p. m + n = m + p n = p

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

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

m n. n < m suc (m - suc n) = m - n

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

s t. disjoint s (bigUnion t) x. x t disjoint s x

f x s. image f (insert x s) = insert (f x) (image f s)

p. p 0 (n. p n p (suc n)) n. p n

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

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

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

s t x. x s t x s x t

s t x. x s t x s x t

s t u. s t \ u s t disjoint s u

s t u. s t u s u t u

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

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

x s t. disjoint (insert x s) t ¬(x t) disjoint s t

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

s t x. x s \ t x s ¬(x t)

s. s = x t. s = insert x t ¬(x t)

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 q x) (x. p x) x. q x

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

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

m n p q. m p n q m + n p + q

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

x s t. insert x s t = if x t then s t else insert x (s t)

p. (∃!x. p x) (x. p x) x x'. p x p x' x = 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

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

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

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

f s t.
    (y. y t x. x s f x = y)
    g. y. y t g y s f (g y) = y

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

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 b.
    (x y s. ¬(x = y) f x (f y s) = f y (f x s))
    fold f b = b
    x s.
      finite s
      fold f b (insert x s) =
      if x s then fold f b s else f x (fold f b s)

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