Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Introduction to Theory of Rearrangement

by
Yuji Sakai, and
Jaroslaw Kotowicz

Received May 22, 1993

MML identifier: REARRAN1
[ Mizar article, MML identifier index ]

```environ

vocabulary PARTFUN1, SEQ_1, FUNCT_1, RELAT_1, BOOLE, FINSEQ_1, FINSET_1,
CARD_1, ARYTM_1, TARSKI, SQUARE_1, RFINSEQ, RFUNCT_3, RLVECT_1, TDGROUP,
FINSEQ_2, FUNCT_3, PROB_1, REARRAN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1,
FUNCT_1, FINSEQ_1, CARD_1, FINSET_1, REAL_1, NAT_1, SQUARE_1, RELSET_1,
PARTFUN1, SEQ_1, RFUNCT_1, FINSEQOP, RVSUM_1, TOPREAL1, RFINSEQ,
RFUNCT_3;
constructors SETWISEO, REAL_1, NAT_1, FINSEQOP, TOPREAL1, RFUNCT_3, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, FINSET_1, RFUNCT_3, RFINSEQ, RELSET_1, PRELAMB, XREAL_0,
FINSEQ_1, ARYTM_3, PARTFUN1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve n,m,k for Nat,
x,y for set,
r for Real;

definition let D be non empty set,
F be PartFunc of D,REAL,
r be Real;
redefine func r(#)F ->Element of PFuncs(D,REAL);
end;

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

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

definition let D be non empty finite set;
cluster terms've_same_card_as_number ascending lenght_equal_card_of_set
FinSequence of bool(D);
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;

reserve C,D for non empty finite set,
a for FinSequence of bool D;

theorem :: REARRAN1:1
for a be FinSequence of bool D holds
a is lenght_equal_card_of_set iff len a = card D;

theorem :: REARRAN1:2
for a be FinSequence holds
a is ascending iff for n,m st n<=m & n in dom a & m in dom a holds a.n c= a.m;

theorem :: REARRAN1:3
for a be terms've_same_card_as_number lenght_equal_card_of_set
FinSequence of bool D holds a.(len a) = D;

theorem :: REARRAN1:4
for a be lenght_equal_card_of_set FinSequence of bool D holds len a <> 0;

theorem :: REARRAN1:5
for a be ascending terms've_same_card_as_number FinSequence of bool D holds
for n,m holds n in dom a & m in dom a & n<>m implies a.n <> a.m;

theorem :: REARRAN1:6
for a be ascending terms've_same_card_as_number FinSequence of bool D holds
for n holds 1 <= n & n <= len a - 1 implies a.n <> a.(n+1);

theorem :: REARRAN1:7
for a be terms've_same_card_as_number FinSequence of bool D
st n in dom a holds a.n <> {};

theorem :: REARRAN1:8
for a be terms've_same_card_as_number FinSequence of bool D
st 1<=n & n<=len a - 1 holds a.(n+1) \ a.n <> {};

theorem :: REARRAN1:9
for a be terms've_same_card_as_number lenght_equal_card_of_set
FinSequence of bool D ex d be Element of D st a.1 = {d};

theorem :: REARRAN1:10
for a be terms've_same_card_as_number ascending FinSequence of bool D
st 1<=n & n<=len a - 1
ex d be Element of D st
a.(n+1) \ a.n = {d} & a.(n+1) = a.n \/ {d} & a.(n+1) \ {d} = a.n;

definition let D be non empty finite set,
A be RearrangmentGen of D;
func Co_Gen A -> RearrangmentGen of D means
:: REARRAN1:def 4
for m st 1 <= m & m <= len it - 1 holds it.m = D \ A.(len A -m);
end;

theorem :: REARRAN1:11
for A be RearrangmentGen of D holds Co_Gen(Co_Gen A) = A;

theorem :: REARRAN1:12
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds
len MIM FinS(F,D) = len CHI(A,C);

definition let D,C be non empty finite set,
A be RearrangmentGen of C,
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));
func Rlor(F,A) -> PartFunc of C,REAL equals
:: REARRAN1:def 6
Sum (MIM(FinS(F,D)) (#) CHI(Co_Gen A,C));
end;

theorem :: REARRAN1:13
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds dom Rland(F,A) = C;

theorem :: REARRAN1:14
for c be Element of C, F be PartFunc of D,REAL, A be 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 st 1<=n & n<len A & c in A.(n+1) \ A.n holds
(MIM(FinS(F,D)) (#) CHI(A,C))#c = (n |-> (0 qua Real)) ^ (MIM(FinS(F,D)/^n));

theorem :: REARRAN1:15
for c be Element of C, F be PartFunc of D,REAL, A be 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 st 1<=n & n<len A & c in A.(n+1) \ A.n holds
Rland(F,A).c = FinS(F,D).(n+1);

theorem :: REARRAN1:16
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds rng Rland(F,A) = rng FinS(F,D);

theorem :: REARRAN1:17
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds
Rland(F,A), FinS(F,D) are_fiberwise_equipotent;

theorem :: REARRAN1:18
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds FinS(Rland(F,A),C) = FinS(F,D);

theorem :: REARRAN1:19
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds Sum (Rland(F,A),C) = Sum (F,D);

theorem :: REARRAN1:20
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:21
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds dom Rlor(F,A) = C;

theorem :: REARRAN1:22
for c be Element of C, F be PartFunc of D,REAL, A be 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 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);

theorem :: REARRAN1:23
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds rng Rlor(F,A) = rng FinS(F,D);

theorem :: REARRAN1:24
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D
holds Rlor(F,A), FinS(F,D) are_fiberwise_equipotent;

theorem :: REARRAN1:25
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds FinS(Rlor(F,A),C) = FinS(F,D);

theorem :: REARRAN1:26
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card C = card D holds Sum (Rlor(F,A),C) = Sum (F,D);

theorem :: REARRAN1:27
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:28
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:29
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:30
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:31
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:32
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:33
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card D = card C holds Rland(F-r,A) = Rland(F,A) - r;

theorem :: REARRAN1:34
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:35
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:36
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:37
for F be PartFunc of D,REAL, A be 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);

theorem :: REARRAN1:38
for F be PartFunc of D,REAL, A be RearrangmentGen of C
st F is total & card D = card C holds Rlor(F-r,A) = Rlor(F,A) - r;

theorem :: REARRAN1:39
for F be PartFunc of D,REAL, A be 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;

```