Package set-size: Sizes of finite sets

Information

nameset-size
version1.9
descriptionSizes of finite sets
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Set

Files

Defined Constants

Theorems

size = 0

hasSize universe 2

x. hasSize (insert x ) 1

x. size (insert x ) = 1

s. finite s hasSize s (size s)

s. hasSize s 0 s =

s. size s = fold (λx n. Number.Natural.suc n) s 0

s n. hasSize s n size s = n

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

f s. finite s Number.Natural.≤ (size (image f s)) (size s)

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

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

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

a b. a b finite b Number.Natural.< (size a) (size b)

a b. a b finite b Number.Natural.≤ (size a) (size b)

n. hasSize { m. m | Number.Natural.≤ m n } (Number.Natural.+ n 1)

n. size { m. m | Number.Natural.≤ m n } = Number.Natural.+ n 1

f s t. finite t s image f t Number.Natural.≤ (size s) (size t)

s t.
    finite s finite t
    Number.Natural.≤ (size (s t)) (Number.Natural.+ (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 Number.Natural.≤ (size b) (size a) a = b

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

s n. finite s Number.Natural.≤ n (size s) t. t s hasSize t n

s n. (finite s Number.Natural.≤ n (size s)) t. t s hasSize t n

s t.
    finite s t s size (s - t) = Number.Natural.- (size s) (size t)

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

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

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

s. finite s size { t. t | t s } = Number.Natural.exp 2 (size s)

s n. hasSize s n hasSize { t. t | t s } (Number.Natural.exp 2 n)

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

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

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

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

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

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

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

s t m n.
    hasSize s m hasSize t n t s
    hasSize (s - t) (Number.Natural.- m n)

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

s t u.
    finite u disjoint s t s t = u
    Number.Natural.+ (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. Data.Pair., x y | x s y t } =
    Number.Natural.* (size s) (size t)

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

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. hasSize s 0 s = )
  s n.
    hasSize s (Number.Natural.suc n)
    a t. hasSize t n ¬(a t) s = insert a t

s t m n.
    hasSize s m hasSize t n
    hasSize { x y. Data.Pair., x y | x s y t } (Number.Natural.* m 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 Number.Natural.≤ (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) Number.Natural.≤ (size (t x)) n)
    Number.Natural.≤ (size (bigUnion { x. t x | x s }))
      (Number.Natural.* m n)

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    hasSize { x y. Data.Pair., x y | x s y t x }
      (Number.Natural.* m n)

d s t.
    finite s finite t
    size { f. f | (x. x s f x t) x. ¬(x s) f x = d } =
    Number.Natural.exp (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 }
      (Number.Natural.exp 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 }) (Number.Natural.* 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

Input Type Operators

Input Constants

Assumptions

T

finite

bigUnion =

n. Number.Natural.≤ 0 n

n. Number.Natural.≤ n n

s. s

s. s s

F p. p

1 = Number.Natural.suc 0

x. ¬(x )

a. finite (insert a )

t. t ¬t

n. ¬Number.Natural.< n n

n. Number.Natural.< n (Number.Natural.suc n)

(~) = λp. p F

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx. T

x. x = x T

n. ¬(Number.Natural.suc n = 0)

m. Number.Natural.- m 0 = m

n. Number.Natural.- n n = 0

universe = insert T (insert F )

n. Number.Natural.bit0 n = Number.Natural.+ n n

s t. disjoint s (t - s)

() = λp q. p q p

t. (t T) (t F)

n. Number.Natural.bit1 n = Number.Natural.suc (Number.Natural.+ n n)

m. Number.Natural.suc m = Number.Natural.+ m 1

n. Number.Natural.- (Number.Natural.suc n) 1 = n

x s. ¬(insert x s = )

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

(¬T F) (¬F T)

f y. (let xyf x) = f y

p. x y. p = Data.Pair., x y

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

m n. Number.Natural.* m n = Number.Natural.* n m

m n. Number.Natural.+ m n = Number.Natural.+ n m

m n. m = n Number.Natural.≤ m n

m n. Number.Natural.< m n Number.Natural.≤ m n

m n. Number.Natural.- (Number.Natural.+ 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

m n. ¬Number.Natural.≤ m n Number.Natural.< n m

m n. Number.Natural.< m (Number.Natural.suc n) Number.Natural.≤ m n

m n. Number.Natural.≤ (Number.Natural.suc m) n Number.Natural.< m n

m. m = 0 n. m = Number.Natural.suc n

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

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

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

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

m n. Number.Natural.suc m = Number.Natural.suc n m = n

m n.
    Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.≤ m n

m n. Number.Natural.+ 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 | Number.Natural.< m 0 } =

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

m n.
    Number.Natural.* m (Number.Natural.suc n) =
    Number.Natural.+ m (Number.Natural.* m n)

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

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

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

m n. Number.Natural.≤ m n d. n = Number.Natural.+ m d

s t x. s t s insert x t

f g. f = g x. f x = g x

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

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

m n. Number.Natural.≤ m n Number.Natural.≤ n m m = n

s t. s (t - s) = t s t

s t. s t t s s = t

PAIR'. fn. a0 a1. fn (Data.Pair., 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

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

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

m n. Number.Natural.< m n Number.Natural.≤ 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

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

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

p q r. p q r p q r

m n p.
    Number.Natural.+ m (Number.Natural.+ n p) =
    Number.Natural.+ (Number.Natural.+ m n) p

m n p. Number.Natural.+ m n = Number.Natural.+ m p n = p

m n p.
    Number.Natural.< m n Number.Natural.< n p Number.Natural.< m p

m n p.
    Number.Natural.≤ m n Number.Natural.< n p Number.Natural.< m p

m n p.
    Number.Natural.≤ m n Number.Natural.≤ n p Number.Natural.≤ m p

s t. s = t x. x s x t

s t. s t x. x s x t

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

m n.
    Number.Natural.< n m
    Number.Natural.suc (Number.Natural.- m (Number.Natural.suc n)) =
    Number.Natural.- 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

P. P 0 (n. P n P (Number.Natural.suc n)) n. P n

(t. ¬¬t t) (¬T F) (¬F T)

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

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

(n. Number.Natural.+ 0 n = n)
  m n.
    Number.Natural.+ (Number.Natural.suc m) n =
    Number.Natural.suc (Number.Natural.+ m n)

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

(n. Number.Natural.* 0 n = 0)
  m n.
    Number.Natural.* (Number.Natural.suc m) n =
    Number.Natural.+ (Number.Natural.* m n) n

x y a b. Data.Pair., x y = Data.Pair., a b x = a y = b

x y s t. Data.Pair., x y cross s t x s y t

m n p q.
    Number.Natural.≤ m p Number.Natural.≤ n q
    Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ p q)

(m. Number.Natural.exp m 0 = 1)
  m n.
    Number.Natural.exp m (Number.Natural.suc n) =
    Number.Natural.* m (Number.Natural.exp m n)

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

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

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

(m. Number.Natural.< m 0 F)
  m n.
    Number.Natural.< m (Number.Natural.suc n)
    m = n Number.Natural.< m n

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

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

n.
    { m. m | Number.Natural.< m (Number.Natural.suc n) } =
    insert n { m. m | Number.Natural.< m n }

(m. Number.Natural.≤ m 0 m = 0)
  m n.
    Number.Natural.≤ m (Number.Natural.suc n)
    m = Number.Natural.suc n Number.Natural.≤ m n

P a b. Data.Pair., a b { x y. Data.Pair., x y | P x y } P a b

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

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

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

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

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)

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

(n. Number.Natural.+ 0 n = n) (m. Number.Natural.+ m 0 = m)
  (m n.
     Number.Natural.+ (Number.Natural.suc m) n =
     Number.Natural.suc (Number.Natural.+ m n))
  m n.
    Number.Natural.+ m (Number.Natural.suc n) =
    Number.Natural.suc (Number.Natural.+ m n)

s t a.
    { x y. Data.Pair., x y | x insert a s y t x } =
    image (Data.Pair., a) (t a)
    { x y. Data.Pair., 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) }

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

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

(n. Number.Natural.* 0 n = 0) (m. Number.Natural.* m 0 = 0)
  (n. Number.Natural.* 1 n = n) (m. Number.Natural.* m 1 = m)
  (m n.
     Number.Natural.* (Number.Natural.suc m) n =
     Number.Natural.+ (Number.Natural.* m n) n)
  m n.
    Number.Natural.* m (Number.Natural.suc n) =
    Number.Natural.+ m (Number.Natural.* m n)

d a s t.
    { f. f |
      (x. x insert a s f x t) x. ¬(x insert a s) f x = d } =
    image (λ(Data.Pair., 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 })