Package set-size-thm: set-size-thm

Information

nameset-size-thm
version1.12
descriptionset-size-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-25
showData.Bool

Files

Theorems

Set.size Set.∅ = 0

Set.hasSize Set.universe 2

x. Set.hasSize (Set.insert x Set.∅) 1

x. Set.size (Set.insert x Set.∅) = 1

s. Set.finite s Set.hasSize s (Set.size s)

s. Set.hasSize s 0 s = Set.∅

s n. Set.hasSize s n Set.size s = n

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

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

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

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

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

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

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

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

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

s t.
    Set.finite s Set.finite t
    Number.Natural.≤ (Set.size (Set.∪ s t))
      (Number.Natural.+ (Set.size s) (Set.size t))

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

a b. Set.finite b Set.⊆ a b Set.size a = Set.size b a = b

a b.
    Set.finite b Set.⊆ a b Number.Natural.≤ (Set.size b) (Set.size a)
    a = b

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

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

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

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

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

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

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

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

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

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

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

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

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

s t.
    Set.finite s Set.finite t
    Number.Natural.+ (Set.size (Set.∪ s t)) (Set.size (Set.∩ s t)) =
    Number.Natural.+ (Set.size s) (Set.size t)

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

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

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

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

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

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

s t.
    Set.finite s Set.finite t
    Set.size { x y. Data.Pair., x y | Set.∈ x s Set.∈ y t } =
    Number.Natural.* (Set.size s) (Set.size t)

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

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

P.
    P Set.∅
    (s.
       Set.finite s ¬(s = Set.∅)
       x. Set.∈ x s (P (Set.delete s x) P s)) s. Set.finite s P s

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

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

(s. Set.hasSize s 0 s = Set.∅)
  s n.
    Set.hasSize s (Number.Natural.suc n)
    a t. Set.hasSize t n ¬Set.∈ a t s = Set.insert a t

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

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

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

s t.
    Set.finite s Set.finite t
    Number.Natural.≤ (Set.size s) (Set.size t)
    f.
      Set.⊆ (Set.image f s) t
      x y. Set.∈ x s Set.∈ y s f x = f y x = y

s t m n.
    Set.hasSize s m
    (x.
       Set.∈ x s
       Set.finite (t x) Number.Natural.≤ (Set.size (t x)) n)
    Number.Natural.≤ (Set.size (Set.bigUnion { x. t x | Set.∈ x s }))
      (Number.Natural.* m n)

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

d s t.
    Set.finite s Set.finite t
    Set.size
      { f. f |
        (x. Set.∈ x s Set.∈ (f x) t) x. ¬Set.∈ x s f x = d } =
    Number.Natural.exp (Set.size t) (Set.size s)

d s t m n.
    Set.hasSize s m Set.hasSize t n
    Set.hasSize
      { f. f | (x. Set.∈ x s Set.∈ (f x) t) x. ¬Set.∈ x s f x = d }
      (Number.Natural.exp n m)

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

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

s f.
    Set.finite s Set.⊆ (Set.image f s) s
    ((y. Set.∈ y s x. Set.∈ x s f x = y)
     x y. Set.∈ x s Set.∈ y s f x = f y x = y)

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

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

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

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

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

Input Type Operators

Input Constants

Assumptions

T

Set.finite Set.∅

Set.bigUnion Set.∅ = Set.∅

n. Number.Natural.≤ 0 n

n. Number.Natural.≤ n n

s. Set.⊆ Set.∅ s

s. Set.⊆ s s

F p. p

1 = Number.Natural.suc 0

x. ¬Set.∈ x Set.∅

a. Set.finite (Set.insert a Set.∅)

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

Set.universe = Set.insert T (Set.insert F Set.∅)

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

s t. Set.disjoint s (Set.- 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. ¬(Set.insert x s = Set.∅)

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. Set.finite (Set.delete s x) Set.finite s

s x. Set.finite (Set.insert x s) Set.finite s

s t. Set.finite s Set.finite (Set.- s t)

s t. Set.∪ s t = Set.∪ t s

f s. Set.finite s Set.finite (Set.image f s)

p x. Set.∈ x (Set.fromPredicate p) p x

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

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. Set.∈ x s) ¬(s = Set.∅)

() = λ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. Set.disjoint s t Set.∩ s t = Set.∅

s t. Set.⊆ s t Set.∪ s t = t

s t. Set.- s t = Set.∅ Set.⊆ s t

s t. Set.- s t = s Set.disjoint s t

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

s t. Set.∪ (Set.- s t) t = Set.∪ s t

s t. Set.finite t Set.⊆ s t Set.finite s

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

{ m. m | Number.Natural.< m 0 } = Set.∅

x s. Set.delete s x = s ¬Set.∈ x s

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

s t. Set.finite (Set.∪ s t) Set.finite s Set.finite t

s t. Set.finite s Set.finite t Set.finite (Set.∩ 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. Set.⊆ s t Set.⊆ s (Set.insert x t)

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

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

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

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

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

s t. Set.∪ s (Set.- t s) = t Set.⊆ s t

s t. Set.⊆ s t Set.⊆ t s s = t

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

(s. Set.∪ Set.∅ s = s) s. Set.∪ s Set.∅ = s

f s x. Set.∈ x s Set.∈ (f x) (Set.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. Set.⊂ s t Set.⊆ 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. Set.bigUnion s = Set.∅ t. Set.∈ t s t = Set.∅

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

s t. Set.⊆ s t x. Set.∈ x s Set.∈ 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.
    Set.finite s
    (Set.finite (Set.bigUnion s) t. Set.∈ t s Set.finite t)

s t. Set.disjoint s (Set.bigUnion t) x. Set.∈ x t Set.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. Set.∈ x { y. y | p y } p x

x y s. Set.∈ x (Set.insert y s) x = y Set.∈ x s

x s t. Set.⊆ (Set.insert x s) t Set.∈ x t Set.⊆ s t

s t x. Set.∈ x (Set.∩ s t) Set.∈ x s Set.∈ x t

s t x. Set.∈ x (Set.∪ s t) Set.∈ x s Set.∈ x t

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

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

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

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

s t x. Set.∈ x (Set.- s t) Set.∈ x s ¬Set.∈ x t

s. s = Set.∅ x t. s = Set.insert x t ¬Set.∈ 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. Set.∈ y (Set.image f s) x. y = f x Set.∈ 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. Set.∈ (Data.Pair., x y) (Set.cross s t) Set.∈ x s Set.∈ 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 | Set.∈ x Set.∅ Set.∈ y (t x) } = Set.∅

x s t.
    Set.∪ (Set.insert x s) t =
    if Set.∈ x t then Set.∪ s t else Set.insert x (Set.∪ s t)

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

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

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

n.
    { m. m | Number.Natural.< m (Number.Natural.suc n) } =
    Set.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. Set.∈ (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 Set.∅
    (x s. P s ¬Set.∈ x s Set.finite s P (Set.insert x s))
    s. Set.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. Set.∈ x s Set.∈ y s f x = f y x = y)
    (Set.finite (Set.image f s) Set.finite s)

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

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

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

s.
    { t. t | Set.⊆ t s } =
    Set.image (λp. { x. x | p x })
      { p. p |
        (x. Set.∈ x s Set.∈ (p x) Set.universe)
        x. ¬Set.∈ 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))
    Set.fold f Set.∅ b = b
    x s.
      Set.finite s
      Set.fold f (Set.insert x s) b =
      if Set.∈ x s then Set.fold f s b else f x (Set.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. Set.∈ x (Set.insert a s) Set.∈ (f x) t)
      x. ¬Set.∈ x (Set.insert a s) f x = d } =
    Set.image (λ(Data.Pair., b g) x. if x = a then b else g x)
      (Set.cross t
         { f. f |
           (x. Set.∈ x s Set.∈ (f x) t) x. ¬Set.∈ x s f x = d })