:: Stirling Numbers of the Second Kind
::  by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005-2021 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
  n<k implies n block k = 0;

theorem :: STIRL2_1:30
  n block 0 = 1 iff n=0;

theorem :: STIRL2_1:31
  n<>0 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<j holds min* f
  "{i} < min* f"{j};

theorem :: STIRL2_1:37
  for f be Function of Segm(n+1),Segm(k+1)
   st f is onto "increasing & f"{f.n}= {n} holds rng (f|n) c= Segm k &
  for g be Function of Segm n,Segm k st g=f|n holds g is onto
  "increasing;

theorem :: STIRL2_1:38
  for f be Function of Segm(n+1),Segm k,
      g be Function of Segm n,Segm k st f is onto
  "increasing & f"{f.n}<>{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<j holds min* g
  "{i} < min* g"{j};

theorem :: STIRL2_1:40
  for f be Function of Segm n,Segm k,
      g be Function of Segm(n+1),Segm(k+1) st f is onto
  "increasing & f=g|Segm n & g.n = k
  holds g is onto "increasing & g"{g.n}={n};

theorem :: STIRL2_1:41
  for f be Function of Segm n,Segm k,
      g be Function of Segm(n+1),Segm k st f is onto
  "increasing & f=g|Segm n & g.n < k holds g is onto "increasing & g"{g.n}<>{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<k holds card{f where f is Function of Segm(n+1),Segm k: f is
    onto "increasing & f"{f.n}<>{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 & n<k
  holds Order.n < Order.k;

::$CT


theorem :: STIRL2_1:61
  for F,G be Function,y st y in rng (G*F) & G is one-to-one holds
  ex x st x in dom G & x in rng F & G"{y}={x} & F"{x}=(G*F)"{y};

definition
  let Ne,Ke;
  let f be Function of Ne,Ke;
  attr f is 'increasing means
:: STIRL2_1:def 3

  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:62
  for F be Function of Ne,Ke st F is 'increasing holds min* rng F= F.min* dom F
;

:: existence of an expansion

theorem :: STIRL2_1:63
  for F be Function of Ne,Ke st rng F is finite ex I be Function of Ne,
  Ke,P be Permutation of rng F st F=P*I & rng F=rng I & I is 'increasing;

:: uniqueness of expansion

theorem :: STIRL2_1:64
  for F be Function of Ne,Ke st rng F is finite for I1,I2 be
  Function of Ne,Me,P1,P2 be Function st P1 is one-to-one & P2 is one-to-one &
  rng I1=rng I2 & rng I1=dom P1 & dom P1=dom P2 & F=P1*I1 & F=P2*I2 & I1 is
  'increasing & I2 is 'increasing holds P1=P2 & I1=I2;

theorem :: STIRL2_1:65
  for F be Function of Ne,Ke st rng F is finite for I1,I2 be Function of
Ne,Ke, P1,P2 be Permutation of rng F st F=P1*I1 & F=P2*I2 & rng F=rng I1 & rng
  F=rng I2 & I1 is 'increasing & I2 is 'increasing holds P1=P2 & I1=I2;

::$N Stirling numbers of the second kind
theorem :: STIRL2_1:66
  for D be non empty set, F be XFinSequence of D st
  (for i st i in dom F holds F.i is finite) &
  (for i,j st i in dom F & j in dom F & i<>j 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);