:: Stirling Numbers of the Second Kind
:: by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: STIRL2_1:1
theorem Th2: :: STIRL2_1:2
theorem :: STIRL2_1:3
theorem :: STIRL2_1:4
theorem Th5: :: STIRL2_1:5
theorem Th6: :: STIRL2_1:6
theorem :: STIRL2_1:7
theorem Th8: :: STIRL2_1:8
theorem :: STIRL2_1:9
theorem Th10: :: STIRL2_1:10
theorem :: STIRL2_1:11
theorem Th12: :: STIRL2_1:12
theorem :: STIRL2_1:13
theorem Th14: :: STIRL2_1:14
:: deftheorem Def1 defines "increasing STIRL2_1:def 1 :
theorem Th15: :: STIRL2_1:15
theorem Th16: :: STIRL2_1:16
theorem Th17: :: STIRL2_1:17
theorem Th18: :: STIRL2_1:18
theorem Th19: :: STIRL2_1:19
theorem Th20: :: STIRL2_1:20
theorem :: STIRL2_1:21
theorem :: STIRL2_1:22
theorem Th23: :: STIRL2_1:23
theorem Th24: :: STIRL2_1:24
theorem Th25: :: STIRL2_1:25
:: deftheorem defines block STIRL2_1:def 2 :
theorem Th26: :: STIRL2_1:26
theorem Th27: :: STIRL2_1:27
theorem :: STIRL2_1:28
theorem Th29: :: STIRL2_1:29
theorem :: STIRL2_1:30
theorem Th31: :: STIRL2_1:31
theorem Th32: :: STIRL2_1:32
theorem :: STIRL2_1:33
scheme :: STIRL2_1:sch 3
Sch3{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5(
set )
-> set ,
P1[
set ,
set ,
set ] } :
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) }
provided
A1:
for
x being
set st
x in F3()
\ F1() holds
F5(
x)
in F4()
and A2:
(
F1()
c= F3() &
F2()
c= F4() )
and A3:
(
F2() is
empty implies
F1() is
empty )
and A4:
for
f being
Function of
F3(),
F4() st ( for
x being
set st
x in F3()
\ F1() holds
F5(
x)
= f . x ) holds
(
P1[
f,
F3(),
F4()] iff
P1[
f | F1(),
F1(),
F2()] )
scheme :: STIRL2_1:sch 4
Sch4{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
P1[
set ,
set ,
set ] } :
provided
A1:
(
F2() is
empty implies
F1() is
empty )
and A2:
not
F3()
in F1()
and A3:
for
f being
Function of
F1()
\/ {F3()},
F2()
\/ {F4()} st
f . F3()
= F4() holds
(
P1[
f,
F1()
\/ {F3()},
F2()
\/ {F4()}] iff
P1[
f | F1(),
F1(),
F2()] )
theorem Th34: :: STIRL2_1:34
theorem Th35: :: STIRL2_1:35
theorem Th36: :: STIRL2_1:36
theorem Th37: :: STIRL2_1:37
theorem Th38: :: STIRL2_1:38
theorem Th39: :: STIRL2_1:39
theorem Th40: :: STIRL2_1:40
theorem Th41: :: STIRL2_1:41
Lm1:
for k, n being Element of NAT st k < n holds
n \/ {k} = n
theorem Th42: :: STIRL2_1:42
theorem Th43: :: STIRL2_1:43
:: deftheorem Def3 defines "**" STIRL2_1:def 3 :
theorem Th44: :: STIRL2_1:44
theorem Th45: :: STIRL2_1:45
theorem Th46: :: STIRL2_1:46
theorem :: STIRL2_1:47
theorem :: STIRL2_1:48
theorem :: STIRL2_1:49
:: deftheorem defines Sum STIRL2_1:def 4 :
theorem Th50: :: STIRL2_1:50
theorem Th51: :: STIRL2_1:51
theorem Th52: :: STIRL2_1:52
theorem :: STIRL2_1:53
theorem Th54: :: STIRL2_1:54
theorem Th55: :: STIRL2_1:55
theorem Th56: :: STIRL2_1:56
theorem Th57: :: STIRL2_1:57
theorem Th58: :: STIRL2_1:58
Lm2:
for n being Element of NAT holds n |^ 3 = (n * n) * n
theorem :: STIRL2_1:59
theorem Th60: :: STIRL2_1:60
theorem Th61: :: STIRL2_1:61
theorem Th62: :: STIRL2_1:62
theorem :: STIRL2_1:63
theorem Th64: :: STIRL2_1:64
theorem Th65: :: STIRL2_1:65
theorem Th66: :: STIRL2_1:66
theorem Th67: :: STIRL2_1:67
theorem Th68: :: STIRL2_1:68
theorem Th69: :: STIRL2_1:69
Lm3:
for X being finite set
for x being set st x in X holds
card (X \ {x}) < card X
theorem Th70: :: STIRL2_1:70
Lm4:
for n being Element of NAT
for N being finite Subset of NAT
for F being Function of N, card N st n in N & F is bijective & ( for n, k being Element of NAT st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
for k being Element of NAT st k in N holds
( ( k < n implies P . k = (F " ) . ((F . k) + 1) ) & ( k = n implies P . k = (F " ) . 0 ) & ( k > n implies P . k = k ) )
theorem Th71: :: STIRL2_1:71
:: deftheorem Def5 defines "increasing STIRL2_1:def 5 :
theorem Th72: :: STIRL2_1:72
theorem :: STIRL2_1:73
theorem Th74: :: STIRL2_1:74
theorem :: STIRL2_1:75