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

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 func r (#) F -> Element of PFuncs D,REAL ;
coherence
r (#) F is Element of PFuncs D,REAL

proof end;

end;

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

proof end;

definition

let IT be FinSequence;
attr IT is terms've_same_card_as_number means :Def1: :: REARRAN1:def 1
for n being Nat st 1 <= n & n <= len IT holds
for B being finite set st B = IT . n holds
card B = n;
attr IT is ascending means :Def2: :: REARRAN1:def 2
for n being Nat st 1 <= n & 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 & 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 & 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 & k <= len A holds
A . k is finite

proof end;

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

proof end;

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

proof end;

definition

let X be set ;
let IT be FinSequence of X;
attr IT is lenght_equal_card_of_set means :Def3: :: REARRAN1:def 3
ex B being finite set st
( B = union X & 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 & len IT = card B ) );

registration

let D be non empty finite set ;
cluster terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool D;
existence
ex b₁ being FinSequence of bool D st
( b₁ is terms've_same_card_as_number & b₁ is ascending & b₁ is lenght_equal_card_of_set )

proof end;

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 )

proof end;

theorem Th2: :: REARRAN1:2

for a being FinSequence holds
( a is ascending iff for n, m being Element of NAT st n <= m & n in dom a & m in dom a holds
a . n c= a . m )

proof end;

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

proof end;

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

proof end;

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 & m in dom a & n <> m holds
a . n <> a . m

proof end;

theorem Th6: :: 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 & n <= (len a) - 1 holds
a . n <> a . (n + 1)

proof end;

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

proof end;

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 <> {}

proof end;

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 & n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}

proof end;

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}

proof end;

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 & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )

proof end;

definition

let D be non empty finite set ;
let A be RearrangmentGen of D;
func Co_Gen A -> RearrangmentGen of D means :Def4: :: REARRAN1:def 4
for m being Nat st 1 <= m & m <= (len it) - 1 holds
it . m = D \ (A . ((len A) - m));
existence
ex b₁ being RearrangmentGen of D st
for m being Nat st 1 <= m & m <= (len b₁) - 1 holds
b₁ . m = D \ (A . ((len A) - m))

proof end;

uniqueness
for b₁, b₂ being RearrangmentGen of D st ( for m being Nat st 1 <= m & m <= (len b₁) - 1 holds
b₁ . m = D \ (A . ((len A) - m)) ) & ( for m being Nat st 1 <= m & m <= (len b₂) - 1 holds
b₂ . m = D \ (A . ((len A) - m)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Co_Gen REARRAN1:def 4 :

for D being non empty finite set
for A, b₃ being RearrangmentGen of D holds
( b₃ = Co_Gen A iff for m being Nat st 1 <= m & m <= (len b₃) - 1 holds
b₃ . m = D \ (A . ((len A) - m)) );

theorem :: REARRAN1:11

for D being non empty finite set
for A being RearrangmentGen of D holds Co_Gen (Co_Gen A) = A

proof end;

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 & card C = card D holds
len (MIM (FinS F,D)) = len (CHI A,C)

proof end;

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 & card C = card D holds
dom (Rland F,A) = C

proof end;

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 & card C = card D holds
( ( c in A . 1 implies ((MIM (FinS F,D)) (#) (CHI A,C)) # c = MIM (FinS F,D) ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS F,D)) (#) (CHI A,C)) # c = (n |-> 0 ) ^ (MIM ((FinS F,D) /^ n)) ) )

proof end;

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 & card C = card D holds
( ( c in A . 1 implies (Rland F,A) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland F,A) . c = (FinS F,D) . (n + 1) ) )

proof end;

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 & card C = card D holds
rng (Rland F,A) = rng (FinS F,D)

proof end;

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 & card C = card D holds
Rland F,A, FinS F,D are_fiberwise_equipotent

proof end;

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 & card C = card D holds
FinS (Rland F,A),C = FinS F,D

proof end;

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 & card C = card D holds
Sum (Rland F,A),C = Sum F,D

proof end;

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 & card C = card D holds
( FinS ((Rland F,A) - r),C = FinS (F - r),D & Sum ((Rland F,A) - r),C = Sum (F - r),D )

proof end;

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 & card C = card D holds
dom (Rlor F,A) = C

proof end;

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 & card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor F,A) . c = (FinS F,D) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len (Co_Gen A) & c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor F,A) . c = (FinS F,D) . (n + 1) ) )

proof end;

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 & card C = card D holds
rng (Rlor F,A) = rng (FinS F,D)

proof end;

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 & card C = card D holds
Rlor F,A, FinS F,D are_fiberwise_equipotent

proof end;

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 & card C = card D holds
FinS (Rlor F,A),C = FinS F,D

proof end;

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 & card C = card D holds
Sum (Rlor F,A),C = Sum F,D

proof end;

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 & card C = card D holds
( FinS ((Rlor F,A) - r),C = FinS (F - r),D & Sum ((Rlor F,A) - r),C = Sum (F - r),D )

proof end;

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 & card C = card D holds
( Rlor F,A, Rland F,A are_fiberwise_equipotent & FinS (Rlor F,A),C = FinS (Rland F,A),C & Sum (Rlor F,A),C = Sum (Rland F,A),C )

proof end;

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 & card C = card D holds
( max+ ((Rland F,A) - r), max+ (F - r) are_fiberwise_equipotent & FinS (max+ ((Rland F,A) - r)),C = FinS (max+ (F - r)),D & Sum (max+ ((Rland F,A) - r)),C = Sum (max+ (F - r)),D )

proof end;

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 & card C = card D holds
( max- ((Rland F,A) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,A) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,A) - r)),C = Sum (max- (F - r)),D )

proof end;

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 & card D = card C holds
( len (FinS (Rland F,A),C) = card C & 1 <= len (FinS (Rland F,A),C) )

proof end;

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 & card D = card C & n in dom A holds
(FinS (Rland F,A),C) | n = FinS (Rland F,A),(A . n)

proof end;

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 & card D = card C holds
Rland (F - r),A = (Rland F,A) - r

proof end;

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 & card C = card D holds
( max+ ((Rlor F,A) - r), max+ (F - r) are_fiberwise_equipotent & FinS (max+ ((Rlor F,A) - r)),C = FinS (max+ (F - r)),D & Sum (max+ ((Rlor F,A) - r)),C = Sum (max+ (F - r)),D )

proof end;

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 & card C = card D holds
( max- ((Rlor F,A) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rlor F,A) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rlor F,A) - r)),C = Sum (max- (F - r)),D )

proof end;

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 & card D = card C holds
( len (FinS (Rlor F,A),C) = card C & 1 <= len (FinS (Rlor F,A),C) )

proof end;

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 & card D = card C & n in dom A holds
(FinS (Rlor F,A),C) | n = FinS (Rlor F,A),((Co_Gen A) . n)

proof end;

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 & card D = card C holds
Rlor (F - r),A = (Rlor F,A) - r

proof end;

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 & card D = card C holds
( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent & rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F )

proof end;