:: Functions and Finite Sequences of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received March 15, 1993
:: Copyright (c) 1993-2026 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, FINSEQ_1, RELAT_1, FINSET_1, CLASSES1,
ORDINAL4, CARD_1, ARYTM_3, FUNCT_2, XBOOLE_0, TARSKI, NAT_1, FUNCT_1,
ARYTM_1, XXREAL_0, CARD_3, VALUED_0, FUNCOP_1, FUNCT_4, RFINSEQ;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, XCMPLX_0, XREAL_0, NAT_1, REAL_1,
CLASSES1, SEQM_3, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_4, VALUED_0,
RVSUM_1, XXREAL_0;
constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQM_3,
FINSEQ_4, FINSOP_1, RVSUM_1, FUNCOP_1, CLASSES1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XREAL_0, NAT_1,
FINSEQ_1, FUNCOP_1, VALUED_0, CARD_1, INT_1, RELSET_1, RVSUM_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, SEQM_3, CLASSES1;
equalities RVSUM_1, FUNCOP_1, RELAT_1, FINSEQ_1;
expansions TARSKI, XBOOLE_0, SEQM_3, CLASSES1;
theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, NAT_1, FUNCT_1, FUNCT_2,
CARD_1, CARD_2, RVSUM_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_1, FINSEQ_4, XXREAL_0, FINSOP_1, FUNCOP_1, FUNCT_4, ORDINAL1,
XREAL_0, CLASSES1, INT_1, PARTFUN1;
schemes NAT_1, FINSEQ_1;
begin
reserve x,y for set,
n,m for Nat,
r,s for Real;
registration
let f be finite Relation, x be object;
cluster Coim(f,x) -> finite;
coherence
proof
Coim(f,x) c= dom f by RELAT_1:132;
hence thesis;
end;
end;
theorem Th1:
for f,g,h be FinSequence holds
f,g are_fiberwise_equipotent iff f^h, g^h are_fiberwise_equipotent
proof
let f,g,h be FinSequence;
thus f,g are_fiberwise_equipotent implies f^h, g^h are_fiberwise_equipotent
proof
assume
A1: f,g are_fiberwise_equipotent;
now
let y be object;
card Coim(f,y) = card Coim(g,y) by A1;
hence card Coim(f^h,y) = card Coim(g,y) + card Coim(h,y) by FINSEQ_3:57
.= card Coim(g^h,y) by FINSEQ_3:57;
end;
hence thesis;
end;
assume
A2: f^h,g^h are_fiberwise_equipotent;
now
let x be object;
A3: card Coim(f^h,x) = card Coim(f,x)+card Coim(h,x) & card Coim(g^h,x) =
card Coim(g,x)+card Coim(h,x) by FINSEQ_3:57;
card Coim(f^h,x) = card Coim(g^h,x) by A2;
hence card Coim(f,x) = card Coim(g,x) by A3;
end;
hence thesis;
end;
theorem
for f,g be FinSequence holds f^g, g^f are_fiberwise_equipotent
proof
let f,g be FinSequence;
let y be object;
thus card Coim(f^g,y) = card(g"{y})+ card(f"{y}) by FINSEQ_3:57
.= card Coim(g^f,y) by FINSEQ_3:57;
end;
theorem Th3:
for f,g be FinSequence st
f,g are_fiberwise_equipotent holds len f = len g & dom f = dom g
proof
let f,g be FinSequence;
A1: dom f = Seg len f by FINSEQ_1:def 3;
assume f,g are_fiberwise_equipotent;
then
A2: card(f"(rng f)) = card(g"(rng f)) & rng f = rng g by CLASSES1:75,78;
A3: Seg len g = dom g by FINSEQ_1:def 3;
thus len f = card(Seg len f) by FINSEQ_1:57
.= card(g"(rng g)) by A1,A2,RELAT_1:134
.= card(Seg len g) by A3,RELAT_1:134
.= len g by FINSEQ_1:57;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem Th4:
for f,g be FinSequence holds f,g are_fiberwise_equipotent iff
ex P be Permutation of dom g st f = g*P
proof
let f,g be FinSequence;
thus f,g are_fiberwise_equipotent implies ex P be Permutation of dom g st f
= g*P
proof
assume
A1: f,g are_fiberwise_equipotent;
then dom f = dom g by Th3;
hence thesis by A1,CLASSES1:80;
end;
given P be Permutation of dom g such that
A2: f = g*P;
dom g = {} implies dom g = {};
then rng P c= dom g & dom P = dom g by FUNCT_2:def 1,RELAT_1:def 19;
then dom f = dom g by A2,RELAT_1:27;
hence thesis by A2,CLASSES1:80;
end;
defpred P[Nat] means for X be finite set,F be Function st card(dom(F|X)) = $1
ex a be FinSequence st F|X, a are_fiberwise_equipotent;
Lm1: P[0]
proof
let X be finite set, F be Function;
assume
A1: card(dom(F|X)) = 0;
take A = {};
let x be object;
dom(F|X) = {} by A1;
hence card Coim(F|X,x) = card Coim(A,x) by RELAT_1:132,XBOOLE_1:3;
end;
Lm2: for n st P[n] holds P[n+1]
proof
let n be Nat;
assume
A1: P[n];
let X be finite set, F be Function;
reconsider dx = dom(F|X) as finite set;
set x = the Element of dx;
set Y = X\{x}, dy = dom(F|Y);
A2: dy = dom F /\ Y by RELAT_1:61;
A3: dx = dom F /\ X by RELAT_1:61;
A4: dy = dx \ {x}
proof
thus dy c= dx \ {x}
proof
let y be object;
assume
A5: y in dy;
then y in X \ {x} by A2,XBOOLE_0:def 4;
then
A6: not y in {x} by XBOOLE_0:def 5;
y in dom F by A2,A5,XBOOLE_0:def 4;
then y in dx by A2,A3,A5,XBOOLE_0:def 4;
hence thesis by A6,XBOOLE_0:def 5;
end;
let y be object;
assume
A7: y in dx \{x};
then ( not y in {x})& y in X by A3,XBOOLE_0:def 4,def 5;
then
A8: y in Y by XBOOLE_0:def 5;
y in dom F by A3,A7,XBOOLE_0:def 4;
hence thesis by A2,A8,XBOOLE_0:def 4;
end;
assume
A9: card dom(F|X) = n+1;
then {x} c= dx by CARD_1:27,ZFMISC_1:31;
then card(dom(F|Y)) = card dx - card {x} by A4,CARD_2:44
.= n+1-1 by A9,CARD_1:30
.= n;
then consider a be FinSequence such that
A10: F|Y, a are_fiberwise_equipotent by A1;
take A = a^<* F.x *>;
dx <> {} by A9;
then x in dx;
then
A11: x in dom F /\ X by RELAT_1:61;
then x in dom F by XBOOLE_0:def 4;
then
A12: {x} c= dom F by ZFMISC_1:31;
x in X by A11,XBOOLE_0:def 4;
then
A13: {x} c= X by ZFMISC_1:31;
now
let y be object;
A14: Y misses {x} by XBOOLE_1:79;
A15: (F|Y)"{y} \/ (F|{x})"{y} = (Y /\ F"{y}) \/ (F|{x})"{y} by FUNCT_1:70
.= (Y /\ F"{y}) \/ ({x} /\ F"{y}) by FUNCT_1:70
.= (Y \/ {x}) /\ F"{y} by XBOOLE_1:23
.= (X \/ {x}) /\ F"{y} by XBOOLE_1:39
.= X /\ F"{y} by A13,XBOOLE_1:12
.= (F|X)"{y} by FUNCT_1:70;
reconsider FF = <*F.x*>"{y} as finite set;
A16: card Coim(F|Y,y) = card Coim(a,y) by A10;
A17: dom(F|{x}) = {x} by A12,RELAT_1:62;
A18: dom<*F.x*> = {1} by FINSEQ_1:2,38;
A19: now
per cases;
case
A20: y = F.x;
A21: {x} c= (F|{x})"{y}
proof
let z be object;
A22: y in {y} by TARSKI:def 1;
assume
A23: z in {x};
then z = x by TARSKI:def 1;
then y = (F|{x}).z by A17,A20,A23,FUNCT_1:47;
hence thesis by A17,A23,A22,FUNCT_1:def 7;
end;
(F|{x})"{y} c= {x} by A17,RELAT_1:132;
then (F|{x})"{y} = {x} by A21;
then
A24: card((F|{x})"{y}) = 1 by CARD_1:30;
A25: {1} c= <*F.x*>"{y}
proof
let z be object;
A26: y in {y} by TARSKI:def 1;
assume
A27: z in {1};
then z = 1 by TARSKI:def 1;
then y = <*F.x*>.z by A20;
hence thesis by A18,A27,A26,FUNCT_1:def 7;
end;
<*F.x*>"{y} c= {1} by A18,RELAT_1:132;
then <*F.x*>"{y} = {1} by A25;
hence card((F|{x})"{y}) = card FF by A24,CARD_1:30;
end;
case
A28: y <> F.x;
A29: now
set z = the Element of <*F.x*>"{y};
assume
A30: <*F.x*>"{y} <> {};
then <*F.x*>.z in {y} by FUNCT_1:def 7;
then
A31: <*F.x*>.z = y by TARSKI:def 1;
z in {1} by A18,A30,FUNCT_1:def 7;
then z = 1 by TARSKI:def 1;
hence contradiction by A28,A31;
end;
now
set z = the Element of (F|{x})"{y};
assume
A32: (F|{x})"{y} <> {};
then (F|{x}).z in {y} by FUNCT_1:def 7;
then
A33: (F|{x}).z = y by TARSKI:def 1;
A34: z in {x} by A17,A32,FUNCT_1:def 7;
then z = x by TARSKI:def 1;
hence contradiction by A17,A28,A34,A33,FUNCT_1:47;
end;
hence card((F|{x})"{y}) = card FF by A29;
end;
end;
(F|Y)"{y} /\ (F|{x})"{y} = Y /\ (F"{y}) /\ (F|{x})"{y} by FUNCT_1:70
.= Y /\ F"{y} /\ ({x} /\ F"{y}) by FUNCT_1:70
.= F"{y} /\ Y /\ {x} /\ F"{y} by XBOOLE_1:16
.= F"{y} /\ (Y /\ {x}) /\ F"{y} by XBOOLE_1:16
.= {} /\ F"{y} by A14
.= {};
hence card Coim(F|X,y) = card((F|Y)"{y}) + card FF - card {} by A15,A19,
CARD_2:45
.= card Coim(A,y) by A16,FINSEQ_3:57;
end;
hence thesis;
end;
theorem
for F be Function, X be finite set
ex f be FinSequence st F|X, f are_fiberwise_equipotent
proof
let F be Function, X be finite set;
A1: card(dom(F|X)) = card(dom(F|X));
for n holds P[n] from NAT_1:sch 2(Lm1,Lm2);
hence thesis by A1;
end;
definition
let n be Nat, f be FinSequence;
func f /^ n -> FinSequence means
:Def1:
len it = len f - n & for m be Nat st
m in dom it holds it.m = f.(m+n) if n<=len f otherwise it = {};
existence
proof
thus n<=len f implies ex p1 be FinSequence st len p1 = len f - n & for m
be Nat st m in dom p1 holds p1.m = f.(m+n)
proof
assume n<=len f;
then reconsider k = len f - n as Element of NAT by NAT_1:21;
deffunc F(Nat)=f.($1+n);
consider p be FinSequence such that
A1: len p = k & for m be Nat st m in dom p holds p.m = F(m) from
FINSEQ_1:sch 2;
take p;
thus len p = len f - n by A1;
let m be Nat;
assume m in dom p;
hence thesis by A1;
end;
thus thesis;
end;
uniqueness
proof
let p1,p2 be FinSequence;
thus n<=len f & (len p1 = len f - n & for m be Nat st m in dom p1 holds p1
.m = f.(m+n)) & (len p2 = len f - n & for m be Nat st m in dom p2 holds p2.m =
f.(m+n)) implies p1 = p2
proof
assume that
n<=len f and
A2: len p1 = len f - n and
A3: for m be Nat st m in dom p1 holds p1.m = f.(m+n) and
A4: len p2 = len f - n and
A5: for m be Nat st m in dom p2 holds p2.m = f.(m+n);
A6: dom p1 = Seg len p1 & Seg len p2 = dom p2 by FINSEQ_1:def 3;
now
let m be Nat;
assume
A7: m in dom p1;
then p1.m = f.(m+n) by A3;
hence p1.m = p2.m by A2,A4,A5,A6,A7;
end;
hence thesis by A2,A4,FINSEQ_2:9;
end;
thus thesis;
end;
consistency;
end;
definition
let D be set, n be Nat, f be D-valued FinSequence;
redefine func f /^ n -> FinSequence of D; :: redefines /^ (RFINSEQ, definition)
coherence
proof
set p = f /^ n;
per cases;
suppose
A1: n<=len f;
then reconsider k = len f - n as Element of NAT by NAT_1:21;
A2: len p = k by A1,Def1;
rng p c= rng f
proof
let x be object;
assume x in rng p;
then consider m being Nat such that
A3: m in dom p and
A4: p.m = x by FINSEQ_2:10;
m<=len p by A3,FINSEQ_3:25;
then
A5: m+n<=len f by A2,XREAL_1:19;
A6: m<=m+n by NAT_1:11;
1<=m by A3,FINSEQ_3:25;
then 1<=m+n by A6,XXREAL_0:2;
then
A7: m+n in dom f by A5,FINSEQ_3:25;
p.m = f.(m+n) by A1,A3,Def1;
hence thesis by A4,A7,FUNCT_1:def 3;
end;
then rng p c= D by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
suppose len f < n;
then f /^ n = <*>D by Def1;
hence thesis;
end;
end;
end;
registration
let n be Nat, f be real-valued FinSequence;
cluster f /^ n -> real-valued;
coherence;
end;
Lm3: for n be Nat for f be FinSequence st len f<=n holds (f|n) = f
proof
let n be Nat;
let f be FinSequence;
A1: dom f = Seg len f by FINSEQ_1:def 3;
assume len f<=n;
then f|n = f|Seg n & dom f c= Seg n by A1,FINSEQ_1:5;
hence thesis by RELAT_1:68;
end;
theorem Th6:
for f be FinSequence, n,m be Nat holds
n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f
proof
let f be FinSequence, n,m be Nat;
assume that
A1: n in dom f and
A2: m in Seg n;
dom f = Seg len f & n<=len f by A1,FINSEQ_1:def 3,FINSEQ_3:25;
then
A4: Seg n c= dom f by FINSEQ_1:5;
then Seg n = dom f /\ Seg n by XBOOLE_1:28
.= dom(f|n) by RELAT_1:61;
hence thesis by A2,A4,FUNCT_1:47;
end;
theorem Th7:
for f be FinSequence, n be Nat st n + 1 = len f holds f = (f|n) ^ <*f.(n+1)*>
proof
let f be FinSequence, n be Nat;
assume
A1: n + 1 = len f;
set x = f.(n+1);
set fn = f|n;
A3: len fn = n by A1,FINSEQ_1:59,NAT_1:11;
A4: dom f = Seg len f by FINSEQ_1:def 3;
A5: n<=n+1 by NAT_1:11;
A6: now
let m be Nat;
assume
A7: m in dom f;
then
A8: 1<=m by A4,FINSEQ_1:1;
A9: m<=len f by A4,A7,FINSEQ_1:1;
now
per cases;
case
m = len f;
hence f.m = (fn^<*x*>).m by A1,A3,FINSEQ_1:42;
end;
case
m <> len f;
then m<n+1 by A1,A9,XXREAL_0:1;
then
A10: m<=n by NAT_1:13;
then 1<=n by A8,XXREAL_0:2;
then
A11: n in dom f by A1,A5,FINSEQ_3:25;
A12: Seg len fn = dom fn by FINSEQ_1:def 3;
A13: m in dom fn by A3,A8,A10,FINSEQ_3:25;
hence (fn^<*x*>).m = fn.m by FINSEQ_1:def 7
.= f.m by A3,A13,A11,A12,Th6;
end;
end;
hence f.m = (fn^<*x*>).m;
end;
len (fn^<*x*>) = n + len <*x*> by A3,FINSEQ_1:22
.= len f by A1,FINSEQ_1:40;
hence thesis by A6,FINSEQ_2:9;
end;
Th8A:
for D be non empty set, f be FinSequence of D, n be Nat holds
(f|n)^(f/^n) = f
proof
let D be non empty set, f be FinSequence of D,n be Nat;
set fn = f/^n;
now
per cases;
case
len f<n;
then f/^n = <*>D & f|n = f by Def1,Lm3;
hence thesis by FINSEQ_1:34;
end;
case
A1: n<=len f;
A2: dom f = Seg len f by FINSEQ_1:def 3;
A3: len (f|n) = n by A1,FINSEQ_1:59;
A4: len fn = len f - n by A1,Def1;
then
A5: len ((f|n)^(f/^n)) = n+(len f - n) by A3,FINSEQ_1:22
.= len f;
A6: dom(f|n) = Seg n by A3,FINSEQ_1:def 3;
now
let m be Nat;
assume
A7: m in dom f;
then
A8: m<=len f by A2,FINSEQ_1:1;
A9: 1<=m by A2,A7,FINSEQ_1:1;
now
per cases;
case
A10: m<=n;
then 1<=n by A9,XXREAL_0:2;
then
A11: n in dom f by A1,FINSEQ_3:25;
A12: m in Seg n by A9,A10;
hence ((f|n)^(f/^n)).m = (f|n).m by A6,FINSEQ_1:def 7
.= f.m by A12,A11,Th6;
end;
case
A13: n<m;
then max(0,m-n) = m-n by FINSEQ_2:4;
then reconsider k = m-n as Element of NAT by FINSEQ_2:5;
n+1<=m by A13,NAT_1:13;
then
A14: 1<=k by XREAL_1:19;
k<=len fn by A4,A8,XREAL_1:9;
then
A15: k in dom fn by A14,FINSEQ_3:25;
thus ((f|n) ^ (f/^n)).m = fn.k by A3,A5,A8,A13,FINSEQ_1:24
.= f.(k+n) by A1,A15,Def1
.= f.m;
end;
end;
hence ((f|n) ^ (f/^n)).m = f.m;
end;
hence thesis by A5,FINSEQ_2:9;
end;
end;
hence thesis;
end;
theorem Th8:
for f be FinSequence, n be Nat holds (f|n)^(f/^n) = f
proof
let f be FinSequence, n be Nat;
reconsider D = rng f \/ {1} as non empty set;
f is FinSequence of D by FINSEQ_1:def 4,XBOOLE_1:7;
hence thesis by Th8A;
end;
registration let f be FinSequence, n be Nat;
reduce (f|n)^(f/^n) to f;
reducibility by Th8;
end;
theorem
for R1,R2 be real-valued FinSequence st
R1,R2 are_fiberwise_equipotent holds Sum R1 = Sum R2
proof
let R1,R2 be real-valued FinSequence;
defpred P[Nat] means for f,g be real-valued FinSequence st f,g
are_fiberwise_equipotent & len f = $1 holds Sum f = Sum g;
assume
A1: R1,R2 are_fiberwise_equipotent;
A2: len R1 = len R1;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let f,g be real-valued FinSequence;
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
set a = f.(n+1);
A7: rng f = rng g by A5,CLASSES1:75;
0 qua Nat+1<=n+1 by NAT_1:13;
then n+1 in dom f by A6,FINSEQ_3:25;
then a in rng g by A7,FUNCT_1:def 3;
then consider m being Nat such that
A8: m in dom g and
A9: g.m = a by FINSEQ_2:10;
set gg = g/^m, gm = g|m;
m<=len g by A8,FINSEQ_3:25;
then
A10: len gm = m by FINSEQ_1:59;
A11: 1<=m by A8,FINSEQ_3:25;
then max(0,m-1) = m-1 by FINSEQ_2:4;
then reconsider m1 = m-1 as Element of NAT by FINSEQ_2:5;
A12: m = m1+1;
then m1<=m by NAT_1:11;
then
A13: Seg m1 c= Seg m by FINSEQ_1:5;
m in Seg m by A11;
then gm.m = a by A8,A9,Th6;
then
A14: gm = (gm|m1)^<*a*> by A10,A12,Th7;
set fn = f|n;
A15: g = (g|m)^(g/^m);
A16: gm|m1 = gm|(Seg m1)
.= (g|(Seg m))|(Seg m1)
.= g|((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|(Seg m1) by A13,XBOOLE_1:28
.= g|m1;
A17: f = fn ^ <*a*> by A6,Th7;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A5;
then
card(fn"{x}) + card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x})
by A14,A16,A17,FINSEQ_3:57
.= card(((g|m1)^<*a*>)"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+ card(<*a*>"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x}) + card((g/^m)"{x})+ card(<*a*>"{x})
.= card(((g|m1)^(g/^m))"{x})+ card(<*a*>"{x}) by FINSEQ_3:57;
hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
end;
then
A18: fn, (g|m1)^(g/^m) are_fiberwise_equipotent;
len fn = n by A6,FINSEQ_1:59,NAT_1:11;
then Sum fn = Sum((g|m1)^gg) by A4,A18;
hence Sum f = Sum((g|m1)^gg) + Sum <*a*> by A17,RVSUM_1:75
.= Sum(g|m1) + Sum gg+ Sum <*a*> by RVSUM_1:75
.= Sum(g|m1)+ Sum <*a*> + Sum gg
.= Sum gm + Sum gg by A14,A16,RVSUM_1:75
.= Sum g by A15,RVSUM_1:75;
end;
A19: P[0]
proof
let f,g be real-valued FinSequence;
assume f,g are_fiberwise_equipotent & len f = 0;
then
A20: len g = 0 & f = <*>REAL by Th3;
then g = <*>REAL;
hence thesis by A20;
end;
for n holds P[n] from NAT_1:sch 2(A19,A3);
hence thesis by A1,A2;
end;
definition
let R be real-valued FinSequence;
func MIM(R) -> FinSequence of REAL means
:Def2:
len it = len R & it.(len it) = R.(len R) &
for n be Nat st 1 <= n & n <= len it - 1 holds it.n = (R.n) - (R.(n+1));
existence
proof
per cases;
suppose
A1: len R = 0;
reconsider RR = R as FinSequence of REAL by RVSUM_1:145;
take a = RR;
thus len a = len R & a.(len a) = R.(len R);
let n be Nat;
assume 1<=n & n<=len a - 1;
hence thesis by A1;
end;
suppose
len R <> 0;
then 0<len R;
then 0 qua Nat+1<=len R by NAT_1:13;
then max(0,len R -1) = len R - 1 by FINSEQ_2:4;
then reconsider l = len R -1 as Element of NAT by FINSEQ_2:5;
defpred P[Nat,object] means $2 = R.$1 - R.($1+1);
set t = R.(len R);
A2: for n be Nat st n in Seg l ex x be Element of REAL st P[n,x]
proof let n be Nat;
assume n in Seg l;
consider x being Real such that
A3: P[n,x];
reconsider x as Element of REAL by XREAL_0:def 1;
take x;
thus thesis by A3;
end;
consider p be FinSequence of REAL such that
A4: dom p = Seg l & for n be Nat st n in Seg l holds P[n,p.n] from
FINSEQ_1:sch 5(A2);
reconsider t as Element of REAL by XREAL_0:def 1;
take a = p^<*t*>;
thus
A5: len a = len p + len <*t*> by FINSEQ_1:22
.= l+len <*t*> by A4,FINSEQ_1:def 3
.= l+1 by FINSEQ_1:39
.= len R;
hence a.(len a) = a.(l+1) .= a.(len p +1) by A4,FINSEQ_1:def 3
.= R.(len R) by FINSEQ_1:42;
let n be Nat;
assume 1<=n & n<=len a - 1;
then
A6: n in Seg l by A5;
then p.n = R.n - R.(n+1) by A4;
hence thesis by A4,A6,FINSEQ_1:def 7;
end;
end;
uniqueness
proof
let p1,p2 be FinSequence of REAL;
assume that
A7: len p1 = len R and
A8: p1.(len p1) = R.(len R) and
A9: for n be Nat st 1<=n & n<=len p1 - 1 holds p1.n = R.n - R.(n+1) and
A10: len p2 = len R and
A11: p2.(len p2) = R.(len R) and
A12: for n be Nat st 1<=n & n<=len p2 - 1 holds p2.n = R.n - R.(n+1);
A13: dom p1 = Seg len R by A7,FINSEQ_1:def 3;
now
let n be Nat;
set r = R.n;
assume
A14: n in dom p1;
then
A15: 1<=n by A13,FINSEQ_1:1;
A16: n<=len R by A13,A14,FINSEQ_1:1;
now
per cases;
case
n = len R;
hence p1.n = p2.n by A7,A8,A10,A11;
end;
case
A17: n <> len R;
set s = R.(n+1);
n<len R by A16,A17,XXREAL_0:1;
then n+1<=len R by NAT_1:13;
then
A18: n<=len R - 1 by XREAL_1:19;
then p1.n = r-s by A7,A9,A15;
hence p1.n = p2.n by A10,A12,A15,A18;
end;
end;
hence p1.n = p2.n;
end;
hence thesis by A7,A10,FINSEQ_2:9;
end;
end;
theorem Th10:
for R be real-valued FinSequence, n be Nat st
len R = n+2 holds MIM(R|(n+1)) = MIM(R)|n ^ <* R.(n+1) *>
proof
let R be real-valued FinSequence, n;
assume that
A1: len R = n+2;
set s = R.(n+1);
set f1 = R|(n+1), m1 = MIM(f1), mf = MIM(R), fn = mf|n;
A3: 0 qua Nat+1<=n+1 by NAT_1:13;
A4: n+1+1 = n+(1+1);
then n+1<=n+2 by NAT_1:11;
then
A5: Seg len R = dom R & n+1 in Seg(n+2) by A3,FINSEQ_1:def 3;
A6: len f1 = n+1 by A1,A4,FINSEQ_1:59,NAT_1:11;
then
A7: len MIM(f1) = n+1 by Def2;
then
A8: dom m1 = Seg(n+1) by FINSEQ_1:def 3;
n+1 in Seg(n+1) by A3;
then f1.(n+1) = s by A1,A5,Th6;
then
A9: m1.(n+1) = s by A6,A7,Def2;
A10: Seg len fn = dom fn by FINSEQ_1:def 3;
A11: Seg len mf = dom mf by FINSEQ_1:def 3;
A12: len mf = n+2 by A1,Def2;
then
A13: len fn = n by FINSEQ_1:59,NAT_1:11;
A14: n<=n+2 by NAT_1:11;
A15: now
let m be Nat;
assume
A16: m in dom m1;
then
A17: 1<=m by A8,FINSEQ_1:1;
A18: m<=n+1 by A8,A16,FINSEQ_1:1;
now
per cases;
case
m = n+1;
hence m1.m = (fn^<*s*>).m by A13,A9,FINSEQ_1:42;
end;
case
m <> n+1;
then
A19: m<n+1 by A18,XXREAL_0:1;
then
A20: m<=n by NAT_1:13;
then
A21: m in Seg n by A17;
set r2 = R.(m+1);
set r1 = R.m;
A22: len mf -1 = n+1 by A12;
1<=n by A17,A20,XXREAL_0:2;
then n in Seg(n+2) by A14;
then fn.m = mf.m by A12,A11,A21,Th6;
then
A23: r1 - r2 = fn.m by A17,A18,A22,Def2
.= (fn^<*s*>).m by A13,A10,A21,FINSEQ_1:def 7;
1<=m+1 & m+1<=n+1 by A19,NAT_1:11,13;
then m+1 in Seg(n+1);
then
A24: f1.(m+1) = r2 by A1,A5,Th6;
len m1 -1 = n & f1.m = r1 by A1,A7,A5,A8,A16,Th6;
hence m1.m = (fn^<*s*>).m by A17,A20,A23,A24,Def2;
end;
end;
hence m1.m = (fn^<*s*>).m;
end;
len(fn^<*s*>) = n + len <*s*> by A13,FINSEQ_1:22
.= n+1 by FINSEQ_1:40;
hence thesis by A7,A15,FINSEQ_2:9;
end;
theorem Th11:
for R be real-valued FinSequence, r,s be Real, n be Nat
st len R = n+2 & R.(n+1) = r & R.(n+2) = s holds
MIM(R) = MIM(R)|n ^ <* r-s,s *>
proof
let R be real-valued FinSequence, r,s,n;
set mf = MIM(R), nf = mf|n;
assume that
A1: len R = n+2 and
A2: R.(n+1) = r and
A3: R.(n+2) = s;
A4: len mf = n+2 by A1,Def2;
then
A5: dom mf = Seg(n+2) by FINSEQ_1:def 3;
A6: n+(1+1) = n+1+1;
then n+1<=n+2 by NAT_1:11;
then
A7: n<n+2 by NAT_1:13;
A8: len nf = n by A4,FINSEQ_1:59,NAT_1:11;
then len (nf^<* r-s,s *>) = n + len <* r-s,s *> by FINSEQ_1:22;
then
A9: len(nf^<* r-s,s *>) = n+2 by FINSEQ_1:44;
A10: n<=n+2 by NAT_1:11;
now
let m be Nat;
assume
A11: m in dom mf;
then
A12: 1<=m by A5,FINSEQ_1:1;
A13: m<=n+2 by A5,A11,FINSEQ_1:1;
now
per cases;
case
A14: m = n+2;
hence mf.m = s by A1,A3,A4,Def2
.= <* r-s,s *>.(n+2-n)
.= (nf ^ <* r-s,s *>).m by A8,A9,A7,A14,FINSEQ_1:24;
end;
case
m <> n+2;
then m<n+2 by A13,XXREAL_0:1;
then
A15: m<=n+1 by A6,NAT_1:13;
A16: len mf - 1 = n+1 by A4;
now
per cases;
case
A17: m = n+1;
then
A18: n<m by NAT_1:13;
thus mf.m = r - s by A2,A3,A6,A12,A16,A17,Def2
.= <* r-s,s *>.(n+1-n)
.= (nf ^ <* r-s,s *>).m by A8,A9,A13,A17,A18,FINSEQ_1:24;
end;
case
m <> n+1;
then m<n+1 by A15,XXREAL_0:1;
then
A19: m<=n by NAT_1:13;
then
A20: m in Seg n by A12;
1<=n by A12,A19,XXREAL_0:2;
then
A21: n in Seg(n+2) by A10;
A22: dom nf = Seg len nf by FINSEQ_1:def 3;
dom mf = Seg len mf by FINSEQ_1:def 3;
hence mf.m = nf.m by A4,A20,A21,Th6
.= (nf ^ <* r-s,s *>).m by A8,A20,A22,FINSEQ_1:def 7;
end;
end;
hence mf.m = (nf ^ <* r-s,s *>).m;
end;
end;
hence mf.m = (nf ^ <* r-s,s *>).m;
end;
hence thesis by A4,A9,FINSEQ_2:9;
end;
theorem Th12:
MIM( <*>REAL ) = <*>REAL
proof
set o = <*>REAL, mo = MIM(o);
len mo = len o by Def2;
hence thesis;
end;
theorem Th13:
for r be Real holds MIM(<*r*>) = <*r*>
proof
let r be Real;
set f = <*r*>;
A1: len f = 1 by FINSEQ_1:40;
then
A2: len MIM(f) = 1 by Def2;
then
A3: dom MIM(f) = Seg 1 by FINSEQ_1:def 3;
now
let n be Nat;
assume n in dom MIM(f);
then n = 1 by A3,FINSEQ_1:2,TARSKI:def 1;
hence MIM(f).n = f.n by A1,A2,Def2;
end;
hence thesis by A1,A2,FINSEQ_2:9;
end;
theorem
for r,s be Real holds MIM(<*r,s*>) = <*r-s,s*>
proof
let r,s be Real;
reconsider r,s as Element of REAL by XREAL_0:def 1;
set f = <*r,s*>;
A1: len f = 2 & f.1 = r by FINSEQ_1:44;
A2: f.2 = s;
0 qua Nat+2 = 2 & 0 qua Nat +1 = 1;
then MIM(f) = MIM(f)|0 ^ <*r-s,s*> by A1,A2,Th11;
hence thesis by FINSEQ_1:34;
end;
theorem
for R be real-valued FinSequence, n be Nat holds MIM(R) /^ n = MIM(R/^n)
proof
let R be real-valued FinSequence,n;
set mf = MIM(R), fn = R/^n, mn = MIM(fn);
A1: len mf = len R by Def2;
A2: len mn = len fn by Def2;
now
per cases;
case
A3: len R<n;
then mf /^ n = <*>REAL by A1,Def1;
hence thesis by A3,Def1,Th12;
end;
case
A4: n<=len R;
then
A5: len(mf/^n) = len R - n by A1,Def1;
A6: len mn = len fn by Def2;
then
A7: dom mn = Seg len fn by FINSEQ_1:def 3;
A8: Seg len(mf/^n) = dom(mf/^n) by FINSEQ_1:def 3;
A9: len fn = len R - n by A4,Def1;
A10: Seg len fn = dom fn by FINSEQ_1:def 3;
now
let m be Nat;
set r1 = R.(m+n);
assume
A11: m in dom mn;
then
A12: 1<=m by A7,FINSEQ_1:1;
A13: m<=len fn by A7,A11,FINSEQ_1:1;
A14: fn.m = r1 by A4,A10,A7,A11,Def1;
m<=m+n by NAT_1:11;
then
A15: 1<=m+n by A12,XXREAL_0:2;
now
per cases;
case
A16: m = len fn;
thus (mf/^n).m = mf.(m+n) by A1,A4,A5,A9,A8,A7,A11,Def1
.= r1 by A1,A9,A16,Def2
.= mn.m by A6,A14,A16,Def2;
end;
case
m <> len fn;
then m<len fn by A13,XXREAL_0:1;
then
A17: m+1<=len fn by NAT_1:13;
then
A18: m<=len fn - 1 by XREAL_1:19;
set r2 = R.(m+1+n);
A19: m+1+n = m+n+1;
1<=m+1 by NAT_1:11;
then m+1 in dom fn by A17,FINSEQ_3:25;
then
A20: fn.(m+1) = r2 by A4,Def1;
m+1+n<=len R by A9,A17,XREAL_1:19;
then
A21: m+n<=len R - 1 by A19,XREAL_1:19;
thus (mf/^n).m = mf.(m+n) by A1,A4,A5,A9,A8,A7,A11,Def1
.= r1-r2 by A1,A15,A19,A21,Def2
.= mn.m by A2,A12,A14,A18,A20,Def2;
end;
end;
hence (mf/^n).m = mn.m;
end;
hence thesis by A5,A9,A6,FINSEQ_2:9;
end;
end;
hence thesis;
end;
theorem Th16:
for R be real-valued FinSequence st len R <> 0 holds Sum MIM(R) = R. 1
proof
defpred P[Nat] means for R be real-valued FinSequence st len R <> 0 &
len R = $1 holds Sum MIM(R) = R.1;
let R be real-valued FinSequence;
assume
A1: len R <> 0;
A2: for n st P[n] holds P[n+1]
proof
let n;
assume
A3: P[n];
let R be real-valued FinSequence;
assume that
len R <> 0 and
A4: len R = n+1;
now
per cases;
case
A5: n = 0;
A6: R.1 in REAL by XREAL_0:def 1;
A7: R = <*R.1*> by A4,A5,FINSEQ_1:40;
then MIM(R) = R by Th13;
hence thesis by A7,A6,FINSOP_1:11;
end;
case
n <> 0;
then 0<n;
then 0 qua Nat+1<=n by NAT_1:13;
then max(0,n-1) = n-1 by FINSEQ_2:4;
then reconsider n1 = n-1 as Element of NAT by FINSEQ_2:5;
A8: 0 qua Nat+1<=n1+1 by NAT_1:11;
then
A9: Seg len R = dom R & 1 in Seg(n1+1) by FINSEQ_1:def 3;
n1+2 = n1+1+1;
then n1+1<=n1+2 by NAT_1:11;
then
A10: n1+1 in Seg(n1+2) by A8;
set f1 = R|(n1+1);
set s = R.(n1+2);
set r = R.(n1+1);
A11: n1+2 = len R by A4;
A12: len f1 = n1+1 by A4,FINSEQ_1:59,NAT_1:11;
thus Sum MIM(R) = Sum((MIM(R)|n1) ^ <* r-s,s *>) by A4,Th11
.= Sum(MIM(R)|n1) + Sum(<* r-s,s *>) by RVSUM_1:75
.= Sum(MIM(R)|n1) + (r-s + s) by RVSUM_1:77
.= Sum((MIM(R)|n1) ^<*r*>) by RVSUM_1:74
.= Sum MIM(f1) by A11,Th10
.= f1.1 by A3,A12
.= R.1 by A4,A10,A9,Th6;
end;
end;
hence thesis;
end;
A13: P[0];
for n holds P[n] from NAT_1:sch 2(A13,A2);
hence thesis by A1;
end;
theorem
for R be real-valued FinSequence, n be Nat st n<len R
holds Sum MIM(R/^n) = R.(n+1)
proof
let R be real-valued FinSequence,n;
assume
A1: n<len R;
then
A2: len(R/^n) = len R - n by Def1;
n+1<=len R by A1,NAT_1:13;
then 1<=len R - n by XREAL_1:19;
then
A3: 1 in dom(R/^n) by A2,FINSEQ_3:25;
len(R/^n) <> 0 by A1,A2;
hence Sum MIM(R/^n) = (R/^n).1 by Th16
.= R.(n+1) by A1,A3,Def1;
end;
definition
let IT be real-valued FinSequence;
redefine attr IT is non-increasing means :: redefines non-increasing (VALUED_0, definition)
:Def3:
for n be Nat st n in dom IT & n+1 in dom IT holds
IT.n >= IT.(n+1);
compatibility
proof
thus IT is non-increasing implies for n be Nat st n in dom IT &
n+1 in dom IT holds IT.n >= IT.(n+1)
proof
assume
A1: IT is non-increasing;
let n be Nat such that
A2: n in dom IT & n+1 in dom IT;
n+(0 qua Nat) <= n+1 by XREAL_1:6;
hence thesis by A1,A2;
end;
assume
A3: for n be Nat st n in dom IT & n+1 in dom IT holds IT.n
>= IT.(n+1);
let m, n be Nat such that
A4: m in dom IT and
A5: n in dom IT & m <= n;
defpred P[Nat] means $1 in dom IT & m <= $1 implies IT.m >= IT.$1;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k] and
A8: k+1 in dom IT;
assume m <= k+1;
then
A9: m < k+1 or m = k+1 by XXREAL_0:1;
per cases by A9,NAT_1:13;
suppose
A10: m <= k;
k+(0 qua Nat) <= k+1 & k+1 <= len IT by A8,FINSEQ_3:25,XREAL_1:6;
then
A11: k <= len IT by XXREAL_0:2;
1 <= m by A4,FINSEQ_3:25;
then
A12: 1 <= k by A10,XXREAL_0:2;
then k in dom IT by A11,FINSEQ_3:25;
then IT.k >= IT.(k+1) by A3,A8;
hence thesis by A7,A10,A12,A11,FINSEQ_3:25,XXREAL_0:2;
end;
suppose
m = k+1;
hence thesis;
end;
end;
A13: P[0] by FINSEQ_3:24;
for k being Nat holds P[k] from NAT_1:sch 2(A13,A6);
hence thesis by A5;
end;
end;
registration
cluster <*>REAL -> non-increasing non-decreasing;
coherence;
end;
registration
cluster non-increasing non-decreasing for FinSequence of REAL;
existence
proof
take <*>REAL;
thus thesis;
end;
end;
registration
cluster non-increasing non-decreasing for real-valued FinSequence;
existence
proof
take <*>REAL;
thus thesis;
end;
end;
theorem Th18:
for R be real-valued FinSequence st len R = 0 or len R = 1 holds
R is non-increasing
proof
let R be real-valued FinSequence;
assume
A1: len R = 0 or len R = 1;
now
per cases by A1;
case
len R = 0;
then R = <*>REAL;
then for n st n in dom R & n+1 in dom R holds R.n>=R.(n+1);
hence thesis;
end;
case
len R = 1;
then
A2: dom R = {1} by FINSEQ_1:2,def 3;
now
let n;
assume that
A3: n in dom R and
A4: n+1 in dom R;
n = 1 by A2,A3,TARSKI:def 1;
hence R.n>=R.(n+1) by A2,A4,TARSKI:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th19:
for R be real-valued FinSequence holds R is non-increasing iff
for n,m be Nat st n in dom R & m in dom R & n<m holds R.n>=R.m
proof
let R be real-valued FinSequence;
thus R is non-increasing implies
for n,m being Nat st n in dom R & m in dom R & n<m
holds R.n>=R.m;
assume
A1: for n,m being Nat st n in dom R & m in dom R & n<m holds R.n>=R.m;
let n;
n<n+1 by NAT_1:13;
hence thesis by A1;
end;
theorem
for R be non-increasing real-valued FinSequence, n
holds R|n is non-increasing FinSequence of REAL by FINSEQ_1:106;
theorem
for R be non-increasing real-valued FinSequence, n holds
R /^ n is non-increasing
proof
let f be non-increasing real-valued FinSequence, n;
set fn = f /^ n;
now
let m;
assume that
A1: m in dom fn and
A2: m+1 in dom fn;
A3: m<=m+n by NAT_1:11;
1<=m by A1,FINSEQ_3:25;
then
A4: 1<=m+n by A3,XXREAL_0:2;
A5: 1<=m+n+1 by NAT_1:11;
A6: m+1<=len fn by A2,FINSEQ_3:25;
set r = fn.m, s = fn.(m+1);
A7: m+1+n = m+n+1;
A8: m<=len fn by A1,FINSEQ_3:25;
now
per cases;
case
A9: n<=len f;
then
A10: len fn = len f - n by Def1;
then m+n<=len f by A8,XREAL_1:19;
then
A11: m+n in dom f by A4,FINSEQ_3:25;
m+n+1<=len f by A6,A7,A10,XREAL_1:19;
then
A12: m+n+1 in dom f by A5,FINSEQ_3:25;
r = f.(m+n) & s = f.(m+n+1) by A1,A2,A7,A9,Def1;
hence r>=s by A11,A12,Def3;
end;
case
len f<n;
then fn = <*>REAL by Def1;
hence r>=s;
end;
end;
hence r>=s;
end;
hence thesis;
end;
Lm4: for f,g be non-increasing real-valued FinSequence, n st len f = n+1 &
len f = len g &
f,g are_fiberwise_equipotent holds f.(len f) = g.(len g) & f|n, g|n
are_fiberwise_equipotent
proof
let f,g be non-increasing real-valued FinSequence, n;
assume that
A1: len f = n+1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent;
set r = f.(n+1), s = g.(n+1);
A4: 0 qua Nat+1<=n+1 by NAT_1:13;
then
A5: n+1 in dom f by A1,FINSEQ_3:25;
A6: f = (f|n)^<*r*> by A1,Th7;
A7: n+1 in dom g by A1,A2,A4,FINSEQ_3:25;
A8: now
A9: rng f = rng g by A3,CLASSES1:75;
assume
A10: r <> s;
now
per cases by A10,XXREAL_0:1;
case
A11: r>s;
s in rng f by A7,A9,FUNCT_1:def 3;
then consider m be Nat such that
A12: m in dom f and
A13: f.m = s by FINSEQ_2:10;
A14: m<=len f by A12,FINSEQ_3:25;
now
per cases;
case
m = len f;
hence contradiction by A1,A11,A13;
end;
case
m <> len f;
then m<n+1 by A1,A14,XXREAL_0:1;
hence contradiction by A5,A11,A12,A13,Th19;
end;
end;
hence contradiction;
end;
case
A15: r<s;
r in rng g by A5,A9,FUNCT_1:def 3;
then consider m be Nat such that
A16: m in dom g and
A17: g.m = r by FINSEQ_2:10;
A18: m<=len g by A16,FINSEQ_3:25;
now
per cases;
case
m = len g;
hence contradiction by A1,A2,A15,A17;
end;
case
m <> len g;
then m<n+1 by A1,A2,A18,XXREAL_0:1;
hence contradiction by A7,A15,A16,A17,Th19;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence f.(len f) = g.(len g) by A1,A2;
A19: g = (g|n)^<*r*> by A1,A2,A8,Th7;
now
let x be object;
card Coim(f|n,x) + card(<*r*>"{x}) = card Coim(f,x) by A6,FINSEQ_3:57
.= card Coim(g,x) by A3
.= card Coim(g|n,x) + card(<*r*>"{x}) by A19,FINSEQ_3:57;
hence card Coim(f|n,x) = card Coim(g|n,x);
end;
hence thesis;
end;
defpred P[Nat] means for R be real-valued FinSequence st $1 = len R
ex b be non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent;
Lm5: P[0]
proof
let R be real-valued FinSequence;
assume len R = 0;
then reconsider a = R as non-increasing real-valued FinSequence by Th18;
reconsider a as non-increasing FinSequence of REAL by RVSUM_1:145;
take a;
thus thesis;
end;
Lm6: for n st P[n] holds P[n+1]
proof
let n;
assume
A1: P[n];
let R be real-valued FinSequence;
set fn = R|(Seg n);
A2: fn = R|n;
set q = R.(n+1);
reconsider fn as FinSequence by FINSEQ_1:15;
rng fn c= rng R by RELAT_1:70;
then rng fn c= REAL by XBOOLE_1:1;
then reconsider fn as FinSequence of REAL by FINSEQ_1:def 4;
n<=n+1 by NAT_1:11;
then
A3: dom fn = dom R /\ Seg n & Seg n c= Seg(n+1) by FINSEQ_1:5,RELAT_1:61;
A4: n in NAT by ORDINAL1:def 12;
assume
A5: n+1 = len R;
then dom R = Seg(n+1) by FINSEQ_1:def 3;
then dom fn = Seg n by A3,XBOOLE_1:28;
then
A6: len fn = n by FINSEQ_1:def 3,A4;
then consider a be non-increasing FinSequence of REAL such that
A7: fn,a are_fiberwise_equipotent by A1;
A8: len fn = len a by A7,Th3;
A9: Seg len a = dom a by FINSEQ_1:def 3;
now
per cases;
case
A10: for t be Real st t in rng a holds q<=t;
set b = a^<*q*>;
A11: len b = n + len <*q*> by A6,A8,FINSEQ_1:22
.= n+1 by FINSEQ_1:39;
now
let m;
assume that
A12: m in dom b and
A13: m+1 in dom b;
A14: 1<=m+1 by A13,FINSEQ_3:25;
set r = b.m, s = b.(m+1);
A15: 1<=m by A12,FINSEQ_3:25;
A16: m+1<=len b by A13,FINSEQ_3:25;
then m<=n+1-1 by A11,XREAL_1:19;
then m in Seg n by A15;
then
A17: m in dom a by A6,A8,FINSEQ_1:def 3;
then
A18: r = a.m by FINSEQ_1:def 7;
A19: a.m in rng a by A17,FUNCT_1:def 3;
reconsider b as FinSequence of REAL by RVSUM_1:145;
per cases;
suppose
m+1 = len b;
then s = q by A6,A8,A11,FINSEQ_1:42;
hence r>=s by A10,A18,A19;
end;
suppose
m+1 <> len b;
then m+1<len b by A16,XXREAL_0:1;
then m+1<=n+1-1 by A11,NAT_1:13;
then m+1 in Seg n by A14;
then
A20: m+1 in dom a by A6,A8,FINSEQ_1:def 3;
then a.(m+1) = s by FINSEQ_1:def 7;
hence r>=s by A17,A18,A20,Def3;
end;
end;
then reconsider b as non-increasing FinSequence of REAL
by Def3,RVSUM_1:145;
take b;
fn^<*q*> = R by A5,A2,Th7;
hence R,b are_fiberwise_equipotent by A7,Th1;
end;
case
A21: ex t be Real st t in rng a & not q<=t;
defpred Q[Nat] means $1 in dom a & for r st r = a.$1 holds r<q;
A22: ex k be Nat st Q[k]
proof
consider t be Real such that
A23: t in rng a and
A24: t<q by A21;
consider k be Nat such that
A25: k in dom a and
A26: a.k = t by A23,FINSEQ_2:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus k in dom a by A25;
let r;
assume r = a.k;
hence thesis by A24,A26;
end;
consider mi be Nat such that
A27: Q[mi] & for m be Nat st Q[m] holds mi <= m from NAT_1:sch 5(A22
);
1<=mi by A27,FINSEQ_3:25;
then max(0,mi-1) = mi-1 by FINSEQ_2:4;
then reconsider k = mi-1 as Element of NAT by FINSEQ_2:5;
mi<mi+1 by NAT_1:13;
then
A28: k<=mi by XREAL_1:19;
A29: mi<=len a by A27,FINSEQ_3:25;
then
A30: k<=len a by A28,XXREAL_0:2;
then
A31: len(a/^k) = len a - k by Def1;
A32: dom((a|k)^<*q*>) = Seg len((a|k)^<*q*>) by FINSEQ_1:def 3;
A33: dom (a|k) c= dom((a|k)^<*q*>) by FINSEQ_1:26;
set ak = a/^k, b = (a|k)^<*q*>^ak;
A34: dom (a|k) = Seg len (a|k) by FINSEQ_1:def 3;
A35: len(a|k) = k by A29,A28,FINSEQ_1:59,XXREAL_0:2;
then
A36: len((a|k)^<*q*>) = k+len <*q*> by FINSEQ_1:22
.= k+1 by FINSEQ_1:39;
then
A37: len b = k+1 + len(a/^k) by FINSEQ_1:22;
k+1<=len a by A27,FINSEQ_3:25;
then
A38: 1<=len(a/^k) by A31,XREAL_1:19;
now
let m;
assume that
A39: m in dom b and
A40: m+1 in dom b;
A41: 1<=m+1 by A40,FINSEQ_3:25;
A42: m+1<=len b by A40,FINSEQ_3:25;
set r = b.m, s = b.(m+1);
A43: 1<=m by A39,FINSEQ_3:25;
A44: m<=len b by A39,FINSEQ_3:25;
now
per cases;
case
A45: m+1<=k;
dom(a|k) c= dom((a|k)^(a/^k)) by FINSEQ_1:26; then
A46: dom(a|k) c= dom a;
A47: dom a = Seg len a by FINSEQ_1:def 3;
m<=k by A45,NAT_1:13; then
A48: m in Seg k by A43;
1<=k by A41,A45,XXREAL_0:2; then
A49: k in dom a by A30,A47; then
A50: a.m = (a|k).m by A48,Th6;
A51: m+1 in Seg k by A41,A45; then
A52: a.(m+1) = (a|k).(m+1) by A49,Th6;
A53: b.(m+1) = ((a|k)^<*q*>).(m+1) by A35,A34,A33,A51,FINSEQ_1:def 7
.= a.(m+1) by A35,A34,A51,A52,FINSEQ_1:def 7;
b.m = ((a|k)^<*q*>).m by A35,A34,A33,A48,FINSEQ_1:def 7
.= a.m by A35,A34,A48,A50,FINSEQ_1:def 7;
hence r>=s by A35,A34,A48,A51,A53,A46,Def3;
end;
case
k<m+1;
then
A54: k<=m by NAT_1:13;
now
per cases;
case
A55: k = m;
then m+1 in dom((a|k)^<*q*>) by A36,A32,FINSEQ_1:4;
then
A56: b.(m+1) = ((a|k)^<*q*>).(k+1) by A55,FINSEQ_1:def 7
.= q by A35,FINSEQ_1:42;
A57: m in Seg k by A43,A55;
A58: k in dom a by A9,A30,A43,A55; then
A59: a.m = (a|k).m by A57,Th6;
A60: b.m = ((a|k)^<*q*>).m by A35,A34,A33,A57,FINSEQ_1:def 7
.= a.m by A35,A34,A57,A59,FINSEQ_1:def 7;
now
assume s>r;
then for t be Real st t = a.k holds t<q
by A55,A60,A56;
then mi<=k by A27,A58;
hence contradiction by XREAL_1:44;
end;
hence r>=s;
end;
case
k <> m;
then k<m by A54,XXREAL_0:1;
then
A61: k+1<=m by NAT_1:13;
then
A62: k+1<m+1 by NAT_1:13;
max(0,m-(k+1)) = m-(k+1) by A61,FINSEQ_2:4;
then reconsider l = m-(k+1) as Element of NAT by FINSEQ_2:5;
A63: l+1 = m+1-(k+1);
then
A64: l+1<=len b -(k+1) by A42,XREAL_1:13;
l<=l+1 by NAT_1:11;
then
A65: l<=len(a/^k) by A37,A64,XXREAL_0:2;
1<=l+1 by NAT_1:11;
then
A66: l+1 in dom(a/^k) by A37,A64,FINSEQ_3:25;
1<=l+1+k by A39,FINSEQ_3:25;
then
A67: k+l+1<=len a by A31,A37,A64,XREAL_1:19;
then
A68: k+l+1 in dom a by A43,FINSEQ_3:25;
k+l<=k+l+1 by NAT_1:11;
then
A69: k+l<=len a by A67,XXREAL_0:2;
A70: k+(l+1) <=len a by A31,A37,A64,XREAL_1:19;
now
per cases;
case
A71: k+1 = m;
then m in Seg (k+1) by A43; then
A72: b.m = ((a|k)^<*q*>).(k+1) by A36,A32,A71,FINSEQ_1:def 7
.= q by A35,FINSEQ_1:42;
A73: 1 in dom(a/^k) by A38,FINSEQ_3:25;
b.(m+1) = (a/^k).(k+1+1 - (k+1)) by A36,A42,A62,A71,
FINSEQ_1:24
.= a.mi by A30,A73,Def1;
hence r>=s by A27,A72;
end;
case
k+1 <> m;
then
A74: k+1<m by A61,XXREAL_0:1;
then k+1+1<=m by NAT_1:13;
then
A75: 1<=l by XREAL_1:19;
then
A76: l in dom(a/^k) by A65,FINSEQ_3:25;
l<=k+l by NAT_1:11;
then 1<=k+l by A75,XXREAL_0:2;
then
A77: k+l in dom a by A69,FINSEQ_3:25;
A78: b.m = (a/^k).l by A36,A44,A74,FINSEQ_1:24
.= a.(k+l) by A30,A76,Def1;
b.(m+1) = (a/^k).(l+1) by A36,A42,A62,A63,FINSEQ_1:24
.= a.(k+l+1) by A30,A66,A70,Def1;
hence r>=s by A68,A78,A77,Def3;
end;
end;
hence r>=s;
end;
end;
hence r>=s;
end;
end;
hence r>=s;
end;
then reconsider b as non-increasing FinSequence of REAL
by Def3,RVSUM_1:145;
take b;
now
let x be object;
A79: card Coim(fn,x) = card Coim(a,x) by A7;
thus card Coim(b,x) = card (((a|k)^<*q*>)"{x}) + card(ak"{x}) by
FINSEQ_3:57
.= card((a|k)"{x}) + card(<*q*>"{x}) + card(ak"{x}) by FINSEQ_3:57
.= card((a|k)"{x}) + card(ak"{x}) + card(<*q*>"{x})
.= card(((a|k)^ak)"{x}) + card(<*q*>"{x}) by FINSEQ_3:57
.= card(fn"{x}) + card(<*q*>"{x}) by A79
.= card((fn^<*q*>)"{x}) by FINSEQ_3:57
.= card Coim(R,x) by A5,A2,Th7;
end;
hence R,b are_fiberwise_equipotent;
end;
end;
hence thesis;
end;
theorem Th22:
for R be real-valued FinSequence
ex R1 be non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent
proof
let R be real-valued FinSequence;
A1: len R = len R;
for n holds P[n] from NAT_1:sch 2(Lm5,Lm6);
hence thesis by A1;
end;
Lm7: for n holds for g1,g2 be non-increasing real-valued FinSequence st
n = len g1
& g1,g2 are_fiberwise_equipotent holds g1 = g2
proof
defpred P[Nat] means for g1,g2 be non-increasing real-valued FinSequence st
$1 = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let g1,g2 be non-increasing real-valued FinSequence;
set r = g1.(n+1);
reconsider g1n = g1|n, g2n = g2|n
as non-increasing real-valued FinSequence;
assume that
A3: len g1 = n+1 and
A4: g1,g2 are_fiberwise_equipotent;
A5: len g2 = len g1 by A4,Th3;
then
A6: g1.(len g1) = g2.(len g2) by A3,A4,Lm4;
A7: (g1|n)^<*r*> = g1 by A3,Th7;
len(g1|n) = n by A3,FINSEQ_1:59,NAT_1:11;
then g1n = g2n by A2,A3,A4,A5,Lm4;
hence thesis by A3,A5,A6,A7,Th7;
end;
A8: P[0]
proof
let g1,g2 be non-increasing real-valued FinSequence;
assume len g1 = 0 & g1,g2 are_fiberwise_equipotent;
then len g2 = len g1 & g1 = <*>REAL by Th3;
hence thesis;
end;
thus for n holds P[n] from NAT_1:sch 2(A8,A1);
end;
theorem
for R1,R2 be non-increasing real-valued FinSequence st
R1,R2 are_fiberwise_equipotent holds R1 = R2
proof
let g1,g2 be non-increasing real-valued FinSequence;
A1: len g1 = len g1;
assume g1,g2 are_fiberwise_equipotent;
hence thesis by A1,Lm7;
end;
theorem
for R be real-valued FinSequence, r,s st r <> 0 holds R"{s/r} = (r*R)"{ s }
proof
let R be real-valued FinSequence, r,s;
A1: Seg len R = dom R & dom(r*R) = Seg len(r*R) by FINSEQ_1:def 3;
assume
A2: r <> 0;
reconsider R1 = R as FinSequence of REAL by RVSUM_1:145;
thus R"{s/r} c= (r*R)"{s}
proof
let x be object;
assume
A3: x in R"{s/r};
then x in R1"{s/r};
then reconsider i = x as Element of NAT;
R.i in {s/r} by A3,FUNCT_1:def 7;
then R.i = s/r by TARSKI:def 1;
then r*(R.i) = s by A2,XCMPLX_1:87;
then (r*R).i = s by RVSUM_1:44;
then
A4: (r*R).i in {s} by TARSKI:def 1;
i in dom R by A3,FUNCT_1:def 7;
then i in dom (r*R1) by A1,FINSEQ_2:33;
hence thesis by A4,FUNCT_1:def 7;
end;
let x be object;
assume
A5: x in (r*R)"{s};
then reconsider i = x as Element of NAT;
(r*R).i in {s} by A5,FUNCT_1:def 7;
then (r*R).i = s by TARSKI:def 1;
then r*R.i = s by RVSUM_1:44;
then R.i = s/r by A2,XCMPLX_1:89;
then
A6: R.i in {s/r} by TARSKI:def 1;
i in dom(r*R) by A5,FUNCT_1:def 7;
then i in dom R1 by A1,FINSEQ_2:33;
hence thesis by A6,FUNCT_1:def 7;
end;
theorem
for R be real-valued FinSequence holds (0*R)"{0} = dom R
proof
let R be real-valued FinSequence;
reconsider R1 = R as FinSequence of REAL by RVSUM_1:145;
A1: Seg len(0*R) = dom(0*R) by FINSEQ_1:def 3;
A2: len(0*R1) = len R1 & dom R1 = Seg len R1 by FINSEQ_1:def 3,FINSEQ_2:33;
hence (0*R)"{0} c= dom R by A1,RELAT_1:132;
let x be object;
assume
A3: x in dom R;
then reconsider i = x as Element of NAT;
(0*R).i = 0*R.i by RVSUM_1:44
.= 0;
then (0*R).i in {0} by TARSKI:def 1;
hence thesis by A2,A1,A3,FUNCT_1:def 7;
end;
begin :: Addenda
:: from VECTSP_9, 2006.01.06, A.T.
reserve f, g for Function;
theorem
for f, g st rng f = rng g & f is one-to-one & g is one-to-one holds
f,g are_fiberwise_equipotent
proof
let f, g be Function such that
A1: rng f = rng g and
A2: f is one-to-one and
A3: g is one-to-one;
let x be object;
per cases;
suppose
A4: x in rng f;
then card Coim(f,x) = 1 by A2,FINSEQ_4:73;
hence thesis by A1,A3,A4,FINSEQ_4:73;
end;
suppose
A5: not x in rng f;
then card(f"{x}) = 0 by CARD_1:27,FUNCT_1:72;
hence thesis by A1,A5,CARD_1:27,FUNCT_1:72;
end;
end;
:: from REVROT_1, 2007.03.18, A.T.
theorem
for f being FinSequence holds f /^ len f = {}
proof
let f be FinSequence;
len (f /^ len f) = len f - len f by Def1
.= 0;
hence thesis;
end;
:: from SCMBSORT, 2007.07.26, A.T.
theorem
for f,g be Function,m,n be set st f.m=g.n & f.n=g.m & m in dom f &
n in dom f & dom f = dom g &
(for k be set st k<>m & k<>n & k in dom f holds f.k=g.k)
holds f,g are_fiberwise_equipotent
proof
let f,g be Function,m,n be set;
assume that
A1: f.m=g.n and
A2: f.n=g.m and
A3: m in dom f and
A4: n in dom f and
A5: dom f = dom g and
A6: for k be set st k<>m & k<>n & k in dom f holds f.k=g.k;
set t=id dom f, nm=n .--> m,mn=m .--> n, p=t +* nm +* mn;
A7: dom nm ={ n };
A8: dom t = dom f;
A9: rng t = dom (t") by FUNCT_1:33
.= dom f by A8,FUNCT_1:45;
dom mn ={ m };
then
A10: dom p = dom (t +* nm) \/ {m} by FUNCT_4:def 1
.= dom t \/ {n} \/ {m} by A7,FUNCT_4:def 1
.= dom f \/ {n} \/ {m}
.= dom f \/ {m} by A4,ZFMISC_1:40
.= dom f by A3,ZFMISC_1:40;
A11: now
let x be object;
assume
A12: x in dom f;
then
A13: (p*p).x=p.(p.x) by A10,FUNCT_1:13;
per cases;
suppose
A14: x=m;
hence (p*p).x=p.n by A13,FUNCT_4:89
.=x by A14,FUNCT_4:90;
end;
suppose
A15: x<>m;
now
per cases;
suppose
A16: x=n;
hence (p*p).x=p.m by A13,FUNCT_4:90
.=x by A16,FUNCT_4:89;
end;
suppose
A17: x<>n;
hence (p*p).x=p.(t.x) by A13,A15,FUNCT_4:91
.=p.x by A12,FUNCT_1:17
.=t.x by A15,A17,FUNCT_4:91
.=x by A12,FUNCT_1:17;
end;
end;
hence (p*p).x=x;
end;
end;
rng nm = {m} by FUNCOP_1:8;
then rng t \/ rng nm =dom f by A3,ZFMISC_1:40;
then
A18: rng(t +* nm) \/ rng mn c= dom f \/ rng mn by FUNCT_4:17,XBOOLE_1:9;
for z be object st z in rng(p*p) holds z in rng p by FUNCT_1:14;
then
A19: rng(p*p) c= rng p;
A20: rng p c= rng(t +* nm) \/ rng mn by FUNCT_4:17;
A21: rng mn ={n} by FUNCOP_1:8;
then dom f \/ rng mn =dom p by A4,A10,ZFMISC_1:40;
then
A22: dom (p*p) =dom f by A10,A18,A20,RELAT_1:27,XBOOLE_1:1;
then p*p=t by A11,FUNCT_1:17;
then
A23: p is one-to-one by A10,FUNCT_1:31;
rng p c= dom f \/ rng mn by A18,A20;
then
A24: rng p c= dom p by A4,A10,A21,ZFMISC_1:40;
then
A25: dom (g*p) =dom f by A5,A10,RELAT_1:27;
now
let x be object;
assume
A26: x in dom f;
then
A27: (g*p).x=g.(p.x) by A25,FUNCT_1:12;
per cases;
suppose
x=m;
hence (g*p).x=f.x by A1,A27,FUNCT_4:89;
end;
suppose
A28: x<>m;
now
per cases;
suppose
x=n;
hence (g*p).x=f.x by A2,A27,FUNCT_4:90;
end;
suppose
A29: x<>n;
hence (g*p).x=g.(t.x) by A27,A28,FUNCT_4:91
.=g.x by A26,FUNCT_1:17
.=f.x by A6,A26,A28,A29;
end;
end;
hence (g*p).x=f.x;
end;
end;
then
A30: f=g*p by A25,FUNCT_1:2;
rng(p*p)=dom f by A9,A22,A11,FUNCT_1:17;
then rng p = dom g by A5,A10,A24,A19;
hence thesis by A10,A23,A30,CLASSES1:77;
end;
:: form BINARITH, 2008.08.20, A.T.
theorem
for f being FinSequence, k being Nat holds len (f/^k)=len f-'k
proof
let f be FinSequence,k be Nat;
per cases;
suppose
A1: k<=len f;
then len f-'k=len f-k by XREAL_1:233;
hence thesis by A1,Def1;
end;
suppose
A2: k>len f;
then (f/^k)={} by Def1;
then
A3: len (f/^k)=0;
len f-k<0 by A2,XREAL_1:49;
hence thesis by A3,XREAL_0:def 2;
end;
end;
:: from SCPQSORT, 2008.10.12, A.T.
theorem Th30: :: RFINSEQ:17
for f,g be FinSequence,x be set st x in dom g &
f,g are_fiberwise_equipotent ex y be set st y in dom g & f.x=g.y
proof
let f,g be FinSequence,x be set;
assume that
A1: x in dom g and
A2: f,g are_fiberwise_equipotent;
consider P be Permutation of dom g such that
A3: f = g*P by A2,Th4;
take y=P.x;
thus y in dom g by A1,FUNCT_2:5;
thus thesis by A1,A3,FUNCT_2:15;
end;
theorem Th31:
for f,g,h be FinSequence holds
f,g are_fiberwise_equipotent iff h^f, h^g are_fiberwise_equipotent
proof
let f,g,h be FinSequence;
thus f,g are_fiberwise_equipotent implies h^f, h^g are_fiberwise_equipotent
proof
assume
A1: f,g are_fiberwise_equipotent;
now
let y be object;
card Coim(f,y) = card Coim(g,y) by A1;
hence card Coim(h^f,y) = card(g"{y}) + card(h"{y}) by FINSEQ_3:57
.= card Coim(h^g,y) by FINSEQ_3:57;
end;
hence thesis;
end;
assume
A2: h^f,h^g are_fiberwise_equipotent;
now
let x be object;
A3: card Coim(h^f,x) = card Coim(f,x)+card(h"{x}) & card((h^g)"{x}) =
card(g"{x} )+card(h"{x}) by FINSEQ_3:57;
card Coim(h^f,x) = card Coim(h^g,x) by A2;
hence card Coim(f,x) = card Coim(g,x) by A3;
end;
hence thesis;
end;
theorem
for f,g be FinSequence,m,n,j be Nat st f,g are_fiberwise_equipotent &
m<=n & n <= len f & (for i be Nat st 1<=i & i<=m holds f.i=g.i) &
(for i be Nat st n<i & i<=len f holds f.i=g.i) & m<j & j<=n
ex k be Nat st m<k & k<=n & f.j=g.k
proof
let f,g be FinSequence,m,n,j be Nat;
assume
A1: f,g are_fiberwise_equipotent;
assume that
A2: m<=n and
A3: n <= len f;
assume
A4: for i be Nat st 1<=i & i<=m holds f.i=g.i;
reconsider m3=len f-n as Element of NAT by A3,INT_1:3,XREAL_1:48;
len g=n+m3 by A1,Th3;
then consider s2,r2 be FinSequence such that
A5: len s2 = n and
A6: len r2 = m3 and
A7: g = s2^r2 by FINSEQ_2:22;
A8: len f=n+m3;
then consider s1,r1 be FinSequence such that
A9: len s1 = n and
A10: len r1 = m3 and
A11: f = s1^r1 by FINSEQ_2:22;
A12: dom r1 = Seg m3 by A10,FINSEQ_1:def 3;
assume
A13: for i be Nat st n<i & i<=len f holds f.i=g.i;
now
let i be Nat;
reconsider a = i as Nat;
A14: n < n+1 by XREAL_1:29;
assume
A15: i in dom r1;
then
A16: i in dom r2 by A6,A12,FINSEQ_1:def 3;
1 <= i by A12,A15,FINSEQ_1:1;
then n+1 <= n+i by XREAL_1:6;
then
A17: n< i+n by A14,XXREAL_0:2;
i <= m3 by A12,A15,FINSEQ_1:1;
then
A18: len s1+i <= len f by A8,A9,XREAL_1:6;
thus r1.i=f.(len s1+i) by A11,A15,FINSEQ_1:def 7
.=g.(len s2+a) by A13,A9,A5,A17,A18
.=r2.i by A7,A16,FINSEQ_1:def 7;
end;
then r1=r2 by A10,A6,FINSEQ_2:9;
then
A19: s1,s2 are_fiberwise_equipotent by A1,A11,A7,Th1;
reconsider m2=n-m as Element of NAT by A2,INT_1:3,XREAL_1:48;
A20: m+1 > m by XREAL_1:29;
len s2=m+m2 by A5;
then consider p2,q2 be FinSequence such that
A21: len p2 = m and
A22: len q2 = m2 and
A23: s2 = p2^q2 by FINSEQ_2:22;
A24: Seg m = dom p2 by A21,FINSEQ_1:def 3;
len s1=m+m2 by A9;
then consider p1,q1 be FinSequence such that
A25: len p1 = m and
A26: len q1 = m2 and
A27: s1 = p1^q1 by FINSEQ_2:22;
A28: f=p1^(q1^r1) by A11,A27,FINSEQ_1:32;
A29: dom p1 = Seg m by A25,FINSEQ_1:def 3;
A30: g=p2^(q2^r2) by A7,A23,FINSEQ_1:32;
now
let i be Nat;
reconsider a = i as Nat;
assume
A31: i in dom p1;
then
A32: 1<= i & i <= m by A29,FINSEQ_1:1;
thus p1.i=f.i by A28,A31,FINSEQ_1:def 7
.=g.a by A4,A32
.=p2.i by A30,A24,A29,A31,FINSEQ_1:def 7;
end;
then p1=p2 by A25,A21,FINSEQ_2:9;
then
A33: q1,q2 are_fiberwise_equipotent by A27,A23,A19,Th31;
assume that
A34: m<j and
A35: j<=n;
j-len p1 > 0 by A34,A25,XREAL_1:50;
then reconsider x=j-len p1 as Element of NAT by INT_1:3;
A36: x <= n-len p1 by A35,XREAL_1:9;
A37: Seg m2 = dom q2 by A22,FINSEQ_1:def 3;
A38: 1+ 0<= x by A34,A25,INT_1:7,XREAL_1:50;
then x in dom q2 by A25,A37,A36;
then consider y be set such that
A39: y in dom q2 and
A40: q1.x=q2.y by A33,Th30;
reconsider y as Nat by A39;
A41: len p2 + y in dom s2 by A23,A39,FINSEQ_1:28;
reconsider k=len p2+y as Nat;
take k;
1<=y by A37,A39,FINSEQ_1:1;
then k>=len p2+1 by XREAL_1:6;
hence m<k by A21,A20,XXREAL_0:2;
y<=m2 by A37,A39,FINSEQ_1:1;
then k <= m2+len p2 by XREAL_1:6;
hence k<=n by A21;
Seg m2 = dom q1 by A26,FINSEQ_1:def 3;
then
A42: x in dom q1 by A25,A38,A36;
then len p1 + x in dom s1 by A27,FINSEQ_1:28;
hence f.j=s1.(len p1+x) by A11,FINSEQ_1:def 7
.=q2.y by A27,A40,A42,FINSEQ_1:def 7
.=s2.(len p2+y) by A23,A39,FINSEQ_1:def 7
.=g.k by A7,A41,FINSEQ_1:def 7;
end;
theorem
for t being FinSequence of INT ex u being FinSequence of REAL
st t,u are_fiberwise_equipotent & u is FinSequence of INT
& u is non-increasing
proof
let t be FinSequence of INT;
consider u be non-increasing FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent by Th22;
take u;
thus t,u are_fiberwise_equipotent by A1;
rng t = rng u by A1,CLASSES1:75;
hence u is FinSequence of INT by FINSEQ_1:def 4;
thus thesis;
end;
:: Added by SK, 15.11.2024
theorem ::: variant of FINSEQ_1:47
for p,q,r,s being FinSequence st p^q = r^s & len p <= len r
ex t,u being FinSequence st p^t = r & u^s = q
proof
let p,q,r,s be FinSequence;
assume A1: p^q = r^s & len p <= len r;
then len r - len p in NAT by INT_1:5;
then reconsider k = len r - len p as Nat;
A3: len p + len q = len(p^q) by FINSEQ_1:22
.= len r + len s by A1, FINSEQ_1:22;
then len q = k + len s;
then A5: len q >= k + 0 by XREAL_1:6;
A6: len(p^(q|k)) = len p + len(q|k) by FINSEQ_1:22
.= len p + k by A5, FINSEQ_1:59
.= len r;
A7: len((r/^len p)^s) = len(r/^len p) + len s by FINSEQ_1:22
.= len r - len p + len s by A1, Def1
.= len q by A3;
take q|k, r/^len p;
now
let i be Nat;
assume A8: 1 <= i & i <= len r;
then A9: i in dom r by FINSEQ_3:25;
per cases;
suppose i <= len p;
then A11: i in dom p by A8, FINSEQ_3:25;
hence (p^(q|k)).i = p.i by FINSEQ_1:def 7
.= (r^s).i by A1, A11, FINSEQ_1:def 7
.= r.i by A9, FINSEQ_1:def 7;
end;
suppose len p < i;
then len p + 1 <= i by NAT_1:13;
then consider j being Nat such that
A14: i = len p + 1 + j by NAT_1:10;
A15: i = len p + (1+j) by A14;
len p + (1 + j) <= len p + k by A8, A14;
then 1 + j <= k by XREAL_1:6;
then A16: 1 + j <= len(q|k) by A5, FINSEQ_1:59;
1 + 0 <= 1 + j by XREAL_1:6;
then A17: 1+j in dom(q|k) by A16, FINSEQ_3:25;
then A18: 1+j in dom(q|Seg k);
then A19: 1+j in dom q by RELAT_1:60, TARSKI:def 3;
thus (p^(q|k)).i = (q|k).(1+j) by A15, A17, FINSEQ_1:def 7
.= (q|Seg k).(1+j)
.= q.(1+j) by A18, FUNCT_1:47
.= (r^s).i by A1, A15, A19, FINSEQ_1:def 7
.= r.i by A9, FINSEQ_1:def 7;
end;
end;
hence p^(q|k) = r by A6, FINSEQ_1:14;
now
let i be Nat;
assume A20: 1 <= i & i <= len q;
then A21: i in dom q by FINSEQ_3:25;
per cases;
suppose A22: i <= k;
len(r/^len p) = k by A1, Def1;
then A25: i in dom(r/^len p) by A20, A22, FINSEQ_3:25;
A26: i + len p <= len r - len p + len p by A22, XREAL_1:6;
1 + 0 <= i + len p by A20, XREAL_1:7;
then A27: i + len p in dom r by A26, FINSEQ_3:25;
thus ((r/^len p)^s).i = (r/^len p).i by A25, FINSEQ_1:def 7
.= r.(i+len p) by A1, A25, Def1
.= (p^q).(len p + i) by A1, A27, FINSEQ_1:def 7
.= q.i by A21, FINSEQ_1:def 7;
end;
suppose k < i;
then k + 1 <= i by NAT_1:13;
then consider j being Nat such that
A29: i = k + 1 + j by NAT_1:10;
len(r/^len p) = k by A1, Def1;
then A30: i = len(r/^len p) + (1 + j) by A29;
i <= len(r/^len p) + len s by A7, A20, FINSEQ_1:22;
then A31: 1 + j <= len s by A30, XREAL_1:6;
1 + 0 <= 1 + j by XREAL_1:6;
then A32: 1+j in dom s by A31, FINSEQ_3:25;
thus ((r/^len p)^s).i = s.(1+j) by A30, A32, FINSEQ_1:def 7
.= (p^q).(len r + (1+j)) by A1, A32, FINSEQ_1:def 7
.= (p^q).(len p + i) by A29
.= q.i by A21, FINSEQ_1:def 7;
end;
end;
hence thesis by A7, FINSEQ_1:14;
end;