:: Introduction to Theory of Rearrangment
:: by Yuji Sakai and Jaros{\l}aw Kotowicz
::
:: Received May 22, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

definition
let D be non empty set ;
let E be real-membered set ;
let F be PartFunc of D,E;
let r be Real;
:: original:(#)
redefine funcr (#) F ->  Element of PFuncs (D,REAL);
coherence
 r (#) F is Element of PFuncs (D,REAL)
proofend;
end;

Lm1:  for f being Function
for x being set st not x in rng f holds
f " {x} = {}
proofend;

definition
let IT be FinSequence;
attrIT is terms've_same_card_as_number  means :Def1: :: REARRAN1:def 1
 for n being Nat st 1 <= n &amp; n <= len IT holds
for B being finite set st B = IT . n holds
card B = n;
attrIT is ascending  means :Def2: :: REARRAN1:def 2
 for n being Nat st 1 <= n &amp; n <= (len IT) - 1 holds
IT . n c= IT . (n + 1);
end;

:: deftheorem Def1 defines terms've_same_card_as_number REARRAN1:def_1_:_
 for IT being FinSequence holds
( IT is terms've_same_card_as_number iff for n being Nat st 1 <= n &amp; n <= len IT holds
for B being finite set st B = IT . n holds
card B = n );

:: deftheorem Def2 defines ascending REARRAN1:def_2_:_
 for IT being FinSequence holds
( IT is ascending iff for n being Nat st 1 <= n &amp; n <= (len IT) - 1 holds
IT . n c= IT . (n + 1) );

Lm2:  for D being non empty finite set
for A being FinSequence of bool D
for k being Element of NAT st 1 <= k &amp; k <= len A holds
A . k is finite
proofend;

Lm3:  for D being non empty finite set
for A being FinSequence of bool D st len A = card D &amp; A is terms've_same_card_as_number holds
for B being finite set st B = A . (len A) holds
B = D
proofend;

Lm4:  for D being non empty finite set ex B being FinSequence of bool D st
( len B = card D &amp; B is ascending &amp; B is terms've_same_card_as_number )
proofend;

definition
let X be set ;
let IT be FinSequence of X;
attrIT is lenght_equal_card_of_set  means :Def3: :: REARRAN1:def 3
 ex B being finite set st
( B = union X &amp; len IT = card B );
end;

:: deftheorem Def3 defines lenght_equal_card_of_set REARRAN1:def_3_:_
 for X being set
for IT being FinSequence of X holds
( IT is lenght_equal_card_of_set iff ex B being finite set st
( B = union X &amp; len IT = card B ) );

registration
let D be non empty finite set ;
cluster Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like terms've_same_card_as_number ascending lenght_equal_card_of_set for FinSequence of bool D;
existence
 ex b1 being FinSequence of bool D st
( b1 is terms've_same_card_as_number &amp; b1 is ascending &amp; b1 is lenght_equal_card_of_set )
proofend;
end;

definition
let D be non empty finite set ;
mode RearrangmentGen of D is terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool D;
end;

theorem Th1: :: REARRAN1:1
for D being non empty finite set
for a being FinSequence of bool D holds
( a is lenght_equal_card_of_set iff len a = card D )
proofend;

theorem Th2: :: REARRAN1:2
for a being FinSequence holds
( a is ascending iff for n, m being Element of NAT st n <= m &amp; n in dom a &amp; m in dom a holds
a . n c= a . m )
proofend;

theorem Th3: :: REARRAN1:3
for D being non empty finite set
for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D holds a . (len a) = D
proofend;

theorem Th4: :: REARRAN1:4
for D being non empty finite set
for a being lenght_equal_card_of_set FinSequence of bool D holds len a <> 0
proofend;

theorem Th5: :: REARRAN1:5
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D
for n, m being Element of NAT st n in dom a &amp; m in dom a &amp; n <> m holds
a . n <> a . m
proofend;

theorem :: REARRAN1:6
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D
for n being Element of NAT st 1 <= n &amp; n <= (len a) - 1 holds
a . n <> a . (n + 1)
proofend;

Lm5:  for n being Element of NAT
for D being non empty finite set
for a being FinSequence of bool D st n in dom a holds
a . n c= D
proofend;

theorem Th7: :: REARRAN1:7
for n being Element of NAT
for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
proofend;

theorem Th8: :: REARRAN1:8
for n being Element of NAT
for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st 1 <= n &amp; n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}
proofend;

theorem Th9: :: REARRAN1:9
for D being non empty finite set
for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D ex d being Element of D st a . 1 = {d}
proofend;

theorem Th10: :: REARRAN1:10
for n being Element of NAT
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n &amp; n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} &amp; a . (n + 1) = (a . n) \/ {d} &amp; (a . (n + 1)) \ {d} = a . n )
proofend;

definition
let D be non empty finite set ;
let A be RearrangmentGen of D;
func Co_Gen A ->  RearrangmentGen of D means :: REARRAN1:def 4
 for m being Nat st 1 <= m &amp; m <= (len it) - 1 holds
it . m = D \ (A . ((len A) - m));
existence
 ex b1 being RearrangmentGen of D st
for m being Nat st 1 <= m &amp; m <= (len b1) - 1 holds
b1 . m = D \ (A . ((len A) - m))
proofend;
uniqueness
 for b1, b2 being RearrangmentGen of D st ( for m being Nat st 1 <= m &amp; m <= (len b1) - 1 holds
b1 . m = D \ (A . ((len A) - m)) ) &amp; ( for m being Nat st 1 <= m &amp; m <= (len b2) - 1 holds
b2 . m = D \ (A . ((len A) - m)) ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being RearrangmentGen of D st ( for m being Nat st 1 <= m &amp; m <= (len b1) - 1 holds
b1 . m = D \ (b2 . ((len b2) - m)) ) holds
for m being Nat st 1 <= m &amp; m <= (len b2) - 1 holds
b2 . m = D \ (b1 . ((len b1) - m))
proofend;
end;

:: deftheorem  defines Co_Gen REARRAN1:def_4_:_
 for D being non empty finite set
for A, b3 being RearrangmentGen of D holds
( b3 = Co_Gen A iff for m being Nat st 1 <= m &amp; m <= (len b3) - 1 holds
b3 . m = D \ (A . ((len A) - m)) );

theorem :: REARRAN1:11
canceled;

theorem Th12: :: REARRAN1:12
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
proofend;

definition
let D, C be non empty finite set ;
let A be RearrangmentGen of C;
let F be PartFunc of D,REAL;
func Rland (F,A) ->  PartFunc of C,REAL equals :: REARRAN1:def 5
 Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));
correctness
coherence
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is PartFunc of C,REAL;
;
func Rlor (F,A) ->  PartFunc of C,REAL equals :: REARRAN1:def 6
 Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C)));
correctness
coherence
Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C))) is PartFunc of C,REAL;
;
end;

:: deftheorem  defines Rland REARRAN1:def_5_:_
 for D, C being non empty finite set
for A being RearrangmentGen of C
for F being PartFunc of D,REAL holds Rland (F,A) = Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));

:: deftheorem  defines Rlor REARRAN1:def_6_:_
 for D, C being non empty finite set
for A being RearrangmentGen of C
for F being PartFunc of D,REAL holds Rlor (F,A) = Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C)));

theorem Th13: :: REARRAN1:13
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
dom (Rland (F,A)) = C
proofend;

theorem Th14: :: REARRAN1:14
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) &amp; ( for n being Element of NAT st 1 <= n &amp; n < len A &amp; c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
proofend;

theorem Th15: :: REARRAN1:15
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( ( c in A . 1 implies (Rland (F,A)) . c = (FinS (F,D)) . 1 ) &amp; ( for n being Element of NAT st 1 <= n &amp; n < len A &amp; c in (A . (n + 1)) \ (A . n) holds
(Rland (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
proofend;

theorem Th16: :: REARRAN1:16
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
rng (Rland (F,A)) = rng (FinS (F,D))
proofend;

theorem Th17: :: REARRAN1:17
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
proofend;

theorem Th18: :: REARRAN1:18
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
FinS ((Rland (F,A)),C) = FinS (F,D)
proofend;

theorem Th19: :: REARRAN1:19
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
Sum ((Rland (F,A)),C) = Sum (F,D)
proofend;

theorem :: REARRAN1:20
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( FinS (((Rland (F,A)) - r),C) = FinS ((F - r),D) &amp; Sum (((Rland (F,A)) - r),C) = Sum ((F - r),D) )
proofend;

theorem Th21: :: REARRAN1:21
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
dom (Rlor (F,A)) = C
proofend;

theorem Th22: :: REARRAN1:22
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor (F,A)) . c = (FinS (F,D)) . 1 ) &amp; ( for n being Element of NAT st 1 <= n &amp; n < len (Co_Gen A) &amp; c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
proofend;

theorem Th23: :: REARRAN1:23
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
rng (Rlor (F,A)) = rng (FinS (F,D))
proofend;

theorem Th24: :: REARRAN1:24
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
Rlor (F,A), FinS (F,D) are_fiberwise_equipotent
proofend;

theorem Th25: :: REARRAN1:25
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
FinS ((Rlor (F,A)),C) = FinS (F,D)
proofend;

theorem Th26: :: REARRAN1:26
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
Sum ((Rlor (F,A)),C) = Sum (F,D)
proofend;

theorem :: REARRAN1:27
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( FinS (((Rlor (F,A)) - r),C) = FinS ((F - r),D) &amp; Sum (((Rlor (F,A)) - r),C) = Sum ((F - r),D) )
proofend;

theorem :: REARRAN1:28
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( Rlor (F,A), Rland (F,A) are_fiberwise_equipotent &amp; FinS ((Rlor (F,A)),C) = FinS ((Rland (F,A)),C) &amp; Sum ((Rlor (F,A)),C) = Sum ((Rland (F,A)),C) )
proofend;

theorem :: REARRAN1:29
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( max+ ((Rland (F,A)) - r), max+ (F - r) are_fiberwise_equipotent &amp; FinS ((max+ ((Rland (F,A)) - r)),C) = FinS ((max+ (F - r)),D) &amp; Sum ((max+ ((Rland (F,A)) - r)),C) = Sum ((max+ (F - r)),D) )
proofend;

theorem :: REARRAN1:30
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( max- ((Rland (F,A)) - r), max- (F - r) are_fiberwise_equipotent &amp; FinS ((max- ((Rland (F,A)) - r)),C) = FinS ((max- (F - r)),D) &amp; Sum ((max- ((Rland (F,A)) - r)),C) = Sum ((max- (F - r)),D) )
proofend;

theorem Th31: :: REARRAN1:31
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C holds
( len (FinS ((Rland (F,A)),C)) = card C &amp; 1 <= len (FinS ((Rland (F,A)),C)) )
proofend;

theorem :: REARRAN1:32
for n being Element of NAT
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C &amp; n in dom A holds
(FinS ((Rland (F,A)),C)) | n = FinS ((Rland (F,A)),(A . n))
proofend;

theorem :: REARRAN1:33
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C holds
Rland ((F - r),A) = (Rland (F,A)) - r
proofend;

theorem :: REARRAN1:34
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( max+ ((Rlor (F,A)) - r), max+ (F - r) are_fiberwise_equipotent &amp; FinS ((max+ ((Rlor (F,A)) - r)),C) = FinS ((max+ (F - r)),D) &amp; Sum ((max+ ((Rlor (F,A)) - r)),C) = Sum ((max+ (F - r)),D) )
proofend;

theorem :: REARRAN1:35
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card C = card D holds
( max- ((Rlor (F,A)) - r), max- (F - r) are_fiberwise_equipotent &amp; FinS ((max- ((Rlor (F,A)) - r)),C) = FinS ((max- (F - r)),D) &amp; Sum ((max- ((Rlor (F,A)) - r)),C) = Sum ((max- (F - r)),D) )
proofend;

theorem Th36: :: REARRAN1:36
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C holds
( len (FinS ((Rlor (F,A)),C)) = card C &amp; 1 <= len (FinS ((Rlor (F,A)),C)) )
proofend;

theorem :: REARRAN1:37
for n being Element of NAT
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C &amp; n in dom A holds
(FinS ((Rlor (F,A)),C)) | n = FinS ((Rlor (F,A)),((Co_Gen A) . n))
proofend;

theorem :: REARRAN1:38
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r
proofend;

theorem :: REARRAN1:39
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total &amp; card D = card C holds
( Rland (F,A),F are_fiberwise_equipotent &amp; Rlor (F,A),F are_fiberwise_equipotent &amp; rng (Rland (F,A)) = rng F &amp; rng (Rlor (F,A)) = rng F )
proofend;