Package set-finite-thm: set-finite-thm

Information

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

Files

Theorems

Set.finite Set.∅

Set.finite Set.universe

Set.infinite Set.universe

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

s. Set.infinite s ¬(s = Set.∅)

s x. Set.finite s Set.finite (Set.delete s x)

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. Set.finite s a. ¬Set.∈ a s

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

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

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

n. Set.finite { m. 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)

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

s t. Set.finite s Set.finite t Set.finite (Set.∩ s t)

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

s. Set.finite s a. x. Set.∈ x s Number.Natural.≤ x a

s. Set.finite s Set.finite { t. t | Set.⊆ t s }

s.
    Set.finite s
    (Set.finite (Set.bigUnion s) t. Set.∈ t s Set.finite t)

s.
    Set.finite (Set.bigUnion s)
    Set.finite s t. Set.∈ t s Set.finite t

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

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

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

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

f s t.
    Set.finite t Set.⊆ t (Set.image f s)
    s'. Set.finite s' Set.⊆ s' s t = Set.image f s'

f s t.
    Set.finite t Set.⊆ t (Set.image f s)
    s'. Set.finite s' Set.⊆ s' s Set.⊆ t (Set.image f s')

s t.
    Set.finite s Set.finite t
    Set.finite { x y. Data.Pair., x y | Set.∈ x s Set.∈ y 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

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

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

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

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

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

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

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

Input Type Operators

Input Constants

Assumptions

T

Set.bigUnion Set.∅ = Set.∅

x. Set.∈ x Set.universe

s. Set.⊆ s s

F p. p

Set.fromPredicate (λx. F) = Set.∅

x. ¬Set.∈ x Set.∅

t. t ¬t

(~) = λp. p F

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

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

x. x = x T

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

s. Set.infinite s ¬Set.finite s

x s. Set.⊆ (Set.delete s x) s

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

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

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

() = λp q. p q p

t. (t T) (t F)

s. Set.⊆ s Set.∅ s = Set.∅

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

(¬T F) (¬F T)

a b. (a b) a b

p x. Set.∈ x (Set.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

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

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

x s. Set.∈ x s Set.insert x s = s

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

t1 t2. ¬t1 ¬t2 t2 t1

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

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

f g x. Function.o f g x = f (g x)

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

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

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

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

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

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

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

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

p q r. p q r p q r

p q r. p q r p q r

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

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

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

s t. s = t x. Set.∈ x s Set.∈ x t

s t. Set.⊆ s t x. Set.∈ x s Set.∈ x t

f s t. Set.⊆ s t Set.⊆ (Set.image f s) (Set.image f t)

f g s. Set.image (Function.o f g) s = Set.image f (Set.image g s)

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

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

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

p x. Set.∈ x { y. y | p y } p x

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

(s t. Set.⊆ (Set.∩ s t) s) s t. Set.⊆ (Set.∩ t s) s

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

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

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

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.∅

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

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

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

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

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

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 }

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)

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)

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.∅

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

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

(P f Q. (z. Set.∈ z { x. f x | P x } Q z) x. P x Q (f x))
  (P f Q.
     (z. Set.∈ z { x y. f x y | P x y } Q z)
     x y. P x y Q (f x y))
  P f Q.
    (z. Set.∈ z { w x y. f w x y | P w x y } Q z)
    w x y. P w x y Q (f w x y)