:: Stirling Numbers of the Second Kind
:: by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_0, NAT_1, ORDINAL1, CARD_1,
TARSKI, ARYTM_3, ARYTM_1, FUNCT_1, RELAT_1, FUNCT_2, INT_1, FINSET_1,
AFINSQ_1, FINSEQ_1, FINSOP_1, CARD_3, BINOP_2, ZFMISC_1, NEWTON,
REALSET1, STIRL2_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
RELAT_1, FUNCT_1, RELSET_1, SEQ_4, PARTFUN1, FINSET_1, AFINSQ_1,
AFINSQ_2, XXREAL_0, XCMPLX_0, FUNCT_2, INT_1, NAT_1, BINOP_1, BINOP_2,
NEWTON, DOMAIN_1;
constructors WELLORD2, DOMAIN_1, SETWISEO, REAL_1, BINOP_2, SEQ_4, NEWTON,
AFINSQ_2, RELSET_1, PARTFUN3, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, AFINSQ_1,
CARD_1, VALUED_0, XXREAL_2, RELSET_1, AFINSQ_2, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve k, l, m, n, i, j for Nat,
K, N for non empty Subset of NAT,
Ke, Ne, Me for Subset of NAT,
X,Y for set;
theorem :: STIRL2_1:1
min N = min* N;
theorem :: STIRL2_1:2
min(min K,min N) = min(K\/N);
theorem :: STIRL2_1:3
min(min* Ke,min* Ne) <= min* (Ke\/Ne);
theorem :: STIRL2_1:4
not min* Ne in Ne/\Ke implies min* Ne = min* (Ne\Ke);
theorem :: STIRL2_1:5
for n be Element of NAT holds min* {n} = n & min {n} = n;
theorem :: STIRL2_1:6
for n,k be Element of NAT holds min* {n,k} = min(n,k) & min {n,k} = min(n,k);
theorem :: STIRL2_1:7
for n,k,l be Element of NAT holds min* {n,k,l} = min(n,min(k,l));
theorem :: STIRL2_1:8
n is Subset of NAT;
registration
let n;
cluster -> natural for Element of Segm n;
end;
theorem :: STIRL2_1:9
N c= n implies n-1 is Element of NAT;
theorem :: STIRL2_1:10
k in Segm n implies k<=n-1 & n-1 is Element of NAT;
theorem :: STIRL2_1:11
min* n = 0;
theorem :: STIRL2_1:12
N c= Segm n implies min* N <= n-1;
theorem :: STIRL2_1:13
N c= Segm n & N <> {n-1} implies min* N < n-1;
theorem :: STIRL2_1:14
Ne c= Segm n & n>0 implies min* Ne <= n-1;
reserve f for Function of Segm n,Segm k;
definition
let n,X;
let f be Function of Segm n,X;
let x be set;
redefine func f"x -> Subset of NAT;
end;
definition
let X,k;
let f be Function of X, Segm k;
let x be object;
redefine func f.x -> Element of Segm k;
end;
definition
let n,k be Nat;
let f be Function of Segm n,Segm k;
attr f is "increasing means
:: STIRL2_1:def 1
(n = 0 iff k = 0) & for l,m st l in rng f
& m in rng f & l < m holds min* f"{l} < min* f"{m};
end;
theorem :: STIRL2_1:15
n=0 & k=0 implies f is onto "increasing;
theorem :: STIRL2_1:16
n>0 implies min* f"{m} <= n-1;
theorem :: STIRL2_1:17
f is onto implies n>=k;
theorem :: STIRL2_1:18
f is onto "increasing implies for m st m < k holds m <= min* f"{ m};
theorem :: STIRL2_1:19
f is onto "increasing implies for m st m < k holds min* f"{m} <= n-k+m;
theorem :: STIRL2_1:20
f is onto "increasing & n = k implies f = id n;
theorem :: STIRL2_1:21
f = id n & n > 0 implies f is "increasing;
theorem :: STIRL2_1:22
(n=0 iff k=0) implies
ex f be Function of Segm n, Segm k st f is "increasing;
theorem :: STIRL2_1:23
(n=0 iff k=0) & n>=k implies
ex f be Function of Segm n,Segm k st f is onto "increasing;
scheme :: STIRL2_1:sch 1
:: uogolnic na skonczone zbiory, a moze gdzies jest ??? !!!
Sch1{n,k() -> Nat,P[set]}:
{f where f is Function of Segm n(),Segm k():P[f]} is finite;
theorem :: STIRL2_1:24
for n,k holds
{f where f is Function of Segm n,Segm k:f is onto "increasing} is finite;
theorem :: STIRL2_1:25
for n,k holds
card {f where f is Function of Segm n,Segm k:f is onto "increasing}
is Element of NAT;
:: Stirling Numbers of the second kind
definition
let n,k be Nat;
func n block k -> set equals
:: STIRL2_1:def 2
card {f where f is Function of Segm n,Segm k:f is onto "increasing};
end;
registration
let n,k be Nat;
cluster n block k -> natural;
end;
theorem :: STIRL2_1:26
n block n = 1;
theorem :: STIRL2_1:27
k<>0 implies 0 block k = 0;
theorem :: STIRL2_1:28
0 block k = 1 iff k=0;
theorem :: STIRL2_1:29
n0 implies n block 0 = 0;
theorem :: STIRL2_1:32
n<>0 implies n block 1 = 1;
theorem :: STIRL2_1:33
1<=k & k <=n or k=n iff n block k qua Nat > 0;
reserve x,y for set;
scheme :: STIRL2_1:sch 2
Sch2{X,Y,X1,Y1()->set,f()->Function of X(),Y(),F(object)->object}:
ex h be
Function of X1(),Y1() st h|X() = f() & for x st x in X1()\X() holds h.x = F(x)
provided
for x st x in X1()\X() holds F(x) in Y1() and
X() c= X1() & Y() c= Y1() and
Y() is empty implies X() is empty;
scheme :: STIRL2_1:sch 3
Sch3{X,Y,X1,Y1()->set,F(object)->object,P[set,set,set]}:
card{f where f is Function of X(),Y(): P[f,X(),Y()]}
= card{f where f is Function of X1(),Y1():
P[f,X1(),Y1()]& rng (f|X()) c=Y()&
(for x st x in X1()\X() holds f.x=F(x))}
provided
for x st x in X1()\X() holds F(x) in Y1() and
X() c= X1() & Y() c= Y1() and
Y() is empty implies X() is empty and
for f be Function of X1(),Y1() st (for x st x in X1()\X() holds F(x)
=f.x) holds P[f,X1(),Y1()] iff P[f|X(),X(),Y()];
scheme :: STIRL2_1:sch 4
Sch4{X,Y()->set, x,y()->object,P[set,set,set]}:
card{f where f is Function of X(),Y(): P[f,X(),Y()]}
= card{f where f is Function of (X()\/{x()}),(Y()\/{y()}): P[f,X()
\/{x()},Y()\/{y()}] & rng (f|X()) c=Y() & f.x()=y()}
provided
Y() is empty implies X() is empty and
not x() in X() and
for f be Function of X()\/{x()},Y()\/{y()} st f.x()=y() holds P[f,X(
)\/{x()},Y()\/{y()}] iff P[f|X(),X(),Y()];
theorem :: STIRL2_1:34
for f be Function of Segm(n+1),Segm(k+1)
st f is onto "increasing & f"{f.n}=
{n} holds f.n=k;
theorem :: STIRL2_1:35
for f be Function of Segm(n+1),Segm k st k<>0 & f"{f.n}<>{n}
ex m st m in f"{f.n} & m<>n;
theorem :: STIRL2_1:36
for f be Function of Segm n, Segm k,
g be Function of Segm(n+m),Segm(k+l) st g is
"increasing & f=g|n holds for i,j st i in rng f & j in rng f & i{n} & f|n =g holds g is onto "increasing;
theorem :: STIRL2_1:39
for f be Function of Segm n,Segm k, g be Function of Segm(n+1),Segm(k+m)
st f is onto
"increasing & f=g|n holds for i,j st i in rng g & j in rng g & i{n}
;
theorem :: STIRL2_1:42
card{f where f is Function of Segm(n+1),Segm(k+1):
f is onto "increasing & f
"{f.n}={n}}=
card{f where f is Function of Segm n,Segm k: f is onto "increasing};
theorem :: STIRL2_1:43
for l st l{n} & f.n=l}
= card{f where f is Function of Segm n,Segm k: f is onto "increasing};
theorem :: STIRL2_1:44
for f be Function, n holds union (rng (f|n)) \/ f.n=union rng (f |(n+1));
scheme :: STIRL2_1:sch 5
Sch6{D()->non empty set,n()->Nat,P[object,object]}:
ex p be XFinSequence of D() st dom p = Segm n() &
for k st k in Segm n() holds P[k,p.k]
provided
for k st k in Segm n() ex x be Element of D() st P[k,x];
scheme :: STIRL2_1:sch 6
Sch8{X,Y()->finite set,x()->set,P[set],f()->Function of card Y(),Y()}:
ex F be XFinSequence of NAT st dom F = card Y() &
card{g where g is Function of X(),Y():P[g]} = Sum(F) &
for i st i in dom F holds F.i = card{g where g is Function
of X(),Y(): P[g] & g.x()=f().i}
provided
f() is onto one-to-one and
Y() is non empty and
x() in X();
theorem :: STIRL2_1:45
k * (n block k)= card{f where f is
Function of Segm(n+1),Segm k: f is onto "increasing & f"{f.n}<>{n}};
:: Recursive dependence
theorem :: STIRL2_1:46
(n+1) block (k+1) = (k+1)*(n block (k+1) ) + (n block k);
theorem :: STIRL2_1:47
n>=1 implies n block 2 = 1/2 * (2 |^ n - 2 );
theorem :: STIRL2_1:48
n >= 2 implies n block 3 = 1/6 * ( 3 |^ n - 3 * 2 |^ n + 3 );
theorem :: STIRL2_1:49
n >= 3 implies n block 4 = 1/24 * ( 4 |^ n - 4 * 3 |^ n + 6* 2|^ n - 4 );
theorem :: STIRL2_1:50
3! = 6 & 4! = 24;
theorem :: STIRL2_1:51
n choose 1=n & n choose 2=n*(n-1)/2 & n choose 3=n*(n-1)*(n-2)/6
& n choose 4=n*(n-1)*(n-2)*(n-3)/24;
theorem :: STIRL2_1:52
(n + 1) block n = (n + 1) choose 2;
theorem :: STIRL2_1:53
(n + 2) block n = 3*((n + 2) choose 4) + ((n + 2) choose 3);
theorem :: STIRL2_1:54
for F be Function,y holds rng (F|(dom F\F"{y}))=rng F\{y} & for
x st x<>y holds (F|(dom F\F"{y}))"{x}=F"{x};
theorem :: STIRL2_1:55
card X=k+1 & x in X implies card (X\{x})=k;
scheme :: STIRL2_1:sch 7
Sch9{P[set],Q[set,Function]}: for F be Function st rng F is finite holds P[F
]
provided
P[{}] and
for F be Function st for x st x in rng F & Q[x,F] holds P[F|(dom F\F
"{x})] holds P[F];
theorem :: STIRL2_1:56
for N be Subset of NAT st N is finite ex k st for n st n in N holds n<=k;
theorem :: STIRL2_1:57
for X,Y for x,y being object
st (Y is empty implies X is empty) & not x in X
for
F be Function of X,Y ex G be Function of X\/{x},Y\/{y} st G|X = F & G.x=y;
theorem :: STIRL2_1:58
for X,Y,x,y st (Y is empty implies X is empty) for F be Function
of X,Y,G be Function of X\/{x},Y\/{y} st G|X=F & G.x=y holds ( F is onto
implies G is onto) & ( not y in Y & F is one-to-one implies G is one-to-one);
theorem :: STIRL2_1:59
for N be finite Subset of NAT
ex Order be Function of N, Segm card N
st Order is bijective & for n,k st n in dom Order & k in dom Order & nj holds F.i misses F.j)
ex CardF be XFinSequence of NAT st dom CardF = dom F &
(for i st i in dom CardF holds CardF.i=card (F.i)) &
card union rng F = Sum(CardF);