:: by Cezary Kaliszyk

::

:: Received February 23, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

registration
end;

theorem Th5: :: CARDFIN2:5

for n being Nat

for a, b being Real st a < b holds

ex c being Real st

( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )

for a, b being Real st a < b holds

ex c being Real st

( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )

proof end;

theorem Th6: :: CARDFIN2:6

for n being positive Nat

for c being Real st c < 0 holds

|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2

for c being Real st c < 0 holds

|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2

proof end;

definition

let s be set ;

{ f where f is Permutation of s : f is without_fixpoints } is set ;

end;
func derangements s -> set equals :: CARDFIN2:def 2

{ f where f is Permutation of s : f is without_fixpoints } ;

coherence { f where f is Permutation of s : f is without_fixpoints } ;

{ f where f is Permutation of s : f is without_fixpoints } is set ;

:: deftheorem defines derangements CARDFIN2:def 2 :

for s being set holds derangements s = { f where f is Permutation of s : f is without_fixpoints } ;

for s being set holds derangements s = { f where f is Permutation of s : f is without_fixpoints } ;

theorem Th7: :: CARDFIN2:7

for s being finite set holds derangements s = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds

h . x <> x ) ) }

h . x <> x ) ) }

proof end;

theorem Th8: :: CARDFIN2:8

for s being non empty finite set ex c being Real st

( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )

( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )

proof end;

theorem Th9: :: CARDFIN2:9

for s being non empty finite set holds |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2

proof end;

reconsider j = 1, z = 0 as Element of INT by INT_1:def 2;

deffunc H

definition

ex b_{1} being sequence of INT st

( b_{1} . 0 = 1 & b_{1} . 1 = 0 & ( for n being Nat holds b_{1} . (n + 2) = (n + 1) * ((b_{1} . n) + (b_{1} . (n + 1))) ) )

for b_{1}, b_{2} being sequence of INT st b_{1} . 0 = 1 & b_{1} . 1 = 0 & ( for n being Nat holds b_{1} . (n + 2) = (n + 1) * ((b_{1} . n) + (b_{1} . (n + 1))) ) & b_{2} . 0 = 1 & b_{2} . 1 = 0 & ( for n being Nat holds b_{2} . (n + 2) = (n + 1) * ((b_{2} . n) + (b_{2} . (n + 1))) ) holds

b_{1} = b_{2}
end;

func der_seq -> sequence of INT means :Def3: :: CARDFIN2:def 3

( it . 0 = 1 & it . 1 = 0 & ( for n being Nat holds it . (n + 2) = (n + 1) * ((it . n) + (it . (n + 1))) ) );

existence ( it . 0 = 1 & it . 1 = 0 & ( for n being Nat holds it . (n + 2) = (n + 1) * ((it . n) + (it . (n + 1))) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines der_seq CARDFIN2:def 3 :

for b_{1} being sequence of INT holds

( b_{1} = der_seq iff ( b_{1} . 0 = 1 & b_{1} . 1 = 0 & ( for n being Nat holds b_{1} . (n + 2) = (n + 1) * ((b_{1} . n) + (b_{1} . (n + 1))) ) ) );

for b

( b

registration

let c be Integer;

let F be XFinSequence of INT ;

coherence

( c (#) F is finite & c (#) F is INT -valued & c (#) F is Sequence-like ) ;

end;
let F be XFinSequence of INT ;

coherence

( c (#) F is finite & c (#) F is INT -valued & c (#) F is Sequence-like ) ;

registration
end;

theorem :: CARDFIN2:13

for F being XFinSequence of INT

for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))

for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))

proof end;

theorem Th14: :: CARDFIN2:14

for X, N being XFinSequence of INT st len N = (len X) + 1 holds

for c being Integer st N | (len X) = c (#) X holds

Sum N = (c * (Sum X)) + (N . (len X))

for c being Integer st N | (len X) = c (#) X holds

Sum N = (c * (Sum X)) + (N . (len X))

proof end;

definition

let s, t be set ;

{ f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t))

end;
func not-one-to-one (s,t) -> Subset of (Funcs (s,t)) equals :: CARDFIN2:def 4

{ f where f is Function of s,t : not f is one-to-one } ;

coherence { f where f is Function of s,t : not f is one-to-one } ;

{ f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t))

proof end;

:: deftheorem defines not-one-to-one CARDFIN2:def 4 :

for s, t being set holds not-one-to-one (s,t) = { f where f is Function of s,t : not f is one-to-one } ;

for s, t being set holds not-one-to-one (s,t) = { f where f is Function of s,t : not f is one-to-one } ;

theorem Th16: :: CARDFIN2:16

for s, t being finite set st card s <= card t holds

card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))

card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))

proof end;

Lm1: 2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23

proof end;

theorem Th17: :: CARDFIN2:17

for s being finite set

for t being non empty finite set st card s = 23 & card t = 365 holds

2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))

for t being non empty finite set st card s = 23 & card t = 365 holds

2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))

proof end;

theorem :: CARDFIN2:18

for s, t being non empty finite set st card s = 23 & card t = 365 holds

prob (not-one-to-one (s,t)) > 1 / 2

prob (not-one-to-one (s,t)) > 1 / 2

proof end;

:: we cannot divide and it has to be proved separately.