:: Introduction to Theory of Rearrangment
:: by Yuji Sakai and Jaros{\l}aw Kotowicz
::
:: Received May 22, 1993
:: Copyright (c) 1993-2017 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, REAL_1, XBOOLE_0, MEMBERED, PARTFUN1,
VALUED_1, FUNCT_1, RELAT_1, FINSEQ_1, NAT_1, XXREAL_0, FINSET_1, CARD_1,
ARYTM_1, TARSKI, ARYTM_3, ZFMISC_1, ORDINAL4, RFINSEQ, RFUNCT_3,
CLASSES1, CARD_3, PBOOLE, FINSEQ_2, FUNCT_3, VALUED_0, REARRAN1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MEMBERED, FUNCT_1,
RELSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, NAT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, RFUNCT_1,
FINSEQOP, RVSUM_1, CLASSES1, RFINSEQ, RFUNCT_3;
constructors REAL_1, NAT_1, FINSEQOP, RVSUM_1, RFINSEQ, RFUNCT_3, CLASSES1,
RELSET_1, BINOP_2;
registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, VALUED_0, CARD_1, FINSEQ_2, FUNCT_1,
INT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, FINSEQ_2, RELAT_1;
expansions TARSKI, XBOOLE_0;
theorems FINSEQ_1, NAT_1, FUNCT_1, FINSEQ_2, TARSKI, CARD_2, CARD_1, PARTFUN1,
FINSET_1, FINSEQ_3, RFUNCT_1, RVSUM_1, ZFMISC_1, RFINSEQ, RFUNCT_3,
RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, FUNCOP_1, ORDINAL1,
VALUED_1, CLASSES1, INT_1, XREAL_0;
schemes NAT_1, FINSEQ_1;
begin
reserve n,m,k for Nat,
x,y for set,
r for Real;
definition
let D be non empty set, E be real-membered set, F be PartFunc of D,E, r be
Real;
redefine func r(#)F ->Element of PFuncs(D,REAL);
coherence
proof
reconsider F as PartFunc of D,E;
r(#)F is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
end;
Lm1: for f be Function,x be object st not x in rng f holds f"{x}={}
proof
let f be Function,x be object;
assume
A1: not x in rng f;
rng f misses {x}
proof
set y = the Element of rng f /\ {x};
assume rng f /\ {x} <> {};
then y in rng f & y in {x} by XBOOLE_0:def 4;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis by RELAT_1:138;
end;
definition
let IT be FinSequence;
attr IT is terms've_same_card_as_number means
:Def1:
for n be Nat st 1<=n &
n<=len IT for B being finite set st B = IT.n holds card B = n;
attr IT is ascending means
:Def2:
for n be Nat st 1<=n & n<=len IT - 1 holds IT.n c= IT.(n+1);
end;
Lm2: for D be non empty finite set, A be FinSequence of bool D, k be Nat
st 1 <= k & k <= len A holds A.k is finite
proof
let D be non empty finite set, A be FinSequence of bool D, k be Nat;
assume 1 <= k & k <= len A;
then k in dom A by FINSEQ_3:25;
then A.k in bool D by FINSEQ_2:11;
hence thesis;
end;
Lm3: for D be non empty finite set, A be FinSequence of bool D st len A = card
D & A is terms've_same_card_as_number for B being finite set st B = A.(len A)
holds B = D
proof
let D be non empty finite set, A be FinSequence of bool D;
assume that
A1: len A = card D and
A2: A is terms've_same_card_as_number;
A3: 0+1<=len A by A1,NAT_1:13;
then len A in dom A by FINSEQ_3:25;
then
A4: A.(len A) in bool D by FINSEQ_2:11;
let B be finite set such that
A5: B = A.(len A);
assume B <> D;
then
A6: B c< D by A5,A4;
card B = card D by A1,A2,A5,A3;
hence contradiction by A6,CARD_2:48;
end;
Lm4: for D be non empty finite set holds ex B be FinSequence of bool(D) st len
B = card D & B is ascending & B is terms've_same_card_as_number
proof
let D be non empty finite set;
defpred P[Nat] means for D be non empty finite set st card D = $1
holds ex B be FinSequence of bool(D) st len B = card D & B is ascending & B is
terms've_same_card_as_number;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let D be non empty finite set;
assume
A3: card D = n+1;
set x = the Element of D;
set Y = D\{x};
{x} c= D by ZFMISC_1:31;
then
A4: card Y = card D - card {x} by CARD_2:44
.= n+1-1 by A3,CARD_1:30
.= n;
now
per cases;
case
A5: n=0;
set f = <*D*>;
A6: len f = 1 by FINSEQ_1:39;
A7: rng f = {D} by FINSEQ_1:39;
rng f c= bool D
proof
let z be object;
assume z in rng f;
then z=D by A7,TARSKI:def 1;
hence thesis by ZFMISC_1:def 1;
end;
then reconsider f as FinSequence of bool D by FINSEQ_1:def 4;
take f;
thus card D = len f by A3,A5,FINSEQ_1:40;
thus f is ascending
by A6,XXREAL_0:2;
thus f is terms've_same_card_as_number
proof
let m be Nat;
assume 1<=m & m<=len f;
then
A8: m = 1 by A6,XXREAL_0:1;
let B be finite set;
assume B = f.m;
hence thesis by A3,A5,A8,FINSEQ_1:40;
end;
end;
case
n<>0;
then reconsider Y as non empty finite set by A4;
D in bool D by ZFMISC_1:def 1;
then
A9: {D} c= bool D by ZFMISC_1:31;
consider f be FinSequence of bool Y such that
A10: len f = card Y and
A11: f is ascending and
A12: f is terms've_same_card_as_number by A2,A4;
set g = f ^ <*D*>;
A13: rng <*D*> = {D} & rng g = rng f \/ rng <*D*> by FINSEQ_1:31,39;
bool Y c= bool D by ZFMISC_1:67;
then rng f c= bool D;
then rng g c= bool D \/ bool D by A9,A13,XBOOLE_1:13;
then reconsider g as FinSequence of bool D by FINSEQ_1:def 4;
take g;
A14: len <*D*> = 1 by FINSEQ_1:39;
then
A15: len g = len f + 1 by FINSEQ_1:22;
thus len g = card D by A3,A4,A10,A14,FINSEQ_1:22;
thus g is ascending
proof
let m be Nat;
assume that
A16: 1 <= m and
A17: m <= len g - 1;
m in dom f by A15,A16,A17,FINSEQ_3:25;
then
A18: g.m = f.m by FINSEQ_1:def 7;
per cases;
suppose
A19: m=len f;
then reconsider gm = g.m as finite set by A16,A18,Lm2;
gm = Y & g.(m+1) = D by A10,A12,A18,A19,Lm3,FINSEQ_1:42;
hence thesis;
end;
suppose
m<>len f;
then mlen g;
then mm+1;
then n 0
proof
let A be lenght_equal_card_of_set FinSequence of bool D;
assume len A = 0;
then card(D)=0 by Th1;
hence contradiction;
end;
theorem Th5:
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
proof
let A be ascending terms've_same_card_as_number FinSequence of bool D;
let n,m;
assume that
A1: n in dom A and
A2: m in dom A and
A3: n <> m & A.n = A.m;
A4: 1 <= m & m <= len A by A2,FINSEQ_3:25;
A5: 1 <= n & n <= len A by A1,FINSEQ_3:25;
reconsider Am = A.m as finite set by A4,Lm2;
card(Am)=m by A4,Def1;
hence contradiction by A3,A5,Def1;
end;
theorem
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)
proof
let A be ascending terms've_same_card_as_number FinSequence of bool D;
let n;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
n<=n+1 by NAT_1:11;
then n<=len A by A3,XXREAL_0:2;
then
A4: n in dom A by A1,FINSEQ_3:25;
1<=n+1 by NAT_1:11;
then
A5: n+1 in dom A by A3,FINSEQ_3:25;
n <> n+1;
hence thesis by A4,A5,Th5;
end;
Lm5: n in dom a implies a.n c= D
proof
assume n in dom a;
then a.n in bool D by FINSEQ_2:11;
hence thesis;
end;
theorem Th7:
for a be terms've_same_card_as_number FinSequence of bool D st n
in dom a holds a.n <> {}
proof
let A be terms've_same_card_as_number FinSequence of bool D;
assume n in dom A;
then
A1: 1<=n & n<=len A by FINSEQ_3:25;
assume A.n = {};
hence contradiction by A1,Def1,CARD_1:27;
end;
theorem Th8:
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 <> {}
proof
let A be terms've_same_card_as_number FinSequence of bool D;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
n<=n+1 by NAT_1:11;
then
A4: n<=len A by A3,XXREAL_0:2;
then reconsider An1 = A.(n+1), An = A.n as finite set by A1,A3,Lm2,NAT_1:11;
1<=n+1 by NAT_1:11;
then
A5: card (An1) = n+1 by A3,Def1;
assume A.(n+1) \ A.n = {};
then
A6: A.(n+1) c= A.n by XBOOLE_1:37;
card (An) = n by A1,A4,Def1;
then n+1 <= n by A5,A6,NAT_1:43;
then 1<=n-n by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
theorem Th9:
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}
proof
let A be terms've_same_card_as_number lenght_equal_card_of_set FinSequence
of bool D;
len A <> 0 by Th4;
then
A1: 0+1<=len A by NAT_1:13;
then reconsider A1 = A.1 as finite set by Lm2;
card(A1)=1 by A1,Def1;
then consider x being object such that
A2: {x} = A.1 by CARD_2:42;
1 in dom A by A1,FINSEQ_3:25;
then A.1 c= D by Lm5;
then reconsider x as Element of D by A2,ZFMISC_1:31;
take x;
thus thesis by A2;
end;
theorem Th10:
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
proof
let A be terms've_same_card_as_number ascending FinSequence of bool D;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
A4: A.n c= A.(n+1) by A1,A2,Def2;
n<=n+1 by NAT_1:11;
then
A5: n<=len A by A3,XXREAL_0:2;
then reconsider An1 = A.(n+1), An = A.n as finite set by A1,A3,Lm2,NAT_1:11;
A6: card(An) = n by A1,A5,Def1;
A7: 1<=n+1 by NAT_1:11;
then card(An1) = n+1 by A3,Def1;
then card (An1 \ An) = n+1-n by A4,A6,CARD_2:44
.= 1;
then consider x being object such that
A8: {x} = A.(n+1) \ A.n by CARD_2:42;
x in A.(n+1) \ A.n by A8,ZFMISC_1:31;
then
A9: not x in A.n by XBOOLE_0:def 5;
A10: x in A.(n+1) by A8,ZFMISC_1:31;
n+1 in dom A by A3,A7,FINSEQ_3:25;
then A.(n+1) c= D by Lm5;
then reconsider x as Element of D by A10;
take x;
thus {x} = A.(n+1) \ A.n by A8;
thus A.n \/ {x} = A.(n+1) \/ A.n by A8,XBOOLE_1:39
.= A.(n+1) by A4,XBOOLE_1:12;
hence A.(n+1) \ {x} = (A.n \ {x}) \/ ({x} \ {x}) by XBOOLE_1:42
.= (A.n \ {x}) \/ {} by XBOOLE_1:37
.= A.n by A9,ZFMISC_1:57;
end;
definition
let D be non empty finite set, A be RearrangmentGen of D;
func Co_Gen A -> RearrangmentGen of D means
for m be Nat st 1 <= m & m <= len it - 1 holds it.m = D \ A.(len A -m);
existence
proof
deffunc F(Nat)= D \ A.(len A -$1);
set c = card D;
D c= D;
then reconsider y = D as Subset of D;
0+1 <= c by NAT_1:13;
then max(0,c -1) = c - 1 by FINSEQ_2:4;
then reconsider c1=c - 1 as Element of NAT by FINSEQ_2:5;
consider f be FinSequence such that
A1: len f = c1 and
A2: for m be Nat st m in dom f holds f.m = F(m) from FINSEQ_1:sch 2;
A3: dom f = Seg c1 by A1,FINSEQ_1:def 3;
rng f c= bool D
proof
let x be object;
assume x in rng f;
then consider m being Nat such that
A4: m in dom f & f.m = x by FINSEQ_2:10;
D \ A.(len A -m) c= D;
then x is Subset of D by A2,A4;
hence thesis;
end;
then reconsider f as FinSequence of bool(D) by FINSEQ_1:def 4;
set C = f^<*y*>;
A5: len C = len f + len <*y*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
A6: card D = len A by Th1;
A7: C is terms've_same_card_as_number
proof
let m be Nat;
assume that
A8: 1 <= m and
A9: m <= len C;
max(0,len C -m) = len C -m by A9,FINSEQ_2:4;
then reconsider l = len C - m as Element of NAT by FINSEQ_2:5;
let B be finite set such that
A10: B = C.m;
now
per cases;
case
m = len C;
hence thesis by A1,A5,A10,FINSEQ_1:42;
end;
case
m <> len C;
then m < len C by A9,XXREAL_0:1;
then
A11: m+1 <= len C by NAT_1:13;
then
A12: 1 <= l by XREAL_1:19;
A13: l <= len A by A6,A1,A5,XREAL_1:43;
then
A14: l in dom A by A12,FINSEQ_3:25;
then reconsider Al = A.l as finite set by Lm5,FINSET_1:1;
m <= len C - 1 by A11,XREAL_1:19;
then
A15: m in dom f by A5,A8,FINSEQ_3:25;
then C.m = f.m by FINSEQ_1:def 7
.= D \ A.l by A6,A1,A2,A5,A15;
hence card B = card(D) - card(Al) by A10,A14,Lm5,CARD_2:44
.= len A - l by A6,A12,A13,Def1
.= m by A6,A1,A5;
end;
end;
hence thesis;
end;
for m be Nat st 1 <= m & m <= len C - 1 holds C.m c= C.(m+1)
proof
let m be Nat;
assume that
A16: 1 <= m and
A17: m <= len C - 1;
A18: m in dom f by A5,A16,A17,FINSEQ_3:25;
then
A19: C.m = f.m by FINSEQ_1:def 7
.= D \ A.(len A - m) by A2,A18;
per cases;
suppose
m = len C - 1;
then C.(m+1) = D by A5,FINSEQ_1:42;
hence thesis by A19;
end;
suppose
m <> len C - 1;
then
A20: m < len C - 1 by A17,XXREAL_0:1;
then
A21: m+1 < len A by A6,A1,A5,XREAL_1:20;
then max(0,len A -(m+1)) = len A -(m+1) by FINSEQ_2:4;
then reconsider l = len A -(m+1) as Element of NAT by FINSEQ_2:5;
A22: 1 <= m+1 by NAT_1:11;
m+1<= len C - 1 by A5,A20,NAT_1:13;
then
A23: m+1 in dom f by A5,A22,FINSEQ_3:25;
then
A24: C.(m+1) = f.(m+1) by FINSEQ_1:def 7
.= D \ A.l by A2,A23;
m+1+1<=len A by A21,NAT_1:13;
then
A25: 1 <= len A - (m+1) by XREAL_1:19;
l <= len A - 1 by A22,XREAL_1:13;
then A.l c= A.(l+1) by A25,Def2;
hence thesis by A19,A24,XBOOLE_1:34;
end;
end;
then reconsider C as RearrangmentGen of D by A1,A5,A7,Def2,Th1;
take C;
let m be Nat;
assume 1 <= m & m <= len C - 1;
then
A26: m in Seg c1 by A1,A5,FINSEQ_1:1;
then m in dom f by A1,FINSEQ_1:def 3;
hence C.m = f.m by FINSEQ_1:def 7
.= D \ A.(len A -m) by A2,A3,A26;
end;
uniqueness
proof
let f1,f2 be RearrangmentGen of D such that
A27: for m be Nat st 1 <= m & m <= len f1 - 1 holds f1.m = D \ A.(len A -m) and
A28: for m be Nat st 1 <= m & m <= len f2 - 1 holds f2.m = D \ A.(len A -m);
A29: len f2 = card D by Th1;
A30: len A = card D by Th1;
A31: len f1 = card D by Th1;
then
A32: dom f1 = Seg len A by A30,FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
assume
A33: m in dom f1;
then
A34: 1<=m by A32,FINSEQ_1:1;
A35: m<=len A by A32,A33,FINSEQ_1:1;
per cases;
suppose
A36: m = len A;
then f1.m = D by A31,A30,Th3;
hence f1.m = f2.m by A29,A30,A36,Th3;
end;
suppose
m <> len A;
then m PartFunc of C,REAL equals
Sum (MIM(FinS(F,D)) (#) CHI(A,
C));
correctness;
func Rlor(F,A) -> PartFunc of C,REAL equals
Sum (MIM(FinS(F,D)) (#) CHI(
Co_Gen A,C));
correctness;
end;
theorem Th12:
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
proof
let F be PartFunc of D,REAL, A be RearrangmentGen of C;
A1: len CHI(A,C) = len A & len A <> 0 by Th4,RFUNCT_3:def 6;
assume F is total & card C = card D;
then
A2: len MIM(FinS(F,D)) = len CHI(A,C) by Th11;
thus dom Rland(F,A) c= C;
let x be object;
assume x in C;
then reconsider c = x as Element of C;
len (MIM(FinS(F,D))(#) CHI(A,C)) = min(len MIM(FinS(F,D)), len CHI(A,C))
& c is_common_for_dom (MIM(FinS(F,D)) (#) CHI(A,C)) by RFUNCT_3:32,def 7;
hence thesis by A2,A1,RFUNCT_3:28;
end;
theorem Th13:
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 (0 qua Real)) ^
(MIM(FinS(F,D)/^n))
proof
let c be Element of C, F be PartFunc of D,REAL, A be RearrangmentGen of C;
set fd = FinS(F,D), mf = MIM(fd), h = CHI(A,C), fh = (mf(#)h)#c;
A1: dom A = Seg len A by FINSEQ_1:def 3;
A2: dom(mf(#)h) =Seg len(mf(#)h) by FINSEQ_1:def 3;
A3: len h = len A by RFUNCT_3:def 6;
A4: len mf = len fd by RFINSEQ:def 2;
A5: dom fh = Seg len fh by FINSEQ_1:def 3;
A6: min(len mf,len h) = len(mf(#)h) by RFUNCT_3:def 7;
assume F is total & card C = card D;
then
A7: len mf = len h by Th11;
A8: len fh =len(mf(#)h) by RFUNCT_3:def 8;
A9: dom h = Seg len h by FINSEQ_1:def 3;
thus c in A.1 implies (mf (#) h)#c = mf
proof
assume
A10: c in A.1;
A11: for n st n in dom A holds c in A.n
proof
let n;
assume
A12: n in dom A;
then
A13: 1<=n by FINSEQ_3:25;
n<=len A by A12,FINSEQ_3:25;
then 1<=len A by A13,XXREAL_0:2;
then 1 in dom A by FINSEQ_3:25;
then A.1 c= A.n by A12,A13,Th2;
hence thesis by A10;
end;
A14: dom ((mf(#)h)#c) = Seg len mf by A7,A6,A8,FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1=fd.m as Real;
assume
A15: m in dom((mf(#)h)#c);
then
A16: 1<=m by FINSEQ_3:25;
A17: h.m = chi(A.m,C) by A9,A5,A7,A6,A8,A15,RFUNCT_3:def 6;
A18: c in A.m by A1,A5,A7,A3,A6,A8,A11,A15;
m in dom mf by A14,A15,FINSEQ_1:def 3;
then
A19: m<=len mf by FINSEQ_3:25;
now
per cases;
case
A20: m=len mf;
then mf.m = r1 by A4,RFINSEQ:def 2;
then (mf(#)h).m = r1(#)chi(A.m,C) by A2,A5,A8,A15,A17,RFUNCT_3:def 7;
then
A21: ((mf(#)h)#c).m = (r1(#)chi(A.m,C)).c by A15,RFUNCT_3:def 8;
dom(r1(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = r1*(chi(A.m,C)).c by A21,VALUED_1:def 5
.= r1*1 by A18,RFUNCT_1:63
.= mf.m by A4,A20,RFINSEQ:def 2;
end;
case
A22: m<>len mf;
reconsider r2=fd.(m+1) as Real;
m (0 qua Real);
A37: len mfn = len fdn by RFINSEQ:def 2;
A38: len n0 = n by CARD_1:def 7;
len fdn = len fd - n by A7,A3,A4,A26,RFINSEQ:def 1;
then
A39: len (n0 ^ mfn) = n + (len fd -n) by A37,A38,FINSEQ_1:22
.= len mf by RFINSEQ:def 2;
then
A40: dom(n0^mfn) = Seg len mf by FINSEQ_1:def 3;
A41: dom n0 = Seg len n0 by FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1=fd.m as Real;
assume
A42: m in dom (n0^mfn);
then
A43: 1<=m by FINSEQ_3:25;
m in dom mf by A40,A42,FINSEQ_1:def 3;
then
A44: m<=len mf by FINSEQ_3:25;
A45: h.m = chi(A.m,C) by A9,A7,A40,A42,RFUNCT_3:def 6;
now
per cases;
case
A46: m<=n;
reconsider r2=fd.(m+1) as Real;
mlen mf;
reconsider r2=fd.(m+1) as Real;
m (0 qua Real)) ^ mfn by A3,A5,A6,A7,Th13;
hence Rland(F,B).c = Sum(n |-> In(0,REAL)) + (Sum mfn)
by A1,RVSUM_1:75
.= 0 + Sum mfn by RVSUM_1:81
.= FinS(F,D).(n+1) by A4,A2,A6,RFINSEQ:17;
end;
theorem Th15:
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set fd = FinS(F,D), p = Rland(F,B), mf = MIM(fd), h = CHI(B,C);
A3: len mf = len h by A1,A2,Th11;
A4: dom F = D by A1,PARTFUN1:def 2;
then reconsider fd9 = fd, F9 = F as finite Function by FINSET_1:10;
reconsider dfd = dom fd9, dF = dom F9 as finite set;
A5: len h = len B & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
A6: dom p = C by A1,A2,Th12;
A7: dom fd = Seg len fd by FINSEQ_1:def 3;
A8: dom B = Seg len B by FINSEQ_1:def 3;
F|D = F by A4,RELAT_1:68;
then fd, F are_fiberwise_equipotent by A4,RFUNCT_3:def 13;
then card dfd = card dF by CLASSES1:81;
then len fd <> 0 by A4,A7;
then
A9: 0+1<=len fd by NAT_1:13;
then
A10: 1 in dom fd by FINSEQ_3:25;
thus rng p c= rng fd
proof
let x be object;
assume x in rng p;
then consider c be Element of C such that
c in dom p and
A11: p.c = x by PARTFUN1:3;
defpred P[set] means $1 in dom B & c in B.$1;
A12: ex n be Nat st P[n]
proof
take n = len B;
B.n = C by Th3;
hence thesis by A3,A5,A9,FINSEQ_3:25;
end;
consider mi be Nat such that
A13: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A12);
A14: 1<=mi by A13,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A15: mi<=len B by A13,FINSEQ_3:25;
now
per cases;
case
mi = 1;
then p.c = fd.1 by A1,A2,A13,Th14;
hence thesis by A10,A11,FUNCT_1:def 3;
end;
case
mi <> 1;
then 1 {} by A3,A5,A7,A8,A10,Th7;
B.1 c= C by A3,A5,A7,A8,A10,Lm5;
then reconsider y as Element of C by A24;
p.y = fd.1 by A1,A2,A24,Th14;
hence thesis by A6,A20,A23,FUNCT_1:def 3;
end;
case
A25: mi<>1;
set y = the Element of B.(m1+1) \ B.m1;
1 {} by A3,A5,A26,Th8;
then
A28: y in B.(m1+1) by XBOOLE_0:def 5;
B.mi c= C by A3,A5,A7,A8,A20,Lm5;
then reconsider y as Element of C by A28;
m1ma;
then l=r by A11,A22,RFINSEQ:19;
now
per cases;
case
l=mi;
then o in {x} by A13,TARSKI:def 1;
hence thesis by A22,FUNCT_1:def 7;
end;
case
l<>mi;
then mi=o by A13,A22,RFINSEQ:19;
then r=o by A24,XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence thesis by A22,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let y be object;
assume
A25: y in fd"{x};
then
A26: y in dom fd by FUNCT_1:def 7;
reconsider l=y as Element of NAT by A25;
A27: 1<=l by A26,FINSEQ_3:25;
fd.y in {x} by A25,FUNCT_1:def 7;
then
A28: fd.l=x by TARSKI:def 1;
then mi<=l by A13,A26;
then mi0;
then
A48: 0+1ma;
then n+1=r by A4,A1,A2,A11,A40,A51,RFINSEQ:19;
r>=p.c by A4,A1,A2,A13,A36,A40,A48,A51,RFINSEQ:19
;
then r=p.c by A52,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in B.n;
hence thesis by A39,A41,A46,A49,FINSEQ_3:25,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A53: P[ 0 ] by FINSEQ_3:25;
A54: for n holds P[n] from NAT_1:sch 2(A53,A38);
ma in dom B by A4,A1,A11,FINSEQ_3:29;
then cy in p"{x} by A37,A54;
hence thesis;
end;
let y be object;
assume
A55: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A55,FUNCT_1:def 7;
then
A56: p.cy = x by TARSKI:def 1;
defpred Q[Nat] means $1 in dom B & ma<$1 & cy in B.$1;
assume
A57: not y in B.ma;
A58: ex n be Nat st Q[n]
proof
take n=len B;
len B <> 0 by Th4;
then 0+1<=len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25;
A59: B.n= C by Th3;
now
assume n <= ma;
then ma=len B by A4,A1,A16,XXREAL_0:1;
then cy in B.ma by A59;
hence contradiction by A57;
end;
hence thesis by A59;
end;
consider mm be Nat such that
A60: Q[mm] & for n be Nat st Q[n] holds mm<=n from NAT_1:
sch 5(A58);
1<=mm by A60,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A60,NAT_1:13;
then
A61: ma<=1m by XREAL_1:19;
then
A62: 1<=1m by A30,XXREAL_0:2;
A63: mm in dom fd by A4,A1,A60,FINSEQ_3:29;
A64: mm<=len B by A60,FINSEQ_3:25;
A65: mm 1m;
then
A68: ma < 1m by A61,XXREAL_0:1;
now
assume cy in B.(1m);
then mm<=1m by A60,A67,A68;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in B.(1m+1) \ B.(1m) by A60,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A62,A66,Th14;
hence contradiction by A11,A56,A60,A63;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(fd"{x}) by A4,A1,A30,A16,A33,A36,Def1;
end;
case
A69: mi<>1;
then 1 n+1;
then
A83: mima;
then n+1=r by A4,A1,A2,A11,A77,A87,RFINSEQ:19;
r>=p.c by A4,A1,A2,A13,A77,A83,A87,RFINSEQ:19;
then r=p.c by A88,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in B.n \ B.m1;
hence thesis by A76,A79,A83,A84,A85,FINSEQ_3:25
,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A89: P[ 0 ];
A90: for n holds P[n] from NAT_1:sch 2(A89,A75);
assume
A91: y in B.ma \ B.m1;
then y in B.ma;
then reconsider cy = y as Element of C by A74;
ma in dom B by A4,A1,A11,FINSEQ_3:29;
then cy in p"{x} by A31,A91,A90;
hence thesis;
end;
let y be object;
assume
A92: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A92,FUNCT_1:def 7;
then
A93: p.cy = x by TARSKI:def 1;
assume
A94: not y in B.ma \ B.m1;
now
per cases by A94,XBOOLE_0:def 5;
case
A95: not y in B.ma;
defpred Q[Nat] means $1 in dom B & ma<$1 & cy in B.$1;
A96: ex n be Nat st Q[n]
proof
take n=len B;
len B <> 0 by Th4;
then 0+1<=len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25;
A97: B.n= C by Th3;
now
assume n <= ma;
then ma=len B by A4,A1,A16,XXREAL_0:1;
then cy in B.ma by A97;
hence contradiction by A95;
end;
hence thesis by A97;
end;
consider mm be Nat such that
A98: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A96);
1<=mm by A98,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A98,NAT_1:13;
then
A99: ma<=1m by XREAL_1:19;
then
A100: 1<=1m by A30,XXREAL_0:2;
A101: mm in dom fd by A4,A1,A98,FINSEQ_3:29;
A102: mm<=len B by A98,FINSEQ_3:25;
A103: mm 1m;
then
A106: ma < 1m by A99,XXREAL_0:1;
now
assume cy in B.(1m);
then mm<=1m by A98,A105,A106;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in B.(1m+1) \ B.(1m) by A98,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A100,A104,Th14;
hence contradiction by A11,A93,A98,A101;
end;
end;
hence contradiction;
end;
case
A107: y in B.m1;
defpred Q[Nat] means $1 in dom B & $1<=m1 & cy in B.$1;
A108: ex n be Nat st Q[n] by A72,A107;
consider mm be Nat such that
A109: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A108);
A110: 1<=mm by A109,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m=mm-1 as Element of NAT by FINSEQ_2:5;
A111: mm<=len B by A109,FINSEQ_3:25;
A112: mm in dom fd by A4,A1,A109,FINSEQ_3:29;
now
per cases;
case
mm=1;
then p.cy = fd.1 by A3,A109,Th14;
then mi<=1 by A13,A35,A93;
hence contradiction by A14,A69,XXREAL_0:1;
end;
case
mm<>1;
then 1 (0 qua Real)) ^ mfn by A3,A5,A6,A7,Th13;
hence Rlor(F,B).c = Sum(n |-> In(0,REAL)) + (Sum mfn)
by A1,RVSUM_1:75
.= 0 + Sum mfn by RVSUM_1:81
.= FinS(F,D).(n+1) by A4,A2,A6,RFINSEQ:17;
end;
theorem Th22:
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set fd = FinS(F,D), p = Rlor(F,B), mf = MIM(fd), b = Co_Gen B, h = CHI(b,C);
A3: len mf = len h by A1,A2,Th11;
dom F is finite;
then reconsider F9 = F as finite Function by FINSET_1:10;
A4: dom fd = Seg len fd by FINSEQ_1:def 3;
A5: dom p = C by A1,A2,Th20;
A6: dom b = Seg len b by FINSEQ_1:def 3;
reconsider dfd = dom fd, dF = dom F9 as finite set;
A7: len h = len b & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
A8: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then fd, F are_fiberwise_equipotent by A8,RFUNCT_3:def 13;
then card dfd = card dF by CLASSES1:81;
then len fd <> 0 by A8,A4;
then
A9: 0+1<=len fd by NAT_1:13;
then
A10: 1 in dom fd by FINSEQ_3:25;
thus rng p c= rng fd
proof
let x be object;
assume x in rng p;
then consider c be Element of C such that
c in dom p and
A11: p.c = x by PARTFUN1:3;
defpred P[set] means $1 in dom b & c in b.$1;
A12: ex n be Nat st P[n]
proof
take n = len b;
b.n = C by Th3;
hence thesis by A3,A7,A9,FINSEQ_3:25;
end;
consider mi be Nat such that
A13: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A12);
A14: 1<=mi by A13,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A15: mi<=len b by A13,FINSEQ_3:25;
now
per cases;
case
mi = 1;
then p.c = fd.1 by A1,A2,A13,Th21;
hence thesis by A10,A11,FUNCT_1:def 3;
end;
case
mi <> 1;
then 1 {} by A3,A7,A4,A6,A10,Th7;
b.1 c= C by A3,A7,A4,A6,A10,Lm5;
then reconsider y as Element of C by A24;
p.y = fd.1 by A1,A2,A24,Th21;
hence thesis by A5,A20,A23,FUNCT_1:def 3;
end;
case
A25: mi<>1;
set y = the Element of b.(m1+1) \ b.m1;
1 {} by A3,A7,A26,Th8;
then
A28: y in b.(m1+1) by XBOOLE_0:def 5;
b.mi c= C by A3,A7,A4,A6,A20,Lm5;
then reconsider y as Element of C by A28;
m1ma;
then l=r by A14,A21,RFINSEQ:19;
now
per cases;
case
l=mi;
then o in {x} by A10,TARSKI:def 1;
hence thesis by A21,FUNCT_1:def 7;
end;
case
l<>mi;
then mi=o by A10,A21,RFINSEQ:19;
then r=o by A23,XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence thesis by A21,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let y be object;
assume
A24: y in fd"{x};
then
A25: y in dom fd by FUNCT_1:def 7;
reconsider l=y as Element of NAT by A24;
A26: 1<=l by A25,FINSEQ_3:25;
fd.y in {x} by A24,FUNCT_1:def 7;
then
A27: fd.l=x by TARSKI:def 1;
then mi<=l by A10,A25;
then mi0;
then
A47: 0+1ma;
then n+1=r by A5,A1,A6,A14,A39,A50,RFINSEQ:19;
r>=p.c by A5,A1,A6,A10,A35,A39,A47,A50,RFINSEQ:19
;
then r=p.c by A51,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in b.n;
hence thesis by A38,A40,A45,A48,FINSEQ_3:25,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A52: P[ 0 ] by FINSEQ_3:25;
A53: for n holds P[n] from NAT_1:sch 2(A52,A37);
ma in dom b by A5,A1,A14,FINSEQ_3:29;
then cy in p"{x} by A36,A53;
hence thesis;
end;
let y be object;
assume
A54: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A54,FUNCT_1:def 7;
then
A55: p.cy = x by TARSKI:def 1;
defpred Q[Nat] means $1 in dom b & ma<$1 & cy in b.$1;
assume
A56: not y in b.ma;
A57: ex n be Nat st Q[n]
proof
take n=len b;
len b <> 0 by Th4;
then 0+1<=len b by NAT_1:13;
hence n in dom b by FINSEQ_3:25;
A58: b.n= C by Th3;
now
assume n <= ma;
then ma=len b by A5,A1,A15,XXREAL_0:1;
then cy in b.ma by A58;
hence contradiction by A56;
end;
hence thesis by A58;
end;
consider mm be Nat such that
A59: Q[mm] & for n be Nat st Q[n] holds mm<=n from NAT_1:
sch 5(A57 );
1<=mm by A59,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A59,NAT_1:13;
then
A60: ma<=1m by XREAL_1:19;
then
A61: 1<=1m by A29,XXREAL_0:2;
A62: mm in dom fd by A5,A1,A59,FINSEQ_3:29;
A63: mm<=len b by A59,FINSEQ_3:25;
A64: mm 1m;
then
A67: ma < 1m by A60,XXREAL_0:1;
now
assume cy in b.(1m);
then mm<=1m by A59,A66,A67;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in b.(1m+1) \ b.(1m) by A59,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A61,A65,Th21;
hence contradiction by A14,A55,A59,A62;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(fd"{x}) by A5,A1,A29,A15,A32,A35,Def1;
end;
case
A68: mi<>1;
then 1 n+1;
then
A82: mima;
then n+1=r by A5,A1,A6,A14,A76,A86,RFINSEQ:19;
r>=p.c by A5,A1,A6,A10,A76,A82,A86,RFINSEQ:19;
then r=p.c by A87,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in b.n \ b.m1;
hence thesis by A75,A78,A82,A83,A84,FINSEQ_3:25
,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A88: P[ 0 ];
A89: for n holds P[n] from NAT_1:sch 2(A88,A74);
assume
A90: y in b.ma \ b.m1;
then y in b.ma;
then reconsider cy = y as Element of C by A73;
ma in dom b by A5,A1,A14,FINSEQ_3:29;
then cy in p"{x} by A30,A90,A89;
hence thesis;
end;
let y be object;
assume
A91: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A91,FUNCT_1:def 7;
then
A92: p.cy = x by TARSKI:def 1;
assume
A93: not y in b.ma \ b.m1;
now
per cases by A93,XBOOLE_0:def 5;
case
A94: not y in b.ma;
defpred Q[Nat] means $1 in dom b & ma<$1 & cy in b.$1;
A95: ex n be Nat st Q[n]
proof
take n=len b;
len b <> 0 by Th4;
then 0+1<=len b by NAT_1:13;
hence n in dom b by FINSEQ_3:25;
A96: b.n= C by Th3;
now
assume n <= ma;
then ma=len b by A5,A1,A15,XXREAL_0:1;
then cy in b.ma by A96;
hence contradiction by A94;
end;
hence thesis by A96;
end;
consider mm be Nat such that
A97: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A95);
1<=mm by A97,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A97,NAT_1:13;
then
A98: ma<=1m by XREAL_1:19;
then
A99: 1<=1m by A29,XXREAL_0:2;
A100: mm in dom fd by A5,A1,A97,FINSEQ_3:29;
A101: mm<=len b by A97,FINSEQ_3:25;
A102: mm 1m;
then
A105: ma < 1m by A98,XXREAL_0:1;
now
assume cy in b.(1m);
then mm<=1m by A97,A104,A105;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in b.(1m+1) \ b.(1m) by A97,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A99,A103,Th21;
hence contradiction by A14,A92,A97,A100;
end;
end;
hence contradiction;
end;
case
A106: y in b.m1;
defpred Q[Nat] means $1 in dom b & $1<=m1 & cy in b.$1;
A107: ex n be Nat st Q[n] by A71,A106;
consider mm be Nat such that
A108: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A107);
A109: 1<=mm by A108,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m=mm-1 as Element of NAT by FINSEQ_2:5;
A110: mm<=len b by A108,FINSEQ_3:25;
A111: mm in dom fd by A5,A1,A108,FINSEQ_3:29;
now
per cases;
case
mm=1;
then p.cy = fd.1 by A2,A108,Th21;
then mi<=1 by A10,A34,A92;
hence contradiction by A11,A68,XXREAL_0:1;
end;
case
mm<>1;
then 1 by A17,A18,RFUNCT_3:69;
len(FinS(p,C)|(m+1)) = 1 by A17,A20,FINSEQ_1:59;
hence thesis by A22,A21,FINSEQ_1:40;
end;
case
A23: m<>0;
A24: Seg m c= Seg(m+1) by A8,FINSEQ_1:5;
A25: (f|(m+1))|m = (f|(m+1))|(Seg m) by FINSEQ_1:def 15
.= (f|Seg(m+1))|(Seg m) by FINSEQ_1:def 15
.= f|(Seg(m+1) /\ (Seg m)) by RELAT_1:71
.= f|(Seg m) by A24,XBOOLE_1:28
.= f|m by FINSEQ_1:def 15;
A26: 0+1<=m by A23,NAT_1:13;
then consider d be Element of C such that
A27: B.(m+1) \ B.m = {d} and
B.(m+1) = B.m \/ {d} and
A28: B.(m+1) \ {d} = B.m by A15,Th10;
A29: d in {d} by TARSKI:def 1;
then p.d = FinS(F,D).(m+1) by A1,A14,A26,A27,Th14
.= FinS(p,C).(m+1) by A1,Th17
.=(f|(m+1)).(m+1) by A5,A4,A3,A9,A10,RFINSEQ:6;
then
A30: f|(m+1) = f|m ^ <*p.d*> by A16,A25,RFINSEQ:7;
d in dom p /\ B.(m+1) by A11,A27,A29,XBOOLE_0:def 4;
then
A31: d in dom(p|(B.(m+1))) by RELAT_1:61;
A32: (f|(m+1)) is non-increasing by RFINSEQ:20;
A33: dom(p|(B.(m+1))) = dom p /\ (B.(m+1)) by RELAT_1:61
.= B.(m+1) by A9,A11,Lm5,XBOOLE_1:28;
B.(m+1) is finite by A9,Lm5,FINSET_1:1;
then
f|(m+1), p|(B.(m+1)) are_fiberwise_equipotent by A7,A13,A26,A28,A30,A31
,FINSEQ_3:25,RFUNCT_3:65;
hence thesis by A33,A32,RFUNCT_3:def 13;
end;
end;
hence thesis;
end;
A34: P[ 0 ] by FINSEQ_3:25;
for m holds P[m] from NAT_1:sch 2(A34,A6);
hence thesis by A2;
end;
theorem
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
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom Rland(F,B) = C by A1,A2,Th12;
A4: dom F = D by A1,PARTFUN1:def 2;
then
A5: dom(F-r) = D by VALUED_1:3;
then
A6: F-r is total by PARTFUN1:def 2;
(F-r)|D = F-r by A5,RELAT_1:68;
then
A7: len FinS(F-r,D) = card D by A5,RFUNCT_3:67;
A8: len B = card C by Th1;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
F|D = F by A4,RELAT_1:68;
then
A9: FinS(F-r,D) = FinS(F,D) - (card D |-> rr) by A4,RFUNCT_3:73;
A10: now
let c be Element of C;
assume c in dom Rland(F-r,B);
defpred P[set] means $1 in dom B & c in B.$1;
A11: C = B.(len B) by Th3;
len B <> 0 by Th4;
then
A12: 0+1<=len B by NAT_1:13;
then
A13: 1 in dom B by FINSEQ_3:25;
len B in dom B by A12,FINSEQ_3:25;
then
A14: ex n be Nat st P[n] by A11;
consider mi be Nat such that
A15: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A14);
A16: 1<=mi by A15,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi - 1 as Element of NAT by FINSEQ_2:5;
A17: mi<=len B by A15,FINSEQ_3:25;
A18: mi r).1 = r by FUNCOP_1:7;
(Rland(F-r,B)).c = FinS(F-r,D).1 & (Rland(F,B)).c = FinS(F,D).1
by A1,A2,A6,A15,A21,Th14;
hence (Rland(F-r,B)).c = (Rland(F,B)).c - r by A9,A22,A23,VALUED_1:13
.= (Rland(F,B) - r).c by A3,VALUED_1:3;
end;
case
mi <> 1;
then 1 r).(m1+1) = r by FUNCOP_1:7;
m1+1 in dom FinS(F-r,D) by A2,A7,A8,A15,FINSEQ_3:29;
hence (Rland(F-r,B)).c = (Rland(F,B)).c - r by A9,A25,A26,VALUED_1:13
.= (Rland(F,B) - r).c by A3,VALUED_1:3;
end;
end;
hence (Rland(F-r,B)).c = (Rland(F,B) - r).c;
end;
dom(Rland(F,B) - r) = C by A3,VALUED_1:3;
hence thesis by A2,A6,A10,Th12,PARTFUN1:5;
end;
theorem
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max+(Rlor(F,B)-r), mf = max+(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then Rlor(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rlor(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:41;
A6: dom mp = dom (Rlor(F,B)-r) by RFUNCT_3:def 10;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 10;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max-(Rlor(F,B)-r), mf = max-(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then Rlor(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rlor(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:42;
A6: dom mp = dom (Rlor(F,B)-r) by RFUNCT_3:def 11;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 11;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem Th35:
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set p = Rlor(F,B);
assume F is total & card D = card C;
then
A1: dom p = C by Th20;
then
A2: p|C = p by RELAT_1:68;
hence len FinS(p,C) = card C by A1,RFUNCT_3:67;
0+1<=card C by NAT_1:13;
hence thesis by A1,A2,RFUNCT_3:67;
end;
theorem
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)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total & card D = card C and
A2: n in dom B;
set p = Rlor(F,B), b = Co_Gen B;
A3: len FinS(p,C) = card C by A1,Th35;
defpred P[Nat] means $1 in dom b implies FinS(Rlor(F,B),C) | $1 =
FinS(Rlor(F,B),b.$1);
A4: dom b = Seg len b by FINSEQ_1:def 3;
A5: len b = card C by Th1;
A6: dom FinS(p,C) = Seg len FinS(p,C) by FINSEQ_1:def 3;
A7: for m st P[m] holds P[m+1]
proof
set f = FinS(p,C);
let m;
assume
A8: P[m];
A9: m<=m+1 by NAT_1:11;
assume
A10: m+1 in dom b;
then 1<=m+1 by FINSEQ_3:25;
then
A11: m+1 in Seg(m+1) by FINSEQ_1:1;
A12: dom p = C by A1,Th20;
A13: m+1<=len b by A10,FINSEQ_3:25;
then
A14: m<=len b by NAT_1:13;
A15: m by A18,A19,RFUNCT_3:69;
len(FinS(p,C)|(m+1)) = 1 by A18,A21,FINSEQ_1:59;
hence thesis by A23,A22,FINSEQ_1:40;
end;
case
A24: m<>0;
A25: Seg m c= Seg(m+1) by A9,FINSEQ_1:5;
A26: (f|(m+1))|m = (f|(m+1))|(Seg m) by FINSEQ_1:def 15
.= (f|Seg(m+1))|(Seg m) by FINSEQ_1:def 15
.= f|(Seg(m+1) /\ (Seg m)) by RELAT_1:71
.= f|(Seg m) by A25,XBOOLE_1:28
.= f|m by FINSEQ_1:def 15;
A27: 0+1<=m by A24,NAT_1:13;
then consider d be Element of C such that
A28: b.(m+1) \ b.m = {d} and
b.(m+1) = b.m \/ {d} and
A29: b.(m+1) \ {d} = b.m by A16,Th10;
A30: d in {d} by TARSKI:def 1;
then p.d = FinS(F,D).(m+1) by A1,A15,A27,A28,Th21
.= FinS(p,C).(m+1) by A1,Th24
.=(f|(m+1)).(m+1) by A4,A6,A5,A3,A10,A11,RFINSEQ:6;
then
A31: f|(m+1) = f|m ^ <*p.d*> by A17,A26,RFINSEQ:7;
d in dom p /\ b.(m+1) by A12,A28,A30,XBOOLE_0:def 4;
then
A32: d in dom(p|(b.(m+1))) by RELAT_1:61;
A33: (f|(m+1)) is non-increasing by RFINSEQ:20;
A34: dom(p|(b.(m+1))) = dom p /\ (b.(m+1)) by RELAT_1:61
.= b.(m+1) by A10,A12,Lm5,XBOOLE_1:28;
b.(m+1) is finite by A10,Lm5,FINSET_1:1;
then
f|(m+1), p|(b.(m+1)) are_fiberwise_equipotent by A8,A14,A27,A29,A31,A32
,FINSEQ_3:25,RFUNCT_3:65;
hence thesis by A34,A33,RFUNCT_3:def 13;
end;
end;
hence thesis;
end;
A35: dom B = Seg len B & len B = card C by Th1,FINSEQ_1:def 3;
A36: P[ 0 ] by FINSEQ_3:25;
for m holds P[m] from NAT_1:sch 2(A36,A7);
hence thesis by A2,A4,A35,A5;
end;
theorem
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
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom Rlor(F,B) = C by A1,A2,Th20;
set b = Co_Gen B;
A4: len b = card C by Th1;
A5: dom F = D by A1,PARTFUN1:def 2;
then
A6: dom(F-r) = D by VALUED_1:3;
then
A7: F-r is total by PARTFUN1:def 2;
(F-r)|D = F-r by A6,RELAT_1:68;
then
A8: len FinS(F-r,D) = card D by A6,RFUNCT_3:67;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
F|D = F by A5,RELAT_1:68;
then
A9: FinS(F-r,D) = FinS(F,D) - (card D |-> rr) by A5,RFUNCT_3:73;
A10: now
let c be Element of C;
assume c in dom Rlor(F-r,B);
defpred P[set] means $1 in dom b & c in b.$1;
A11: C = b.(len b) by Th3;
len b <> 0 by Th4;
then
A12: 0+1<=len b by NAT_1:13;
then
A13: 1 in dom b by FINSEQ_3:25;
len b in dom b by A12,FINSEQ_3:25;
then
A14: ex n be Nat st P[n] by A11;
consider mi be Nat such that
A15: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A14);
A16: 1<=mi by A15,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi - 1 as Element of NAT by FINSEQ_2:5;
A17: mi<=len b by A15,FINSEQ_3:25;
A18: mi r).1 = r by FUNCOP_1:7;
(Rlor(F-r,B)).c = FinS(F-r,D).1 & (Rlor(F,B)).c = FinS(F,D ).1 by A1,A2
,A7,A15,A21,Th21;
hence (Rlor(F-r,B)).c = (Rlor(F,B)).c - r by A9,A22,A23,VALUED_1:13
.= (Rlor(F,B) - r).c by A3,VALUED_1:3;
end;
case
mi <> 1;
then 1 r).(m1+1) = r by FUNCOP_1:7;
m1+1 in dom FinS(F-r,D) by A2,A8,A4,A15,FINSEQ_3:29;
hence (Rlor(F-r,B)).c = (Rlor(F,B)).c - r by A9,A25,A26,VALUED_1:13
.= (Rlor(F,B) - r).c by A3,VALUED_1:3;
end;
end;
hence (Rlor(F-r,B)).c = (Rlor(F,B) - r).c;
end;
dom(Rlor(F,B) - r) = C by A3,VALUED_1:3;
hence thesis by A2,A7,A10,Th20,PARTFUN1:5;
end;
theorem
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
proof
let F be PartFunc of D,REAL, A be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom F = D by A1,PARTFUN1:def 2;
dom(F|D) = dom F /\ D by RELAT_1:61
.= D by A3;
then
A4: FinS(F,D), F|D are_fiberwise_equipotent by RFUNCT_3:def 13;
Rlor(F,A), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then
A5: Rlor (F,A), F|D are_fiberwise_equipotent by A4,CLASSES1:76;
Rland(F,A), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th16;
then Rland(F,A), F|D are_fiberwise_equipotent by A4,CLASSES1:76;
hence Rland(F,A), F are_fiberwise_equipotent & Rlor(F,A), F
are_fiberwise_equipotent by A3,A5,RELAT_1:68;
hence thesis by CLASSES1:75;
end;