:: Properties of Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz and Yuji Sakai
::
:: 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, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3,
COMPLEX1, RELAT_1, XBOOLE_0, FINSEQ_1, TARSKI, FUNCT_1, PARTFUN1,
VALUED_1, CLASSES1, FUNCOP_1, MEMBERED, VALUED_0, ORDINAL4, BINOP_1,
SETWISEO, CARD_3, NAT_1, RFINSEQ, FUNCT_3, PBOOLE, LIMFUNC1, FINSET_1,
XXREAL_1, FINSEQ_2, RFUNCT_3, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, XXREAL_0, REAL_1, NAT_1, FUNCOP_1, SETWISEO, FINSEQ_2,
FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, RFUNCT_1, FINSEQ_4, SETWOP_2,
FINSET_1, RVSUM_1, RCOMP_1, PARTFUN2, LIMFUNC1, CLASSES1, RFINSEQ;
constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, BINOP_2, COMPLEX1,
SEQM_3, PROB_1, SEQ_4, FINSEQOP, RCOMP_1, FINSEQ_4, FINSOP_1, PARTFUN2,
RFUNCT_1, RVSUM_1, LIMFUNC1, RFINSEQ, CLASSES1, RELSET_1, SETFAM_1,
VALUED_0, SQUARE_1;
registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, VALUED_0, FUNCT_1, CARD_1,
RVSUM_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BINOP_1, SETWISEO, RFINSEQ, XBOOLE_0;
equalities SUBSET_1, FINSEQ_2, RVSUM_1, LIMFUNC1, VALUED_1, RELAT_1;
expansions TARSKI, BINOP_1, XBOOLE_0, RELAT_1;
theorems FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_1, CARD_2, TARSKI, CARD_1, FINSET_1,
PARTFUN1, RCOMP_1, BINOP_1, FINSEQ_3, FUNCOP_1, RFUNCT_1, ZFMISC_1,
RVSUM_1, ABSVALUE, RFINSEQ, RELAT_1, FINSOP_1, XREAL_0, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1,
RELSET_1, XXREAL_1, CLASSES1;
schemes NAT_1, FINSEQ_1, SEQ_1, BINOP_1;
begin :: Nonnegative and Nonpositive Part of a Real Number
reserve n,m for Nat,
r,r1,r2,s,t for Real,
x,y for set;
definition
let r be Real;
func max+ (r) -> Real equals
max(r,0);
correctness;
func max- (r) -> Real equals
max(-r,0);
correctness;
end;
theorem Th1:
for r be Real holds r = max+(r) - max-(r)
proof
let r be Real;
now
per cases;
case
A1: 0<=r;
then max-(r) = 0 by XXREAL_0:def 10;
hence thesis by A1,XXREAL_0:def 10;
end;
case
r<0;
then max+(r) = 0 & max-(r) = -r by XXREAL_0:def 10;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th2:
for r be Real holds |.r.| = max+(r) + max-(r)
proof
let r be Real;
now
per cases;
case
A1: 0<=r;
then max+(r) = r & max-(r) = 0 by XXREAL_0:def 10;
hence thesis by A1,ABSVALUE:def 1;
end;
case
A2: r<0;
then max+(r) = 0 & max-(r) = -r by XXREAL_0:def 10;
hence thesis by A2,ABSVALUE:def 1;
end;
end;
hence thesis;
end;
theorem Th3:
for r be Real holds 2*max+(r) = r + |.r.|
proof
let r be Real;
thus r + |.r.| = max+(r) - max-(r) + |.r.| by Th1
.= max+(r) - max-(r) + (max+(r) + max-(r)) by Th2
.= 2*max+(r);
end;
theorem Th4:
for r,s be Real st 0<=r holds max+(r*s) = r*(max+ s)
proof
let r,s be Real;
assume
A1: 0<=r;
now
per cases;
case
A2: 0<=s;
then max+(r*s) = r*s by A1,XXREAL_0:def 10;
hence thesis by A2,XXREAL_0:def 10;
end;
case
A3: s<0;
then max+ s= 0 by XXREAL_0:def 10;
hence thesis by A1,A3,XXREAL_0:def 10;
end;
end;
hence thesis;
end;
theorem Th5:
for r,s be Real holds max+(r+s) <= max+(r) + max+(s)
proof
let r,s be Real;
A1: 0<=max(r,0) & 0<=max(s,0) by XXREAL_0:25;
A2: r<=max(r,0) & s<=max(s,0) by XXREAL_0:25;
now
per cases;
case
0<=r+s;
then max+(r+s) = r+s by XXREAL_0:def 10;
hence thesis by A2,XREAL_1:7;
end;
case
r+s<0;
then max+(r+s) = 0+0 by XXREAL_0:def 10;
hence thesis by A1;
end;
end;
hence thesis;
end;
Lm1: for D be non empty set, f be FinSequence of D st len f<=n holds (f|n) = f
proof
let D be non empty set,f be FinSequence of D;
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,def 16;
hence thesis by RELAT_1:68;
end;
Lm2: for f be Function,x be set st not x in rng f holds f"{x}={}
proof
let f be Function,x be set;
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;
begin
::
:: Partial Functions from a Domain to the Set of Real Numbers
::
theorem Th6:
for D be non empty set, F be PartFunc of D,REAL, r,s be Real
st r <> 0 holds F"{s/r} = (r(#)F)"{s}
proof
let D be non empty set, F be PartFunc of D,REAL, r,s be Real;
assume
A1: r <> 0;
thus F"{s/r} c= (r(#)F)"{s}
proof
let x be object;
assume
A2: x in F"{s/r};
then reconsider d=x as Element of D;
d in dom F by A2,FUNCT_1:def 7;
then
A3: d in dom(r(#)F) by VALUED_1:def 5;
F.d in {s/r} by A2,FUNCT_1:def 7;
then F.d = s/r by TARSKI:def 1;
then r*F.d = s by A1,XCMPLX_1:87;
then (r(#)F).d = s by A3,VALUED_1:def 5;
then (r(#)F).d in {s} by TARSKI:def 1;
hence thesis by A3,FUNCT_1:def 7;
end;
let x be object;
assume
A4: x in (r(#)F)"{s};
then reconsider d=x as Element of D;
A5: d in dom(r(#)F) by A4,FUNCT_1:def 7;
(r(#)F).d in {s} by A4,FUNCT_1:def 7;
then (r(#)F).d = s by TARSKI:def 1;
then r*F.d = s by A5,VALUED_1:def 5;
then F.d = s/r by A1,XCMPLX_1:89;
then
A6: F.d in {s/r} by TARSKI:def 1;
d in dom F by A5,VALUED_1:def 5;
hence thesis by A6,FUNCT_1:def 7;
end;
theorem Th7:
for D be non empty set, F be PartFunc of D,REAL holds (0(#)F)"{0} = dom F
proof
let D be non empty set, F be PartFunc of D,REAL;
thus (0(#)F)"{0} c= dom F
proof
let x be object;
assume
A1: x in (0(#)F)"{0};
then reconsider d=x as Element of D;
d in dom(0(#)F) by A1,FUNCT_1:def 7;
hence thesis by VALUED_1:def 5;
end;
let x be object;
assume
A2: x in dom F;
then reconsider d=x as Element of D;
A3: d in dom(0(#)F) by A2,VALUED_1:def 5;
then (0(#)F).d = 0*(F.d) by VALUED_1:def 5
.= 0;
then (0(#)F).d in {0} by TARSKI:def 1;
hence thesis by A3,FUNCT_1:def 7;
end;
theorem Th8:
for D be non empty set, F be PartFunc of D,REAL, r st 0<
r holds abs(F)"{r} = F"{-r,r}
proof
let D be non empty set, F be PartFunc of D,REAL, r;
assume
A1: 0<r;
A2: dom abs(F) = dom F by VALUED_1:def 11;
thus abs(F)"{r} c= F"{-r,r}
proof
let x be object;
assume
A3: x in abs(F)"{r};
then reconsider rr = x as Element of D;
abs(F).rr in {r} by A3,FUNCT_1:def 7;
then |.F.rr.| in {r} by VALUED_1:18;
then
A4: |.F.rr.| = r by TARSKI:def 1;
A5: rr in dom abs(F) by A3,FUNCT_1:def 7;
now
per cases;
case
0<=F.rr;
then F.rr = r by A4,ABSVALUE:def 1;
then F.rr in {-r,r} by TARSKI:def 2;
hence thesis by A2,A5,FUNCT_1:def 7;
end;
case
F.rr<0;
then -F.rr = r by A4,ABSVALUE:def 1;
then F.rr in {-r,r} by TARSKI:def 2;
hence thesis by A2,A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
let x be object;
assume
A6: x in F"{-r,r};
then reconsider rr = x as Element of D;
A7: rr in dom F by A6,FUNCT_1:def 7;
A8: F.rr in {-r,r} by A6,FUNCT_1:def 7;
now
per cases by A8,TARSKI:def 2;
case
F.rr = -r;
then r = |.-F.rr.| by A1,ABSVALUE:def 1
.= |.F.rr.| by COMPLEX1:52
.= abs(F).rr by VALUED_1:18;
then abs(F).rr in {r} by TARSKI:def 1;
hence thesis by A2,A7,FUNCT_1:def 7;
end;
case
F.rr = r;
then r = |.F.rr.| by A1,ABSVALUE:def 1
.= abs(F).rr by VALUED_1:18;
then abs(F).rr in {r} by TARSKI:def 1;
hence thesis by A2,A7,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
theorem Th9:
for D be non empty set, F be PartFunc of D,REAL holds abs(F)"{0} = F"{0}
proof
let D be non empty set, F be PartFunc of D,REAL;
A1: dom abs(F) = dom F by VALUED_1:def 11;
thus abs(F)"{0} c= F"{0}
proof
let x be object;
assume
A2: x in abs(F)"{0};
then reconsider r=x as Element of D;
abs(F).r in {0} by A2,FUNCT_1:def 7;
then |.F.r.| in {0} by VALUED_1:18;
then |.F.r.| = 0 by TARSKI:def 1;
then F.r = 0 by ABSVALUE:2;
then
A3: F.r in {0} by TARSKI:def 1;
r in dom abs(F) by A2,FUNCT_1:def 7;
hence thesis by A1,A3,FUNCT_1:def 7;
end;
let x be object;
assume
A4: x in F"{0};
then reconsider r=x as Element of D;
F.r in {0} by A4,FUNCT_1:def 7;
then F.r = 0 by TARSKI:def 1;
then |.F.r.| = 0 by ABSVALUE:2;
then abs(F).r = 0 by VALUED_1:18;
then
A5: abs(F).r in {0} by TARSKI:def 1;
r in dom F by A4,FUNCT_1:def 7;
hence thesis by A1,A5,FUNCT_1:def 7;
end;
theorem Th10:
for D be non empty set, F be PartFunc of D,REAL, r st r<
0 holds abs(F)"{r} = {}
proof
let D be non empty set, F be PartFunc of D,REAL, r;
assume
A1: r<0;
set x = the Element of abs(F)"{r};
assume
A2: abs(F)"{r} <> {};
then reconsider x as Element of D by TARSKI:def 3;
abs(F).x in {r} by A2,FUNCT_1:def 7;
then |.F.x.| in {r} by VALUED_1:18;
then |.F.x.| = r by TARSKI:def 1;
hence contradiction by A1,COMPLEX1:46;
end;
theorem Th11:
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc
of C,REAL, r st r <> 0 holds F,G are_fiberwise_equipotent iff r(#)F, r
(#)G are_fiberwise_equipotent
proof
let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL,
r;
assume
A1: r <> 0;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
A2: rng(rr(#)F) c= REAL & rng(rr(#)G) c= REAL;
thus F,G are_fiberwise_equipotent implies r(#)F, r(#) G
are_fiberwise_equipotent
proof
assume
A3: F,G are_fiberwise_equipotent;
now
let x be Element of REAL;
Coim(F,x/r) = Coim(r(#)F,x) & Coim(G,x/r) = Coim(r(#)G,x) by A1,Th6;
hence card Coim(r(#)F,x) = card Coim(r(#)G,x) by A3,CLASSES1:def 10;
end;
hence thesis by A2,CLASSES1:79;
end;
assume
A4: r(#)F, r(#)G are_fiberwise_equipotent;
A5: now
let x be Element of REAL;
A6: G"{r*x/r} = Coim(r(#)G,r*x) by A1,Th6;
r*x/r = x & F"{r*x/r} = Coim(r(#)F,r*x) by A1,Th6,XCMPLX_1:89;
hence card Coim(F,x) = card Coim(G,x) by A4,A6,CLASSES1:def 10;
end;
rng F c= REAL & rng G c= REAL;
hence thesis by A5,CLASSES1:79;
end;
theorem
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
REAL holds F,G are_fiberwise_equipotent iff -F, -G are_fiberwise_equipotent
by Th11;
theorem
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
REAL st F,G are_fiberwise_equipotent holds abs(F), abs(G)
are_fiberwise_equipotent
proof
let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL;
assume
A1: F,G are_fiberwise_equipotent;
A2: now
let r be Element of REAL;
now
per cases;
case
0<r;
then abs(F)"{r} = F"{-r,r} & abs(G)"{r} = G"{-r,r} by Th8;
hence card(abs(F)"{r}) = card(abs(G)"{r}) by A1,CLASSES1:78;
end;
case
0=r;
then abs(F)"{r} = F"{r} & abs(G)"{r} = G"{r} by Th9;
hence card(abs(F)"{r}) = card(abs(G)"{r}) by A1,CLASSES1:78;
end;
case
A3: r<0;
then abs(F)"{r} = {} by Th10;
hence card(abs(F)"{r}) = card(abs(G)"{r}) by A3,Th10;
end;
end;
hence card Coim(abs(F),r) = card Coim(abs(G),r);
end;
rng abs(F) c= REAL & rng abs(G) c= REAL;
hence thesis by A2,CLASSES1:79;
end;
definition
let X,Y be set;
mode PartFunc-set of X,Y -> set means
:Def3:
for x being Element of it holds x is PartFunc of X,Y;
existence
proof
reconsider h={} as PartFunc of X,Y by RELSET_1:12;
take {h};
thus thesis by TARSKI:def 1;
end;
end;
registration
let X,Y be set;
cluster non empty for PartFunc-set of X,Y;
existence
proof
reconsider h={} as PartFunc of X,Y by RELSET_1:12;
{h} is PartFunc-set of X,Y
proof
let x be Element of {h};
thus thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
definition
let X,Y be set;
mode PFUNC_DOMAIN of X,Y is non empty PartFunc-set of X,Y;
end;
definition
let X,Y be set;
redefine func PFuncs(X,Y) -> PartFunc-set of X,Y; :: redefines PFuncs (PARTFUN1, definition)
coherence
proof
for x be Element of PFuncs(X,Y) holds x is PartFunc of X,Y by PARTFUN1:47;
hence thesis by Def3;
end;
let P be non empty PartFunc-set of X,Y;
redefine mode Element of P -> PartFunc of X,Y; :: redefines Element (SUBSET_1, definition)
coherence by Def3;
end;
definition
let D,C be non empty set, X be Subset of D, c be Element of C;
redefine func X --> c -> Element of PFuncs(D,C); :: redefines --> (FUNCOP_1, definition)
coherence
proof
X --> c is PartFunc of D,C;
hence thesis by PARTFUN1:45;
end;
end;
:: awaryjne, A.T.
registration
let D be non empty set, E be real-membered set;
cluster -> real-valued for Element of PFuncs(D,E);
coherence;
end;
definition
let D be non empty set, E be real-membered set, F1,F2 be Element of PFuncs(D
,E);
redefine func F1+F2 -> Element of PFuncs(D,REAL); :: redefines + (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1+F2 is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
redefine func F1-F2 -> Element of PFuncs(D,REAL); :: redefines - (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1-F2 is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
redefine func F1(#)F2 -> Element of PFuncs(D,REAL); :: redefines (#) (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1(#)F2 is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
redefine func F1/F2 -> Element of PFuncs(D,REAL); :: redefines / (RFUNCT_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1/F2 is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
end;
definition
let D be non empty set, E be real-membered set, F be Element of PFuncs(D,E);
redefine func abs(F) -> Element of PFuncs(D,REAL); :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
abs F is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
redefine func - F -> Element of PFuncs(D,REAL); :: redefines - (VALUED_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
-F is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
redefine func F^ -> Element of PFuncs(D,REAL); :: redefines ^ (RFUNCT_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
F^ is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
end;
definition
let D be non empty set, E be real-membered set, F be Element of PFuncs(D,E),
r be Real;
redefine func r(#)F -> Element of PFuncs(D,REAL); :: redefines (#) (VALUED_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
r(#)F is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
end;
definition
let D be non empty set;
func addpfunc(D) -> BinOp of PFuncs(D,REAL) means
:Def4:
for F1,F2 be Element of PFuncs(D,REAL) holds it.(F1,F2) = F1 + F2;
existence
proof
deffunc O(Element of PFuncs(D,REAL),Element of PFuncs(D,REAL))= $1 + $2;
ex o being BinOp of PFuncs(D,REAL) st for a,b being Element of PFuncs(
D,REAL) holds o.(a,b) = O(a,b) from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be BinOp of PFuncs(D,REAL);
assume that
A1: for f1,f2 be Element of PFuncs(D,REAL) holds o1.(f1,f2) = f1 + f2 and
A2: for f1,f2 be Element of PFuncs(D,REAL) holds o2.(f1,f2) = f1 + f2;
now
let f1,f2 be Element of PFuncs(D,REAL);
o1.(f1,f2) = f1 + f2 by A1;
hence o1.(f1,f2)=o2.(f1,f2) by A2;
end;
hence thesis;
end;
end;
theorem Th14:
for D be non empty set holds addpfunc(D) is commutative
proof
let D be non empty set;
let F1,F2 be Element of PFuncs(D,REAL);
set o=addpfunc(D);
thus o.(F1,F2) = F2+F1 by Def4
.= o.(F2,F1) by Def4;
end;
theorem Th15:
for D be non empty set holds addpfunc(D) is associative
proof
let D be non empty set;
let F1,F2,F3 be Element of PFuncs(D,REAL);
set o=addpfunc(D);
thus o.(F1,o.(F2,F3)) = o.(F1,F2+F3) by Def4
.= F1+(F2+F3) by Def4
.= F1+F2+F3 by RFUNCT_1:8
.= o.(F1,F2) + F3 by Def4
.= o.(o.(F1,F2),F3) by Def4;
end;
theorem Th16:
for D be non empty set holds [#](D) --> (0 qua Real)
is_a_unity_wrt addpfunc(D)
proof
let D be non empty set;
set F = [#](D) --> In(0,REAL);
A1: dom F = D by FUNCOP_1:13;
A2: now
let G be Element of PFuncs(D,REAL);
A3: now
let d be Element of D;
assume d in dom(G+F);
hence (G+F).d = G.d+F.d by VALUED_1:def 1
.= G.d + 0 by FUNCOP_1:7
.= G.d;
end;
dom G /\ D = dom G by XBOOLE_1:28;
then dom(G+F) = dom G by A1,VALUED_1:def 1;
then G+F = G by A3,PARTFUN1:5;
hence addpfunc(D).(G,F) = G by Def4;
end;
addpfunc(D) is commutative by Th14;
hence thesis by A2,BINOP_1:5;
end;
theorem Th17:
for D be non empty set holds the_unity_wrt addpfunc(D) = [#](D)
--> (0 qua Real)
proof
let D be non empty set;
[#](D) --> In(0,REAL) is_a_unity_wrt addpfunc(D) by Th16;
hence thesis by BINOP_1:def 8;
end;
theorem Th18:
for D be non empty set holds addpfunc(D) is having_a_unity
proof
let D be non empty set;
take [#](D) --> In(0,REAL);
thus thesis by Th16;
end;
definition
let D be non empty set, f be FinSequence of PFuncs(D,REAL);
func Sum(f) -> Element of PFuncs(D,REAL) equals
(addpfunc(D)) $$ f;
correctness;
end;
theorem Th19:
for D be non empty set holds Sum(<*> PFuncs(D,REAL) ) = [#](D)
-->(0 qua Real)
proof
let D be non empty set;
set o = addpfunc(D), o0 = [#](D) --> (0 qua Real);
the_unity_wrt o = o0 by Th17;
hence thesis by Th18,FINSOP_1:10;
end;
theorem Th20:
for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be
Element of PFuncs(D,REAL) holds Sum(f^<*G*>) = Sum f + G
proof
let D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of
PFuncs(D,REAL);
set o = addpfunc(D);
thus Sum(f^<*G*>) = o.(o $$ f,G) by Th18,FINSOP_1:4
.= Sum f + G by Def4;
end;
theorem Th21:
for D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL)
holds Sum(f1^f2) = Sum f1 + Sum f2
proof
let D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL);
set o = addpfunc(D);
o is associative by Th15;
hence Sum(f1^f2)= addpfunc(D).(Sum f1,Sum f2) by Th18,FINSOP_1:5
.= Sum f1 + Sum f2 by Def4;
end;
theorem
for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be
Element of PFuncs(D,REAL) holds Sum(<*G*>^f) = G + Sum f
proof
let D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of
PFuncs(D,REAL);
thus Sum(<*G*>^f) = Sum <*G*> + Sum f by Th21
.= G + Sum f by FINSOP_1:11;
end;
theorem Th23:
for D be non empty set, G1,G2 be Element of PFuncs(D,REAL) holds
Sum<*G1,G2*> = G1 + G2
proof
let D be non empty set, G1,G2 be Element of PFuncs(D,REAL);
thus Sum<*G1,G2*> = Sum(<*G1*>^<*G2*>) by FINSEQ_1:def 9
.= Sum<*G1*> + G2 by Th20
.= G1 + G2 by FINSOP_1:11;
end;
theorem
for D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL) holds
Sum<*G1,G2,G3*> = G1 + G2 + G3
proof
let D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL);
thus Sum<*G1,G2,G3*> = Sum(<*G1,G2*>^<*G3*>) by FINSEQ_1:43
.= Sum<*G1,G2*> + G3 by Th20
.= G1 + G2 + G3 by Th23;
end;
theorem
for D be non empty set, f,g be FinSequence of PFuncs(D,REAL) st f,g
are_fiberwise_equipotent holds Sum f = Sum g
proof
let D be non empty set;
defpred P[Nat] means for f,g be FinSequence of PFuncs(D,REAL) st
f,g are_fiberwise_equipotent & len f = $1 holds Sum f = Sum g;
let f,g be FinSequence of PFuncs(D,REAL);
assume
A1: f,g are_fiberwise_equipotent;
A2: len f = len f;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let f,g be FinSequence of PFuncs(D,REAL);
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
0+1<=n+1 by NAT_1:13;
then
A7: n+1 in dom f by A6,FINSEQ_3:25;
then reconsider a=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:11;
rng f = rng g by A5,CLASSES1:75;
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;
A10: g = (g|m) ^ (g/^m) by RFINSEQ:8;
set gg = g/^m, gm = g|m;
m<=len g by A8,FINSEQ_3:25;
then
A11: len gm = m by FINSEQ_1:59;
set fn=f|n;
A12: f = fn ^ <*a*> by A6,RFINSEQ:7;
A13: 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;
A14: m=m1+1;
then m1<=m by NAT_1:11;
then
A15: Seg m1 c= Seg m by FINSEQ_1:5;
m in Seg m by A13,FINSEQ_1:1;
then gm.m = a by A8,A9,RFINSEQ:6;
then
A16: gm = (gm|m1) ^ <*a*> by A11,A14,RFINSEQ:7;
A17: gm|m1 = gm|(Seg m1) by FINSEQ_1:def 16
.= (g|(Seg m))|(Seg m1) by FINSEQ_1:def 16
.= g|((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|(Seg m1) by A15,XBOOLE_1:28
.= g|m1 by FINSEQ_1:def 16;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A5,CLASSES1:def 10;
then
card(fn"{x}) + card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by A10
,A16,A17,A12,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 by CLASSES1:def 10;
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 A12,Th21
.= Sum(g|m1) + Sum gg+ Sum <*a*> by Th21
.= Sum(g|m1)+ Sum <*a*> + Sum gg by RFUNCT_1:8
.= Sum gm + Sum gg by A16,A17,Th21
.= Sum g by A10,Th21;
end;
A19: P[ 0 ]
proof
let f,g be FinSequence of PFuncs(D,REAL);
assume f,g are_fiberwise_equipotent & len f = 0;
then
A20: len g = 0 & f =<*>PFuncs(D,REAL) by RFINSEQ:3;
then g =<*>PFuncs(D,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 D be non empty set, f be FinSequence;
func CHI(f,D) -> FinSequence of PFuncs(D,REAL) means
:Def6:
len it = len f & for n st n in dom it holds it.n = chi(f.n,D);
existence
proof
deffunc F(Nat)= chi(f.$1,D);
consider p be FinSequence such that
A1: len p = len f and
A2: for n be Nat st n in dom p holds p.n = F(n) from FINSEQ_1:sch 2;
rng p c= PFuncs(D,REAL)
proof
let x be object;
assume x in rng p;
then consider n being Nat such that
A3: n in dom p & p.n = x by FINSEQ_2:10;
x = chi(f.n,D) by A2,A3;
hence thesis by PARTFUN1:45;
end;
then reconsider p as FinSequence of PFuncs(D,REAL) by FINSEQ_1:def 4;
take p;
thus len p = len f by A1;
let n;
assume n in dom p;
hence thesis by A2;
end;
uniqueness
proof
let p1,p2 be FinSequence of PFuncs(D,REAL);
assume that
A4: len p1 = len f and
A5: for n st n in dom p1 holds p1.n = chi(f.n,D) and
A6: len p2 = len f and
A7: for n st n in dom p2 holds p2.n = chi(f.n,D);
A8: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3;
now
let n be Nat;
assume
A9: n in dom p1;
then p1.n = chi(f.n,D) by A5;
hence p1.n = p2.n by A4,A6,A7,A8,A9;
end;
hence thesis by A4,A6,FINSEQ_2:9;
end;
end;
definition
let D be non empty set, f be FinSequence of PFuncs(D,REAL), R be FinSequence
of REAL;
func R (#) f -> FinSequence of PFuncs(D,REAL) means
:Def7:
len it = min(len R,len f) &
for n st n in dom it for F be PartFunc of D,REAL, r st r = R.n &
F = f.n holds it.n = r(#)F;
existence
proof
defpred P[Nat,set] means for F be PartFunc of D,REAL, r st r=R.$1 & F = f.
$1 holds $2 = r(#)F;
set m = min(len R,len f);
A1: m<=len f by XXREAL_0:17;
A2: for n be Nat st n in Seg m ex x being Element of PFuncs(D,REAL) st P[n ,x]
proof
let n be Nat;
reconsider r=R.n as Real;
assume
A3: n in Seg m;
then n<=m by FINSEQ_1:1;
then
A4: n<=len f by A1,XXREAL_0:2;
1<=n by A3,FINSEQ_1:1;
then n in dom f by A4,FINSEQ_3:25;
then reconsider F=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:11;
reconsider a= r(#)F as Element of PFuncs(D,REAL);
take a;
thus thesis;
end;
consider p be FinSequence of PFuncs(D,REAL) such that
A5: dom p = Seg m & for n be Nat st n in Seg m holds P[n,p.n] from
FINSEQ_1:sch 5(A2);
take p;
thus len p = m by A5,FINSEQ_1:def 3;
let n;
assume n in dom p;
hence thesis by A5;
end;
uniqueness
proof
set m = min(len R,len f);
let p1,p2 be FinSequence of PFuncs(D,REAL);
assume that
A6: len p1 = m and
A7: for n st n in dom p1 for F be PartFunc of D,REAL, r st r = R.n &
F = f.n holds p1.n = r(#)F and
A8: len p2 = m and
A9: for n st n in dom p2 for F be PartFunc of D,REAL, r st r = R.n &
F = f.n holds p2.n = r(#)F;
A10: dom p1 = Seg m by A6,FINSEQ_1:def 3;
A11: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3;
A12: m<=len f by XXREAL_0:17;
now
let n be Nat;
reconsider r=R.n as Real;
assume
A13: n in dom p1;
then n<=m by A10,FINSEQ_1:1;
then
A14: n<=len f by A12,XXREAL_0:2;
1<=n by A10,A13,FINSEQ_1:1;
then n in dom f by A14,FINSEQ_3:25;
then reconsider F=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:11;
p1.n=r(#)F by A7,A13;
hence p1.n = p2.n by A6,A8,A9,A11,A13;
end;
hence thesis by A6,A8,FINSEQ_2:9;
end;
end;
definition
let D be non empty set, f be FinSequence of PFuncs(D,REAL),
d be Element of D;
func f#d -> FinSequence of REAL means
:Def8:
len it = len f & for n be Element of NAT st n in dom it holds it.n = f.n.d;
existence
proof
defpred P[Nat,set] means $2 = f.$1.d;
A1: for n be Nat st n in Seg len f ex x being Element of REAL st P[n,x]
proof
let n be Nat;
assume n in Seg len f;
then n in dom f by FINSEQ_1:def 3;
then reconsider G=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:11;
take G.d;
thus thesis by XREAL_0:def 1;
end;
consider p being FinSequence of REAL such that
A2: dom p = Seg len f and
A3: for n be Nat st n in Seg len f holds P[n,p.n] from FINSEQ_1:sch 5(A1);
take p;
thus len p = len f by A2,FINSEQ_1:def 3;
thus thesis by A2,A3;
end;
uniqueness
proof
let p1,p2 be FinSequence of REAL;
assume that
A4: len p1 = len f and
A5: for n be Element of NAT st n in dom p1 holds p1.n = f.n.d and
A6: len p2 = len f and
A7: for n be Element of NAT st n in dom p2 holds p2.n = f.n.d;
A8: dom p1=Seg len p1 by FINSEQ_1:def 3;
A9: dom p2=Seg len p2 by FINSEQ_1:def 3;
now
let n be Nat;
assume
A10: n in dom p1;
then p1.n = f.n.d by A5;
hence p1.n = p2.n by A4,A6,A7,A8,A9,A10;
end;
hence thesis by A4,A6,FINSEQ_2:9;
end;
end;
definition
let D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D;
pred d is_common_for_dom f means
for n be Nat st n in dom f holds d in dom (f.n);
end;
theorem Th26:
for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be
Element of D, n be Nat st d is_common_for_dom f & n <> 0 holds
d is_common_for_dom f|n
proof
let D1,D2 be non empty set, f be FinSequence of PFuncs(D1,D2), d1 be Element
of D1, n;
assume that
A1: d1 is_common_for_dom f and
A2: n<> 0;
let m;
assume
A3: m in dom (f|n);
set G = (f|n).m;
per cases;
suppose
n>=len f;
then f|n = f by Lm1;
hence thesis by A1,A3;
end;
suppose
A4: n<len f;
0+1<=n by A2,NAT_1:13;
then
A5: n in dom f by A4,FINSEQ_3:25;
dom(f|n) = Seg len(f|n) & len(f|n) = n by A4,FINSEQ_1:59,def 3;
then G = f.m & m in dom f by A3,A5,RFINSEQ:6;
hence thesis by A1;
end;
end;
theorem
for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be
Element of D, n be Nat st d is_common_for_dom f holds d
is_common_for_dom f /^ n
proof
let D1,D2 be non empty set, f be FinSequence of PFuncs(D1,D2), d1 be Element
of D1, n;
assume
A1: d1 is_common_for_dom f;
let m;
set fn = f /^ n;
assume
A2: m in dom fn;
set G = fn.m;
now
per cases;
case
len f<n;
hence thesis by A2,RELAT_1:38,RFINSEQ:def 1;
end;
case
A3: n<=len f;
1<=m & m<=m+n by A2,FINSEQ_3:25,NAT_1:11;
then
A4: 1<=m+n by XXREAL_0:2;
A5: m<=len fn by A2,FINSEQ_3:25;
len fn = len f - n by A3,RFINSEQ:def 1;
then m+n<=len f by A5,XREAL_1:19;
then
A6: m+n in dom f by A4,FINSEQ_3:25;
G= f.(m+n) by A2,A3,RFINSEQ:def 1;
hence thesis by A1,A6;
end;
end;
hence thesis;
end;
theorem Th28:
for D be non empty set, d be Element of D, f be FinSequence of
PFuncs(D,REAL) st len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f)
proof
let D be non empty set, d be Element of D;
defpred P[Nat] means for f be FinSequence of PFuncs(D,REAL) st
len f =$1 & len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f);
let f be FinSequence of PFuncs(D,REAL);
assume
A1: len f <> 0;
A2: for n st P[n] holds P[n+1]
proof
let n;
assume
A3: P[n];
let f be FinSequence of PFuncs(D,REAL);
assume that
A4: len f = n+1 and
len f <> 0;
A5: dom f = Seg len f by FINSEQ_1:def 3;
now
per cases;
case
A6: n=0;
then
A7: 1 in dom f by A4,FINSEQ_3:25;
then reconsider G = f.1 as Element of PFuncs(D,REAL) by FINSEQ_2:11;
f=<*G*> by A4,A6,FINSEQ_1:40;
then
A8: Sum(f) = G by FINSOP_1:11;
hence d is_common_for_dom f implies d in dom Sum(f) by A7;
assume d in dom Sum(f);
then for m st m in dom f holds
d in dom (f.m) by A4,A5,A6,A8,FINSEQ_1:2,TARSKI:def 1;
hence d is_common_for_dom f;
end;
case
A9: n <> 0;
A10: n<=n+1 by NAT_1:11;
0+1<=n by A9,NAT_1:13;
then
A11: n in dom f by A4,A10,FINSEQ_3:25;
0+1<=n+1 by NAT_1:13;
then
A12: n+1 in dom f by A4,FINSEQ_3:25;
then reconsider G=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:11;
set fn = f|n;
A13: len fn = n by A4,FINSEQ_1:59,NAT_1:11;
f = fn ^ <*G*> by A4,RFINSEQ:7;
then
A14: Sum(f) = Sum(fn) + G by Th20;
thus d is_common_for_dom f implies d in dom Sum(f)
proof
assume
A15: d is_common_for_dom f;
then d is_common_for_dom fn by A9,Th26;
then
A16: d in dom Sum(fn) by A3,A9,A13;
d in dom G by A12,A15;
then d in dom(Sum(fn)) /\ dom G by A16,XBOOLE_0:def 4;
hence thesis by A14,VALUED_1:def 1;
end;
assume d in dom Sum(f);
then
A17: d in dom(Sum(fn)) /\ dom G by A14,VALUED_1:def 1;
then d in dom(Sum(fn)) by XBOOLE_0:def 4;
then
A18: d is_common_for_dom fn by A3,A9,A13;
now
let m;
assume that
A19: m in dom f;
set F = f.m;
A20: m<=len f by A19,FINSEQ_3:25;
A21: 1<=m by A19,FINSEQ_3:25;
now
per cases;
case
m=len f;
hence d in dom F by A4,A17,XBOOLE_0:def 4;
end;
case
m<>len f;
then m<len f by A20,XXREAL_0:1;
then m<=n by A4,NAT_1:13;
then
A22: m in Seg n by A21,FINSEQ_1:1;
then dom fn = Seg len fn & F = fn.m
by A11,FINSEQ_1:def 3,RFINSEQ:6;
hence d in dom F by A13,A18,A22;
end;
end;
hence d in dom F;
end;
hence d is_common_for_dom f;
end;
end;
hence thesis;
end;
A23: P[ 0 ];
for n holds P[n] from NAT_1:sch 2(A23,A2);
hence thesis by A1;
end;
theorem Th29:
for D be non empty set, f be FinSequence of PFuncs(D,REAL), d be
Element of D, n be Nat holds (f|n)#d = (f#d)|n
proof
let D1 be non empty set, f be FinSequence of PFuncs(D1,REAL), d1 be Element
of D1, n be Nat;
A1: len(f#d1) = len f by Def8;
A2: len((f|n)#d1) = len(f|n) by Def8;
now
per cases;
case
A3: len f<=n;
then f|n = f by Lm1;
hence thesis by A1,A3,Lm1;
end;
case
A4: n<len f;
then
A5: len(f|n) = n by FINSEQ_1:59;
A6: len((f#d1)|n) = n by A1,A4,FINSEQ_1:59;
A7: dom f = Seg len f & dom(f#d1) = Seg len(f#d1) by FINSEQ_1:def 3;
A8: dom((f|n)#d1) = Seg len((f|n)#d1) by FINSEQ_1:def 3;
now
per cases;
case
A9: n=0;
thus thesis by A2,A9;
end;
case
A10: n<>0;
A11: dom ((f#d1)|n) = Seg len(f|n) by A5,A6,FINSEQ_1:def 3;
0+1<=n by A10,NAT_1:13;
then
A12: n in dom f by A4,FINSEQ_3:25;
now
let m be Nat;
assume
A13: m in dom ((f#d1)|n);
then
A14: m in dom (f#d1) by A1,A5,A7,A12,A11,RFINSEQ:6;
then reconsider G=f.m as Element of PFuncs(D1,REAL) by A1,A7,
FINSEQ_2:11;
((f#d1)|n).m = (f#d1).m by A1,A5,A7,A12,A11,A13,RFINSEQ:6;
then
A15: ((f#d1)|n).m = G.d1 by A14,Def8;
(f|n).m = G by A5,A12,A11,A13,RFINSEQ:6;
hence ((f#d1)|n).m = ((f|n)#d1).m by A2,A8,A11,A13,A15,Def8;
end;
hence thesis by A2,A5,A6,FINSEQ_2:9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th30:
for D be non empty set, f be FinSequence, d be Element of D
holds d is_common_for_dom CHI(f,D)
proof
let D be non empty set, f be FinSequence, d be Element of D;
let n;
assume n in dom CHI(f,D);
then CHI(f,D).n = chi(f.n,D) by Def6;
then dom (CHI(f,D).n) = D by RFUNCT_1:61;
hence thesis;
end;
theorem Th31:
for D be non empty set, d be Element of D, f be FinSequence of
PFuncs(D,REAL), R be FinSequence of REAL st d is_common_for_dom f holds d
is_common_for_dom R(#)f
proof
let D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL
), R be FinSequence of REAL;
assume
A1: d is_common_for_dom f;
set m = min(len R,len f);
let n;
assume
A2: n in dom (R(#)f);
set G = (R(#)f).n;
len(R(#)f) = m by Def7;
then m<=len f & n<=m by A2,FINSEQ_3:25,XXREAL_0:17;
then
A3: n<=len f by XXREAL_0:2;
1<=n by A2,FINSEQ_3:25;
then
A4: n in dom f by A3,FINSEQ_3:25;
then reconsider F=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:11;
A5: d in dom F by A1,A4;
reconsider r=R.n as Real;
G=r(#)F by A2,Def7;
hence thesis by A5,VALUED_1:def 5;
end;
theorem
for D be non empty set, f be FinSequence, R be FinSequence of REAL, d
be Element of D holds d is_common_for_dom R(#)CHI(f,D) by Th30,Th31;
theorem
for D be non empty set, d be Element of D, f be FinSequence of PFuncs(
D, REAL ) st d is_common_for_dom f holds (Sum(f)).d = Sum (f#d)
proof
let D be non empty set, d be Element of D;
defpred P[Nat] means for f be FinSequence of PFuncs(D,REAL) st
len f = $1 & d is_common_for_dom f holds (Sum(f)).d = Sum(f#d);
let f be FinSequence of PFuncs(D,REAL);
assume
A1: d is_common_for_dom f;
A2: len f = len f;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let f be FinSequence of PFuncs(D,REAL);
assume that
A5: len f = n+1 and
A6: d is_common_for_dom f;
set fn = f|n;
A7: len fn = n by A5,FINSEQ_1:59,NAT_1:11;
0+1<=n+1 by NAT_1:13;
then
A8: n+1 in dom f by A5,FINSEQ_3:25;
then reconsider G=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:11;
A9: dom f = Seg len f & dom(f#d) = Seg len(f#d) by FINSEQ_1:def 3;
f = fn ^ <*G*> by A5,RFINSEQ:7;
then
A10: Sum f = Sum fn + G by Th20;
A11: len (f#d)=len f by Def8;
A12: d in dom G by A6,A8;
now
per cases;
case
A13: n=0;
then
A14: len(f#d) = 1 by A5,Def8;
then
A15: 1 in dom(f#d) by FINSEQ_3:25;
A16: now
let m be Nat;
assume m in Seg 1;
then
A17: m=1 by FINSEQ_1:2,TARSKI:def 1;
hence (f#d).m=G.d by A13,A15,Def8
.=<*G.d*>.m by A17;
end;
len<*G.d*>=1 & dom (f#d) = Seg 1 by A14,FINSEQ_1:40,def 3;
then
A18: f#d = <*G.d*> by A14,A16,FINSEQ_2:9;
A19: G.d in REAL by XREAL_0:def 1;
f = <*G*> by A5,A13,FINSEQ_1:40;
hence (Sum f).d = G.d by FINSOP_1:11
.=Sum (f#d) by A18,A19,FINSOP_1:11;
end;
case
A20: n<>0;
A21: (f#d).(n+1) =G.d by A9,A11,A8,Def8;
d is_common_for_dom fn by A6,A20,Th26;
then d in dom(Sum(fn)) by A7,A20,Th28;
then d in dom(Sum(fn)) /\ dom G by A12,XBOOLE_0:def 4;
then d in dom(Sum(fn)+G) by VALUED_1:def 1;
hence (Sum f).d = (Sum fn).d + G.d by A10,VALUED_1:def 1
.= Sum(fn#d) + G.d by A4,A6,A7,A20,Th26
.= Sum((f#d)|n) + G.d by Th29
.= Sum(((f#d)|n)^<*G.d*>) by RVSUM_1:74
.= Sum(f#d) by A5,A11,A21,RFINSEQ:7;
end;
end;
hence thesis;
end;
A22: P[ 0 ]
proof
let f be FinSequence of PFuncs(D,REAL);
assume that
A23: len f = 0 and
d is_common_for_dom f;
f=<*> PFuncs(D,REAL) by A23;
then
A24: (Sum(f)).d = ([#](D)-->(0 qua Real)).d by Th19
.= 0 by FUNCOP_1:7;
len(f#d)=0 by A23,Def8;
then f#d = <*>PFuncs(D,REAL);
hence thesis by A24,RVSUM_1:72;
end;
for n holds P[n] from NAT_1:sch 2(A22,A3);
hence thesis by A1,A2;
end;
definition
let D be non empty set, F be PartFunc of D,REAL;
func max+(F) -> PartFunc of D,REAL means
:Def10:
dom it = dom F & for d be Element of D st d in dom it holds it.d = max+(F.d);
existence
proof
deffunc Q(set)=In(max+(F.$1),REAL);
defpred P[set] means $1 in dom F;
consider f be PartFunc of D,REAL such that
A1: for d be Element of D holds d in dom f iff P[d] and
A2: for d be Element of D st d in dom f holds f.d = Q(d) from SEQ_1:
sch 3;
take f;
thus dom f = dom F
proof
thus dom f c= dom F
by A1;
let x be object;
assume x in dom F;
hence thesis by A1;
end;
let d be Element of D;
assume d in dom f;
then f.d = Q(d) by A2;
hence thesis;
end;
uniqueness
proof
deffunc F(set)=max+(F.$1);
for f,g being PartFunc of D,REAL st (dom f=dom F & for c be Element of
D st c in dom f holds f.c = F(c)) & (dom g=dom F & for c be Element of D st c
in dom g holds g.c = F(c)) holds f = g from SEQ_1:sch 4;
hence thesis;
end;
func max-(F) -> PartFunc of D,REAL means
:Def11:
dom it = dom F & for d be Element of D st d in dom it holds it.d = max-(F.d);
existence
proof
deffunc F(set)=In(max-(F.$1),REAL);
defpred P[set] means $1 in dom F;
consider f be PartFunc of D,REAL such that
A3: for d be Element of D holds d in dom f iff P[d] and
A4: for d be Element of D st d in dom f holds f.d =F(d) from SEQ_1:sch
3;
take f;
thus dom f = dom F
proof
thus dom f c= dom F
by A3;
let x be object;
assume x in dom F;
hence thesis by A3;
end;
let d be Element of D;
assume d in dom f;
then f.d =F(d) by A4;
hence thesis;
end;
uniqueness
proof
deffunc F(set)=max-(F.$1);
for f,g being PartFunc of D,REAL st (dom f=dom F & for c be Element
of D st c in dom f holds f.c = F(c)) & (dom g=dom F & for c be Element of D st
c in dom g holds g.c = F(c)) holds f = g from SEQ_1:sch 4;
hence thesis;
end;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL holds F = max+(F) -
max-(F) & abs(F) = max+(F) + max-(F) & 2 (#) max+(F) = F + abs(F)
proof
let D be non empty set, F be PartFunc of D,REAL;
A1: dom F = dom F /\ dom F;
A2: dom max+(F) = dom F by Def10;
A3: dom max-(F) = dom F by Def11;
dom -max-(F) = dom max-(F) by VALUED_1:def 5;
then
A4: dom F =dom(max+(F) + -max-(F)) by A2,A3,A1,VALUED_1:def 1;
now
let d be Element of D;
assume
A5: d in dom F;
hence (max+(F) - max-(F)).d = max+(F).d - max-(F).d by A4,VALUED_1:13
.= max+(F.d) - max-(F).d by A2,A5,Def10
.= max+(F.d) - max-(F.d) by A3,A5,Def11
.= F.d by Th1;
end;
hence F = max+(F) - max-(F) by A4,PARTFUN1:5;
A6: dom abs(F) = dom F by VALUED_1:def 11;
then
A7: dom abs(F) = dom(max+(F) + max-(F)) by A2,A3,A1,VALUED_1:def 1;
now
let d be Element of D;
assume
A8: d in dom abs(F);
hence (max+(F) + max-(F)).d = max+(F).d + max-(F).d by A7,VALUED_1:def 1
.= max+(F.d) + max-(F).d by A2,A6,A8,Def10
.= max+(F.d) + max-(F.d) by A3,A6,A8,Def11
.= |.F.d.| by Th2
.= (abs(F)).d by VALUED_1:18;
end;
hence abs(F) = max+(F) + max-(F) by A7,PARTFUN1:5;
A9: dom(2(#)max+(F)) = dom max+(F) by VALUED_1:def 5;
then
A10: dom(2(#)max+(F)) = dom(F + abs(F)) by A2,A6,A1,VALUED_1:def 1;
now
let d be Element of D;
assume
A11: d in dom F;
hence (2(#)max+(F)).d = 2*(max+(F).d) by A2,A9,VALUED_1:def 5
.=2*max+(F.d) by A2,A11,Def10
.= F.d + |.F.d.| by Th3
.= F.d + (abs(F)).d by VALUED_1:18
.=(F+abs(F)).d by A2,A9,A10,A11,VALUED_1:def 1;
end;
hence thesis by A2,A9,A10,PARTFUN1:5;
end;
theorem Th35:
for D be non empty set, F be PartFunc of D,REAL, r st 0<
r holds F"{r} = max+(F)"{r}
proof
let D be non empty set, F be PartFunc of D,REAL, r;
A1: dom max+(F) = dom F by Def10;
assume
A2: 0<r;
thus F"{r} c= max+(F)"{r}
proof
let x be object;
assume
A3: x in F"{r};
then reconsider d=x as Element of D;
F.d in {r} by A3,FUNCT_1:def 7;
then
A4: F.d = r by TARSKI:def 1;
A5: d in dom F by A3,FUNCT_1:def 7;
then (max+(F)).d = max+(F.d) by A1,Def10
.= r by A2,A4,XXREAL_0:def 10;
then (max+(F)).d in {r} by TARSKI:def 1;
hence thesis by A1,A5,FUNCT_1:def 7;
end;
let x be object;
assume
A6: x in (max+ F)"{r};
then reconsider d=x as Element of D;
(max+ F).d in {r} by A6,FUNCT_1:def 7;
then
A7: (max+ F).d = r by TARSKI:def 1;
A8: d in dom F by A1,A6,FUNCT_1:def 7;
then (max+ F).d = max+(F.d) by A1,Def10
.= max(F.d,0);
then F.d = r by A2,A7,XXREAL_0:16;
then F.d in {r} by TARSKI:def 1;
hence thesis by A8,FUNCT_1:def 7;
end;
theorem Th36:
for D be non empty set, F be PartFunc of D,REAL holds F"(
left_closed_halfline(0)) = max+(F)"{0}
proof
set li = left_closed_halfline(0);
let D be non empty set, F be PartFunc of D,REAL;
A1: dom max+(F) = dom F by Def10;
A2: li = {s : s<=0} by XXREAL_1:231;
thus F" li c= max+(F)"{0}
proof
let x be object;
assume
A3: x in F" li;
then reconsider d=x as Element of D;
F.d in li by A3,FUNCT_1:def 7;
then ex s st s=F.d & s<=0 by A2;
then
A4: max(F.d,0) = 0 by XXREAL_0:def 10;
A5: d in dom F by A3,FUNCT_1:def 7;
then (max+(F)).d = max+(F.d) by A1,Def10
.= max(F.d,0);
then (max+(F)).d in {0} by A4,TARSKI:def 1;
hence thesis by A1,A5,FUNCT_1:def 7;
end;
let x be object;
assume
A6: x in (max+ F)"{0};
then reconsider d=x as Element of D;
(max+ F).d in {0} by A6,FUNCT_1:def 7;
then
A7: (max+ F).d = 0 by TARSKI:def 1;
A8: d in dom F by A1,A6,FUNCT_1:def 7;
then (max+ F).d = max+(F.d) by A1,Def10
.= max(F.d,0);
then F.d <= 0 by A7,XXREAL_0:def 10;
then F.d in li by A2;
hence thesis by A8,FUNCT_1:def 7;
end;
theorem Th37:
for D be non empty set, F be PartFunc of D,REAL, d be Element of
D holds 0<=(max+ F).d
proof
let D be non empty set, F be PartFunc of D,REAL, d be Element of D;
A1: dom F = dom (max+ F) by Def10;
per cases;
suppose
d in dom F;
then (max+ F).d = max+(F.d) by A1,Def10
.= max(F.d,0);
hence thesis by XXREAL_0:25;
end;
suppose
not d in dom F;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem Th38:
for D be non empty set, F be PartFunc of D,REAL, r st 0<
r holds F"{-r} = max-(F)"{r}
proof
let D be non empty set, F be PartFunc of D,REAL, r;
A1: dom max-(F) = dom F by Def11;
assume
A2: 0<r;
thus F"{-r} c= max-(F)"{r}
proof
let x be object;
assume
A3: x in F"{-r};
then reconsider d=x as Element of D;
F.d in {-r} by A3,FUNCT_1:def 7;
then
A4: F.d = -r by TARSKI:def 1;
A5: d in dom F by A3,FUNCT_1:def 7;
then (max-(F)).d = max-(F.d) by A1,Def11
.= r by A2,A4,XXREAL_0:def 10;
then (max-(F)).d in {r} by TARSKI:def 1;
hence thesis by A1,A5,FUNCT_1:def 7;
end;
let x be object;
assume
A6: x in (max- F)"{r};
then reconsider d=x as Element of D;
(max- F).d in {r} by A6,FUNCT_1:def 7;
then
A7: (max- F).d = r by TARSKI:def 1;
A8: d in dom F by A1,A6,FUNCT_1:def 7;
then (max- F).d = max-(F.d) by A1,Def11
.= max(-F.d,0);
then -F.d = r by A2,A7,XXREAL_0:16;
then F.d in {-r} by TARSKI:def 1;
hence thesis by A8,FUNCT_1:def 7;
end;
theorem Th39:
for D be non empty set, F be PartFunc of D,REAL holds F"(
right_closed_halfline(0)) = max-(F)"{0}
proof
set li = right_closed_halfline(0);
let D be non empty set, F be PartFunc of D,REAL;
A1: dom max-(F) = dom F by Def11;
A2: li = {s : 0<=s} by XXREAL_1:232;
thus F" li c= max-(F)"{0}
proof
let x be object;
assume
A3: x in F" li;
then reconsider d=x as Element of D;
F.d in li by A3,FUNCT_1:def 7;
then ex s st s=F.d & 0<=s by A2;
then
A4: max(-F.d,0) = 0 by XXREAL_0:def 10;
A5: d in dom F by A3,FUNCT_1:def 7;
then (max-(F)).d = max-(F.d) by A1,Def11
.= max(-F.d,0);
then (max-(F)).d in {0} by A4,TARSKI:def 1;
hence thesis by A1,A5,FUNCT_1:def 7;
end;
let x be object;
assume
A6: x in (max- F)"{0};
then reconsider d=x as Element of D;
(max- F).d in {0} by A6,FUNCT_1:def 7;
then
A7: (max- F).d = 0 by TARSKI:def 1;
A8: d in dom F by A1,A6,FUNCT_1:def 7;
then (max- F).d = max-(F.d) by A1,Def11
.= max(-F.d,0);
then -F.d <= -0 by A7,XXREAL_0:def 10;
then 0<=F.d by XREAL_1:24;
then F.d in li by A2;
hence thesis by A8,FUNCT_1:def 7;
end;
theorem Th40:
for D be non empty set, F be PartFunc of D,REAL, d be Element of
D holds 0<=(max- F).d
proof
let D be non empty set, F be PartFunc of D,REAL, d be Element of D;
A1: dom F = dom (max- F) by Def11;
per cases;
suppose
d in dom F;
then (max- F).d = max-(F.d) by A1,Def11
.= max(-F.d,0);
hence thesis by XXREAL_0:25;
end;
suppose
not d in dom F;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
REAL st F,G are_fiberwise_equipotent holds max+(F), max+(G)
are_fiberwise_equipotent
proof
set li =left_closed_halfline(0);
let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL;
assume
A1: F,G are_fiberwise_equipotent;
A2: now
let r be Element of REAL;
now
per cases;
case
0<r;
then Coim(F,r) = Coim(max+ F,r) & Coim(G,r) = Coim(max+ G,r) by Th35;
hence card Coim(max+ F,r) = card Coim(max+ G,r) by A1,CLASSES1:def 10;
end;
case
A3: r=0;
F" li = (max+ F)"{0} & G" li = (max+ G)"{0} by Th36;
hence card((max+ F)"{r}) = card((max+ G)"{r}) by A1,A3,CLASSES1:78;
end;
case
A4: r<0;
now
assume r in rng(max+ F);
then
ex d be Element of D st d in dom(max+ F) & (max+ F).d = r by PARTFUN1:3;
hence contradiction by A4,Th37;
end;
then
A5: (max+ F)"{r} = {} by Lm2;
now
assume r in rng(max+ G);
then
ex c be Element of C st c in dom(max+ G) & (max+ G).c = r by PARTFUN1:3;
hence contradiction by A4,Th37;
end;
hence card(( max+F)"{r}) = card(( max+ G)"{r}) by A5,Lm2;
end;
end;
hence card Coim(max+F,r) = card Coim(max+ G,r);
end;
rng(max+ F) c= REAL & rng(max+ G) c= REAL;
hence thesis by A2,CLASSES1:79;
end;
theorem
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
REAL st F,G are_fiberwise_equipotent holds max-(F), max-(G)
are_fiberwise_equipotent
proof
set li =right_closed_halfline(0);
let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL;
assume
A1: F,G are_fiberwise_equipotent;
A2: now
let r be Element of REAL;
now
per cases;
case
0<r;
then Coim(F,-r) = (max- F)"{r} & Coim(G,-r) = (max- G)"{r} by Th38;
hence card Coim(max- F,r) = card Coim(max- G,r) by A1,CLASSES1:def 10;
end;
case
A3: r=0;
F" li = (max- F)"{0} & G" li = (max- G)"{0} by Th39;
hence card((max- F)"{r}) = card((max- G)"{r}) by A1,A3,CLASSES1:78;
end;
case
A4: r<0;
now
assume r in rng(max- F);
then
ex d be Element of D st d in dom(max- F) & (max- F).d = r by PARTFUN1:3;
hence contradiction by A4,Th40;
end;
then
A5: (max- F)"{r} = {} by Lm2;
now
assume r in rng(max- G);
then
ex c be Element of C st c in dom(max- G) & (max- G).c = r by PARTFUN1:3;
hence contradiction by A4,Th40;
end;
hence card(( max-F)"{r}) = card(( max- G)"{r}) by A5,Lm2;
end;
end;
hence card Coim(max-F,r) = card Coim(max- G,r);
end;
rng(max- F) c= REAL & rng(max- G) c= REAL;
hence thesis by A2,CLASSES1:79;
end;
registration
let D be non empty set, F be finite PartFunc of D,REAL;
cluster max+(F) -> finite;
coherence
proof
dom F is finite;
then dom(max+(F)) is finite by Def10;
hence thesis by FINSET_1:10;
end;
cluster max-(F) -> finite;
coherence
proof
dom F is finite;
then dom(max-(F)) is finite by Def11;
hence thesis by FINSET_1:10;
end;
end;
theorem
for D,C be non empty set, F be finite PartFunc of D,REAL, G be finite
PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G
are_fiberwise_equipotent holds F, G are_fiberwise_equipotent
proof
let D,C be non empty set, F be finite PartFunc of D,REAL, G be finite
PartFunc of C,REAL;
assume that
A1: max+ F, max+ G are_fiberwise_equipotent and
A2: max- F, max- G are_fiberwise_equipotent;
set lh = left_closed_halfline(0), rh = right_closed_halfline(0), fp0 = (max+
F)"{0}, fm0 = (max- F)"{0}, gp0 = (max+ G)"{0}, gm0 = (max- G)"{0};
A3: lh /\ rh = [.0,0 .] by XXREAL_1:272
.= {0} by XXREAL_1:17;
F"(rng F) c= F"REAL by RELAT_1:143;
then
A4: F"REAL c= dom F & dom F c= F"REAL by RELAT_1:132,134;
A5: F"lh = fp0 & F"rh =fm0 by Th36,Th39;
G"(rng G) c= G"REAL by RELAT_1:143;
then
A6: G"REAL c= dom G & dom G c= G"REAL by RELAT_1:132,134;
A7: G"lh = gp0 & G"rh =gm0 by Th36,Th39;
reconsider fp0,fm0,gp0,gm0 as finite set;
A8: lh \/ rh = REAL \ ].0,0 .[ by XXREAL_1:398
.= REAL \ {} by XXREAL_1:28
.= REAL;
then fp0 \/ fm0 = F"(REAL) by A5,RELAT_1:140;
then
A9: fp0 \/ fm0 = dom F by A4;
gp0 \/ gm0 = G"(lh \/ rh) by A7,RELAT_1:140;
then
A10: gp0 \/ gm0 = dom G by A8,A6;
card(fp0 \/ fm0) = card fp0 + card fm0 - card(fp0 /\ fm0) by CARD_2:45;
then
A11: card(fp0 /\ fm0) = card fp0 + card fm0 - card(fp0 \/ fm0);
card(gp0 \/ gm0) = card gp0 + card gm0 - card(gp0 /\ gm0) by CARD_2:45;
then
A12: card(gp0 /\ gm0) = card gp0 + card gm0 - card(gp0 \/ gm0);
A13: dom F = dom(max+ F) & dom G = dom(max+ G) by Def10;
A14: now
let r be Element of REAL;
A15: card fp0 = card gp0 & card fm0 = card gm0 by A1,A2,CLASSES1:78;
now
per cases;
case
0<r;
then Coim(F,r) = Coim(max+ F,r) & Coim(G,r) = Coim(max+ G,r) by Th35;
hence card Coim(F,r) = card Coim(G,r) by A1,CLASSES1:def 10;
end;
case
0=r;
then F"{r} = F"lh /\ F"rh & G"{r} = G"lh /\ G"rh by A3,FUNCT_1:68;
hence card(F"{r}) = card(G"{r}) by A1,A13,A5,A7,A11,A12,A9,A10,A15,
CLASSES1:81;
end;
case
A16: r<0;
A17: --r=r;
0<-r by A16,XREAL_1:58;
then Coim(F,r) = Coim(max- F,-r) & Coim(G,r) = Coim(max- G,-r) by A17
,Th38;
hence card Coim(F,r) = card Coim(G,r) by A2,CLASSES1:def 10;
end;
end;
hence card Coim(F,r) = card Coim(G,r);
end;
rng F c= REAL & rng G c= REAL;
hence thesis by A14,CLASSES1:79;
end;
theorem Th44:
for D be non empty set, F be PartFunc of D,REAL, X be set holds
(max+ F)|X = max+ (F|X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
A1: dom((max+ F)|X) = dom(max+ F) /\ X by RELAT_1:61;
A2: dom(max+ F) /\ X= dom F /\ X by Def10
.= dom(F|X) by RELAT_1:61;
A3: dom(F|X) = dom(max+ (F|X)) by Def10;
now
let d be Element of D;
assume
A4: d in dom((max+ F)|X);
then
A5: d in dom(max+ F) by A1,XBOOLE_0:def 4;
thus ((max+ F)|X).d = (max+ F).d by A4,FUNCT_1:47
.=max+(F.d) by A5,Def10
.=max+((F|X).d) by A1,A2,A4,FUNCT_1:47
.=(max+ (F|X)).d by A1,A2,A3,A4,Def10;
end;
hence thesis by A2,A3,PARTFUN1:5,RELAT_1:61;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X be set holds (max-
F)|X = max- (F|X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
A1: dom((max- F)|X) = dom(max- F) /\ X by RELAT_1:61;
A2: dom(max- F) /\ X= dom F /\ X by Def11
.= dom(F|X) by RELAT_1:61;
A3: dom(F|X) = dom(max- (F|X)) by Def11;
now
let d be Element of D;
assume
A4: d in dom((max- F)|X);
then
A5: d in dom(max- F) by A1,XBOOLE_0:def 4;
thus ((max- F)|X).d = (max- F).d by A4,FUNCT_1:47
.=max-(F.d) by A5,Def11
.=max-((F|X).d) by A1,A2,A4,FUNCT_1:47
.=(max- (F|X)).d by A1,A2,A3,A4,Def11;
end;
hence thesis by A2,A3,PARTFUN1:5,RELAT_1:61;
end;
theorem Th46:
for D be non empty set, F be PartFunc of D,REAL st (for d be
Element of D st d in dom F holds F.d>=0) holds max+ F = F
proof
let D be non empty set, F be PartFunc of D,REAL;
A1: dom(max+ F) = dom F by Def10;
assume
A2: for d be Element of D st d in dom F holds F.d>=0;
now
let d be Element of D;
assume
A3: d in dom F;
then
A4: F.d>=0 by A2;
thus (max+ F).d = max+(F.d) by A1,A3,Def10
.= F.d by A4,XXREAL_0:def 10;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL st (for d be Element
of D st d in dom F holds F.d<=0) holds max- F = -F
proof
let D be non empty set, F be PartFunc of D,REAL;
A1: dom(max- F) = dom F by Def11;
assume
A2: for d be Element of D st d in dom F holds F.d<=0;
A3: now
let d be Element of D;
assume
A4: d in dom F;
then
A5: F.d<=0 by A2;
thus (max- F).d = max-(F.d) by A1,A4,Def11
.= -F.d by A5,XXREAL_0:def 10
.= (-F).d by VALUED_1:8;
end;
dom F = dom(-F) by VALUED_1:8;
hence thesis by A1,A3,PARTFUN1:5;
end;
theorem Th48:
for D be non empty set, F be PartFunc of D,REAL holds F - 0 = F
proof
let D be non empty set, F be PartFunc of D,REAL;
A1: now
let d be Element of D;
assume d in dom F;
hence (F - 0).d = F.d - 0 by VALUED_1:3
.= F.d;
end;
dom(F - 0) = dom F by VALUED_1:3;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set
holds (F|X) - r = (F-r)| X
proof
let D be non empty set, F be PartFunc of D,REAL, r be Real, X be set;
A1: dom ((F|X) - r) = dom (F|X) by VALUED_1:3;
A2: dom (F|X) = dom F /\ X by RELAT_1:61;
A3: dom F /\ X = dom(F-r) /\ X by VALUED_1:3
.= dom((F-r)|X) by RELAT_1:61;
now
let d be Element of D;
assume
A4: d in dom ((F|X) - r);
then
A5: d in dom F by A1,A2,XBOOLE_0:def 4;
thus ((F|X) - r).d = (F|X).d - r by A1,A4,VALUED_1:3
.= F.d -r by A1,A4,FUNCT_1:47
.= (F-r).d by A5,VALUED_1:3
.=((F-r)|X).d by A1,A2,A3,A4,FUNCT_1:47;
end;
hence thesis by A2,A3,PARTFUN1:5,VALUED_1:3;
end;
theorem Th50:
for D be non empty set, F be PartFunc of D,REAL, r,s
holds F"{s+r} = (F-r)"{s}
proof
let D be non empty set, F be PartFunc of D,REAL, r,s;
thus F"{s+r} c= (F-r)"{s}
proof
let x be object;
assume
A1: x in F"{s+r};
then reconsider d=x as Element of D;
A2: d in dom F by A1,FUNCT_1:def 7;
F.d in {s+r} by A1,FUNCT_1:def 7;
then F.d = s+r by TARSKI:def 1;
then F.d - r = s;
then (F-r).d = s by A2,VALUED_1:3;
then
A3: (F-r).d in {s} by TARSKI:def 1;
d in dom(F-r) by A2,VALUED_1:3;
hence thesis by A3,FUNCT_1:def 7;
end;
let x be object;
assume
A4: x in (F-r)"{s};
then reconsider d=x as Element of D;
d in dom(F-r) by A4,FUNCT_1:def 7;
then
A5: d in dom F by VALUED_1:3;
(F-r).d in {s} by A4,FUNCT_1:def 7;
then (F-r).d = s by TARSKI:def 1;
then F.d -r= s by A5,VALUED_1:3;
then F.d in {s+r} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
theorem
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
REAL , r be Real holds F, G are_fiberwise_equipotent iff F-r,G-r
are_fiberwise_equipotent
proof
let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL,
r be Real;
A1: rng(F-r) c= REAL & rng(G-r) c= REAL;
thus F, G are_fiberwise_equipotent implies F-r, G-r are_fiberwise_equipotent
proof
assume
A2: F, G are_fiberwise_equipotent;
now
let s be Element of REAL;
thus card Coim(F-r,s) = card Coim(F,s+r) by Th50
.= card Coim(G,s+r) by A2,CLASSES1:def 10
.= card Coim(G-r,s) by Th50;
end;
hence thesis by A1,CLASSES1:79;
end;
assume
A3: F-r, G-r are_fiberwise_equipotent;
A4: now
let s be Element of REAL;
A5: s = s-r+r;
hence card Coim(F,s) = card Coim(F-r,s-r) by Th50
.= card Coim(G- r,s-r) by A3,CLASSES1:def 10
.= card Coim(G,s) by A5,Th50;
end;
rng F c= REAL & rng G c= REAL;
hence thesis by A4,CLASSES1:79;
end;
definition
let F be PartFunc of REAL,REAL, X be set;
pred F is_convex_on X means
X c= dom F & for p be Real st 0<=p & p<=1
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X
holds F.(p*r +(1-p)*s) <= p*F.r + (1-p)*F.s;
end;
theorem
for a,b be Real, F be PartFunc of REAL,REAL holds F is_convex_on
[.a,b.] iff [.a,b.] c= dom F &
for p be Real st 0<=p & p<=1
for r,s be Real st r in [.a,b.] & s in [.a,b.]
holds F.(p*r + (1-p)*s) <= p*F.r + (1-p)*F.s
proof
let a,b be Real, f be PartFunc of REAL,REAL;
set ab = {r: a<=r & r<=b};
A1: [.a,b.]= ab by RCOMP_1:def 1;
thus f is_convex_on [.a,b.] implies [.a,b.] c= dom f &
for p be Real st 0<=p
& p<=1 holds
for x,y be Real st x in [.a,b.] & y in [.a,b.] holds f.(p*x + (1-p
)*y) <= p* f.x + (1-p)*f.y
proof
assume
A2: f is_convex_on [.a,b.];
hence [.a,b.] c= dom f;
let p be Real;
assume that
A3: 0<=p and
A4: p<=1;
A5: 0<=1-p by A4,XREAL_1:48;
A6: p*b+(1-p)*b=b;
A7: p*a+(1-p)*a=a;
let x,y be Real;
assume that
A8: x in [.a,b.] and
A9: y in [.a,b.];
A10: ex r2 st r2=y & a<=r2 & r2<=b by A1,A9;
then
A11: (1-p)*y<=(1-p)*b by A5,XREAL_1:64;
A12: ex r1 st r1=x & a<=r1 & r1<=b by A1,A8;
then p*x<=p*b by A3,XREAL_1:64;
then
A13: p*x+(1-p)*y<=b by A11,A6,XREAL_1:7;
A14: (1-p)*a<=(1-p)*y by A5,A10,XREAL_1:64;
p*a<=p*x by A3,A12,XREAL_1:64;
then a<=p*x+(1-p)*y by A14,A7,XREAL_1:7;
then p*x+(1-p)*y in ab by A13;
hence thesis by A1,A2,A3,A4,A8,A9;
end;
assume that
A15: [.a,b.] c= dom f and
A16: for p be Real
st 0<=p & p<=1 holds for x,y be Real st x in [.a,b.]
& y in [.a,b.] holds f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
thus [.a,b.] c= dom f by A15;
let p be Real;
assume
A17: 0<=p & p<=1;
let x,y be Real;
assume that
A18: x in [.a,b.] & y in [.a,b.] and
p*x + (1-p)*y in [.a,b.];
thus thesis by A16,A17,A18;
end;
theorem
for a,b be Real,
F be PartFunc of REAL,REAL holds F is_convex_on [.a,b
.] iff [.a,b.] c= dom F &
for x1,x2,x3 be Real st x1 in [.a,b.] & x2 in [.a,b.]
& x3 in [.a,b.] & x1<x2 & x2<x3 holds (F.x1-F.x2)/(x1-x2)<=(F.x2-F.x3)/(x2-x3)
proof
let a,b be Real, f be PartFunc of REAL,REAL;
thus f is_convex_on [.a,b.] implies [.a,b.] c= dom f &
for x1,x2,x3 be Real
st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1<x2 & x2<x3 holds (f.x1 -
f.x2)/(x1 - x2) <= (f.x2 - f.x3)/(x2 - x3)
proof
assume
A1: f is_convex_on [.a,b.];
hence [.a,b.] c= dom f;
let x1,x2,x3 be Real;
assume that
A2: x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] and
A3: x1<x2 and
A4: x2<x3;
A5: x2-x3<0 by A4,XREAL_1:49;
set r = (x2-x3)/(x1-x3);
A6: r*(f.x2-f.x1)=r*f.x2 -r*f.x1 & (1-r)*(f.x3-f.x2)=(1-r)*f.x3-(1-r)*f. x2;
A7: (x1-x2)/(x1-x3)=(x1-x3)"*(x1-x2) by XCMPLX_0:def 9;
x1<x3 by A3,A4,XXREAL_0:2;
then
A8: x1-x3<0 by XREAL_1:49;
A9: r + (x1-x2)/(x1-x3) = ((x1-x2) + (x2-x3))/(x1-x3) by XCMPLX_1:62
.= 1 by A8,XCMPLX_1:60;
then
A10: r*x1 + (1-r)*x3= (x1*(x2-x3))/(x1-x3)+x3*((x1-x2)/(x1-x3)) by XCMPLX_1:74
.= (x1*(x2-x3))/(x1-x3)+(x3*(x1-x2))/(x1-x3) by XCMPLX_1:74
.=((x2*x1-x3*x1)+(x1-x2)*x3)/(x1-x3) by XCMPLX_1:62
.=x2*(x1-x3)/(x1-x3)
.=x2 by A8,XCMPLX_1:89;
A11: x1-x2<0 by A3,XREAL_1:49;
then r<=1 by A8,A9,XREAL_1:29,140;
then r*f.x2+(1-r)*f.x2<=r*f.x1+(1-r)*f.x3 by A1,A2,A5,A8,A10;
then r*(f.x2-f.x1)<=(1-r)*(f.x3-f.x2) by A6,XREAL_1:21;
then -((1-r)*(f.x3-f.x2))<=-(r*(f.x2-f.x1)) by XREAL_1:24;
then (1-r)*(-(f.x3-f.x2))<=r*(-(f.x2-f.x1));
then (x1-x3)"*(x1-x2)*(f.x2-f.x3)<=(x1-x3)"*(x2-x3)*(f.x1-f.x2) by A9,A7,
XCMPLX_0:def 9;
then
A12: (x1-x3)*((x1-x3)"*(x2-x3)*(f.x1-f.x2))<= (x1-x3)*((x1-x3)"*(x1-x2)*(f
.x2-f.x3)) by A8,XREAL_1:65;
set v=(x1-x2)*(f.x2-f.x3);
set u=(x2-x3)*(f.x1-f.x2);
A13: (x1-x3)*((x1-x3)"*(x1-x2)*(f.x2-f.x3))=((x1-x3)*(x1-x3)")*v
.=1*v by A8,XCMPLX_0:def 7
.=v;
(x1-x3)*((x1-x3)"*(x2-x3)*(f.x1-f.x2))=((x1-x3)*(x1-x3)")*u
.=1*u by A8,XCMPLX_0:def 7
.=u;
hence thesis by A5,A11,A12,A13,XREAL_1:103;
end;
assume that
A14: [.a,b.] c= dom f and
A15: for x1,x2,x3 be Real
st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b
.] & x1<x2 & x2<x3 holds (f.x1-f.x2)/(x1-x2)<=(f.x2-f.x3)/(x2-x3);
now
let p be Real;
assume that
A16: 0<=p and
A17: p<=1;
A18: 0<=1-p by A17,XREAL_1:48;
let x,y be Real;
set r = p*x+(1-p)*y;
assume that
A19: x in [.a,b.] and
A20: y in [.a,b.];
A21: p*y+(1-p)*y = y;
A22: {s: a<=s & s<=b} = [.a,b.] by RCOMP_1:def 1;
then
A23: ex t st t=y & a<=t & t <=b by A20;
then
A24: (1-p)*y<=(1-p)*b by A18,XREAL_1:64;
A25: ex t st t=x & a<=t & t<=b by A22,A19;
then p*b+(1-p)*b = b & p*x<=p*b by A16,XREAL_1:64;
then
A26: r<=b by A24,XREAL_1:7;
A27: (1-p)*a<=(1-p)*y by A18,A23,XREAL_1:64;
p*a+(1-p)*a = a & p*a<=p*x by A16,A25,XREAL_1:64;
then a<=r by A27,XREAL_1:7;
then
A28: r in [.a,b.] by A22,A26;
A29: p*x+(1-p)*x = x;
now
per cases;
case
x=y;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
case
A30: x<>y;
now
per cases;
case
p=0;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
case
A31: p<>0;
now
per cases;
case
p=1;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
case
p<>1;
then p<1 by A17,XXREAL_0:1;
then
A32: 0<1-p by XREAL_1:50;
now
per cases by A30,XXREAL_0:1;
case
A33: x<y;
then (1-p)*x < (1-p)*y by A32,XREAL_1:68;
then
A34: x<r by A29,XREAL_1:8;
then
A35: x-r<0 by XREAL_1:49;
p*x < p*y by A16,A31,A33,XREAL_1:68;
then
A36: r<y by A21,XREAL_1:8;
then
A37: r-y<0 by XREAL_1:49;
A38: x-y<0 by A33,XREAL_1:49;
(f.x-f.r)/(x-r)<=(f.r-f.y)/(r-y) by A15,A19,A20,A28,A36,A34
;
then (f.x-f.r)*(p*(x-y))<=(f.r-f.y)*((1-p)*(x-y)) by A37
,A35,XREAL_1:107;
then (f.x-f.r)*p*(x-y)/(x-y)>=(f.r-f.y)*(1-p)*(x-y)/(x-y)
by A38,XREAL_1:73;
then (f.r-f.y)*(1-p)*(x-y)/(x-y)<=(f.x-f.r)*p by A38,
XCMPLX_1:89;
then f.r *(1-p) - f.y*(1-p) <= f.x *p - f.r *p by A38,
XCMPLX_1:89;
then f.r *p + (f.r *(1-p) - f.y*(1-p)) <= f.x *p by
XREAL_1:19;
then f.r *p + f.r *(1-p) - f.y*(1-p) <= f.x *p;
hence f.r <= p*f.x + (1-p)*f.y by XREAL_1:20;
end;
case
A39: y<x;
then (1-p)*y < (1-p)*x by A32,XREAL_1:68;
then
A40: r<x by A29,XREAL_1:8;
then
A41: r-x<0 by XREAL_1:49;
p*y < p*x by A16,A31,A39,XREAL_1:68;
then
A42: y<r by A21,XREAL_1:8;
then
A43: y-r<0 by XREAL_1:49;
A44: y-x<0 by A39,XREAL_1:49;
(f.y-f.r)/(y-r)<=(f.r-f.x)/(r-x) by A15,A19,A20,A28,A42,A40
;
then (f.y-f.r)*((1-p)*(y-x))<=(f.r-f.x)*(p*(y-x)) by A43
,A41,XREAL_1:107;
then (f.y-f.r)*(1-p)*(y-x)/(y-x)>=(f.r-f.x)*p*(y-x)/(y-x)
by A44,XREAL_1:73;
then (f.r-f.x)*p*(y-x)/(y-x)<=(f.y-f.r)*(1-p) by A44,
XCMPLX_1:89;
then
f.r *p - f.x *p <= f.y *(1-p) - f.r *(1-p) by A44,XCMPLX_1:89;
then f.r *p - f.x *p + f.r *(1-p) <= f.y *(1-p) by
XREAL_1:19;
then f.r *p + f.r *(1-p) - f.x *p <= f.y *(1-p);
hence f.r <= p*f.x + (1-p)*f.y by XREAL_1:20;
end;
end;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
end;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
end;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
end;
hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y;
end;
hence thesis by A14;
end;
theorem
for F be PartFunc of REAL,REAL, X,Y be set st F is_convex_on X & Y c=
X holds F is_convex_on Y
proof
let F be PartFunc of REAL,REAL, X,Y be set;
assume that
A1: F is_convex_on X and
A2: Y c= X;
X c= dom F by A1;
hence Y c= dom F by A2;
let p be Real;
assume
A3: 0<=p & p<=1;
let x,y be Real;
assume x in Y & y in Y & p*x+(1-p)*y in Y;
hence thesis by A1,A2,A3;
end;
theorem
for F be PartFunc of REAL,REAL, X be set, r holds F
is_convex_on X iff F-r is_convex_on X
proof
let F be PartFunc of REAL,REAL, X be set, r;
A1: dom F = dom(F-r) by VALUED_1:3;
thus F is_convex_on X implies F-r is_convex_on X
proof
assume
A2: F is_convex_on X;
hence
A3: X c= dom(F-r) by A1;
let p be Real;
assume
A4: 0<=p & p<=1;
let x,y be Real;
assume that
A5: x in X and
A6: y in X and
A7: p*x + (1-p)*y in X;
F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y by A2,A4,A5,A6,A7;
then
A8: F.(p*x+(1-p)*y) - r <= p*F.x + (1-p)*F.y -r by XREAL_1:9;
p*F.x + (1-p)*F.y - r = p*(F.x -r) + (1-p)*(F.y - r)
.= p*(F-r).x + (1-p)*(F.y - r) by A1,A3,A5,VALUED_1:3
.= p*(F-r).x + (1-p)*(F-r).y by A1,A3,A6,VALUED_1:3;
hence thesis by A1,A3,A7,A8,VALUED_1:3;
end;
assume
A9: F-r is_convex_on X;
hence
A10: X c= dom F by A1;
let p be Real;
assume
A11: 0<=p & p<=1;
let x,y be Real;
assume that
A12: x in X and
A13: y in X and
A14: p*x + (1-p)*y in X;
(F-r).(p*x+(1-p)*y) <= p*(F-r).x + (1-p)*(F-r).y by A9,A11,A12,A13,A14;
then
A15: F.(p*x+(1-p)*y) -r <= p*(F-r).x + (1-p)*(F-r).y by A10,A14,VALUED_1:3;
p*(F-r).x + (1-p)*(F-r).y = p*(F-r).x + (1-p)*(F.y - r) by A10,A13,VALUED_1:3
.= p*(F.x - r) + ((1-p)*F.y - (1-p)*r) by A10,A12,VALUED_1:3
.= p*F.x + (1-p)*F.y - r;
hence thesis by A15,XREAL_1:9;
end;
theorem
for F be PartFunc of REAL,REAL, X be set, r st 0<r holds F
is_convex_on X iff r(#)F is_convex_on X
proof
let F be PartFunc of REAL,REAL, X be set, r;
assume
A1: 0<r;
A2: dom F = dom(r(#)F) by VALUED_1:def 5;
thus F is_convex_on X implies r(#)F is_convex_on X
proof
assume
A3: F is_convex_on X;
then
A4: X c= dom F;
thus X c= dom(r(#)F) by A2,A3;
let p be Real;
assume
A5: 0<=p & p<=1;
let x,y be Real;
assume that
A6: x in X and
A7: y in X and
A8: p*x+(1-p)*y in X;
F.(p*x+(1-p)*y)<=p*F.x + (1-p)*F.y by A3,A5,A6,A7,A8;
then r* F.(p*x+(1-p)*y)<=r*(p*F.x + (1-p)*F.y) by A1,XREAL_1:64;
then (r(#)F).(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*r*F.y by A2,A4,A8,
VALUED_1:def 5;
then (r(#)F).(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r*F.y) by A2,A4,A6,
VALUED_1:def 5;
hence thesis by A2,A4,A7,VALUED_1:def 5;
end;
assume
A9: r(#)F is_convex_on X;
then
A10: X c= dom(r(#)F);
hence X c= dom F by VALUED_1:def 5;
let p be Real;
assume
A11: 0<=p & p<=1;
let x,y be Real;
assume that
A12: x in X and
A13: y in X and
A14: p*x+(1-p)*y in X;
(r(#)F).(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r(#)F).y by A9,A11,A12,A13,A14;
then r*F.(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r(#)F).y by A10,A14,
VALUED_1:def 5;
then r*F.(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*(r(#)F).y by A10,A12,VALUED_1:def 5
;
then r*F.(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*(r*F.y) by A10,A13,VALUED_1:def 5;
then r*F.(p*x+(1-p)*y)/r <= r*(p*F.x + (1-p)*F.y)/r by A1,XREAL_1:72;
then F.(p*x+(1-p)*y) <= r*(p*F.x + (1-p)*F.y)/r by A1,XCMPLX_1:89;
hence thesis by A1,XCMPLX_1:89;
end;
theorem
for F be PartFunc of REAL,REAL, X be set st X c= dom F holds 0(#) F
is_convex_on X
proof
let F be PartFunc of REAL,REAL, X be set;
assume
A1: X c= dom F;
hence X c= dom(0(#)F) by VALUED_1:def 5;
let p be Real;
assume that
0<=p and
p<=1;
let x,y be Real;
assume that
A2: x in X and
A3: y in X and
A4: p*x + (1-p)*y in X;
A5: dom F = dom(0(#)F) by VALUED_1:def 5;
then
A6: (0(#)F).(p*x+(1-p)*y) = 0* F.(p*x+(1-p)*y) by A1,A4,VALUED_1:def 5
.= 0;
p*(0(#)F).x + (1-p)*(0(#)F).y = p*(0* F.x) + (1-p)*(0(#)F).y by A1,A5,A2,
VALUED_1:def 5
.= p*0 + (1-p)*(0* F.y) by A1,A5,A3,VALUED_1:def 5
.= 0 + 0;
hence thesis by A6;
end;
theorem
for F,G be PartFunc of REAL,REAL, X be set st F is_convex_on X & G
is_convex_on X holds F+G is_convex_on X
proof
let F,G be PartFunc of REAL,REAL, X be set;
A1: dom(F+G) = dom F /\ dom G by VALUED_1:def 1;
assume
A2: F is_convex_on X & G is_convex_on X;
then X c= dom F & X c= dom G;
hence
A3: X c= dom(F+G) by A1,XBOOLE_1:19;
let p be Real;
assume
A4: 0<=p & p<=1;
let x,y be Real;
assume that
A5: x in X and
A6: y in X and
A7: p*x + (1-p)*y in X;
F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y & G.(p*x+(1-p)*y) <= p*G.x + (1-p)
*G.y by A2,A4,A5,A6,A7;
then
F.(p*x+(1-p)*y) + G.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y + (p*G.x + (1-p)
*G.y) by XREAL_1:7;
then
A8: (F+G).(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y + (p*G.x + (1-p)*G.y) by A3,A7,
VALUED_1:def 1;
p*F.x+(1-p)*F.y + (p*G.x+(1-p)*G.y) = p*(F.x+G.x) + (1-p)*F.y + (1-p)*G . y
.= p*(F+G).x + (1-p)*F.y + (1-p)*G.y by A3,A5,VALUED_1:def 1
.= p*(F+G).x + (1-p)*(F.y + G.y);
hence thesis by A3,A6,A8,VALUED_1:def 1;
end;
theorem Th59:
for F be PartFunc of REAL,REAL, X be set, r st F
is_convex_on X holds max+(F-r) is_convex_on X
proof
let F be PartFunc of REAL,REAL, X be set, r;
assume
A1: F is_convex_on X;
then
A2: X c= dom F;
A3: dom F = dom(F-r) & dom(max+(F-r)) = dom(F-r) by Def10,VALUED_1:3;
hence X c= dom(max+(F-r)) by A1;
let p be Real;
assume that
A4: 0<=p and
A5: p<=1;
let x,y be Real;
assume that
A6: x in X and
A7: y in X and
A8: p*x+(1-p)*y in X;
F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y by A1,A4,A5,A6,A7,A8;
then F.(p*x+(1-p)*y) -r <= p*F.x + (1-p)*F.y -r by XREAL_1:9;
then
A9: max+(F.(p*x+(1-p)*y) -r) <= max(p*F.x + (1-p)*F.y -r,0) by XXREAL_0:26;
0+p<=1 by A5;
then 0<=1-p by XREAL_1:19;
then
A10: max+((1-p)*(F-r).y) = (1-p)*(max+ ((F-r).y)) by Th4;
A11: max+(p*(F-r).x + (1-p)*(F-r).y)<= max+(p*(F-r).x) + max+((1-p)*(F-r).y)
by Th5;
A12: max+(p*(F-r).x)= p* (max+ ((F-r).x)) by A4,Th4;
reconsider pc = p*x+(1-p)*y as Element of REAL by XREAL_0:def 1;
reconsider x,y as Element of REAL by XREAL_0:def 1;
p*F.x + (1-p)*F.y - r = p*(F.x -r) + (1-p)*(F.y - r)
.= p*(F-r).x + (1-p)*(F.y - r) by A6,A2,VALUED_1:3
.= p*(F-r).x + (1-p)*(F-r).y by A7,A2,VALUED_1:3;
then
max+(F.(p*x+(1-p)*y) -r) <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y))
by A9,A11,A12,A10,XXREAL_0:2;
then
max+ ((F-r).pc) <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y
)) by A8,A2,VALUED_1:3;
then
(max+ (F-r)).pc <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y
)) by A3,A8,A2,Def10;
then
(max+ (F-r)).pc <= p*(max+ (F-r)).x + (1-p)*(max+ ((F-r).y))
by A3,A6,A2,Def10;
hence thesis by A3,A7,A2,Def10;
end;
theorem
for F be PartFunc of REAL,REAL, X be set st F is_convex_on X holds
max+ F is_convex_on X
proof
let F be PartFunc of REAL,REAL, X be set;
assume F is_convex_on X;
then max+(F - 0) is_convex_on X by Th59;
hence thesis by Th48;
end;
theorem Th61:
id [#](REAL) is_convex_on REAL
proof
set i = id [#](REAL);
thus REAL c= dom i by FUNCT_1:17;
let p be Real;
assume that
0<=p and
p<=1;
let x,y be Real;
assume that
A1: x in REAL and
A2: y in REAL and
A3: p*x+(1-p)*y in REAL;
i.x = x & i.y = y by A1,A2,FUNCT_1:17;
hence thesis by A3,FUNCT_1:17;
end;
theorem
for r be Real holds max+(id [#](REAL) - r) is_convex_on REAL by Th59,Th61;
definition
let D be non empty set, F be PartFunc of D,REAL, X be set;
assume
A1: dom(F|X) is finite;
func FinS(F,X) -> non-increasing FinSequence of REAL means
:Def13:
F|X, it are_fiberwise_equipotent;
existence
proof
set x = dom(F|X);
consider b be FinSequence such that
A2: F|x, b are_fiberwise_equipotent by A1,RFINSEQ:5;
rng(F|x) = rng b by A2,CLASSES1:75;
then reconsider b as FinSequence of REAL by FINSEQ_1:def 4;
consider a be non-increasing FinSequence of REAL such that
A3: b,a are_fiberwise_equipotent by RFINSEQ:22;
take a;
x = dom F /\ X by RELAT_1:61;
then F|x = (F|dom F)|X by RELAT_1:71
.=F|X by RELAT_1:68;
hence thesis by A2,A3,CLASSES1:76;
end;
uniqueness by CLASSES1:76,RFINSEQ:23;
end;
theorem Th63:
for D be non empty set, F be PartFunc of D,REAL, X be set st dom
(F|X) is finite holds FinS(F,dom(F|X)) = FinS(F,X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
A1: F|(dom(F|X)) = F|(dom F /\ X) by RELAT_1:61
.= (F|dom F)|X by RELAT_1:71
.= F|X by RELAT_1:68;
assume
A2: dom(F|X) is finite;
then FinS(F,X), F|X are_fiberwise_equipotent by Def13;
hence thesis by A2,A1,Def13;
end;
theorem Th64:
for D be non empty set, F be PartFunc of D,REAL, X be set st dom
(F|X) is finite holds FinS(F|X,X) = FinS(F,X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
A1: (F|X)|X = F|X by RELAT_1:72;
assume
A2: dom(F|X) is finite;
then FinS(F,X), F|X are_fiberwise_equipotent by Def13;
hence thesis by A2,A1,Def13;
end;
theorem Th65:
for D be non empty set, d be Element of D, X be set,
F be PartFunc of D,REAL st
X is finite & d in dom(F|X) holds
FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent
proof
for D be non empty set, X be finite set, F be PartFunc of D,REAL, x be
object st x in dom(F|X)
holds FinS(F,X\{x})^<*F.x*>, F|X are_fiberwise_equipotent
proof
let D be non empty set, X be finite set, F be PartFunc of D,REAL,
x be object;
set Y = X \ {x};
set A = FinS(F,Y)^<* F.x *>;
assume x in dom(F|X);
then
A1: x in dom F /\ X by RELAT_1:61;
then x in X by XBOOLE_0:def 4;
then
A2: {x} c= X by ZFMISC_1:31;
x in dom F by A1,XBOOLE_0:def 4;
then
A3: {x} c= dom F by ZFMISC_1:31;
dom(F|Y) is finite;
then
A4: F|Y, FinS(F,Y) are_fiberwise_equipotent by Def13;
now
let y be object;
A5: Y misses {x} by XBOOLE_1:79;
A6: card Coim(F|Y,y) = card Coim(FinS(F,Y),y) by A4,CLASSES1:def 10;
A7: dom(F|{x}) = {x} by A3,RELAT_1:62;
A8: dom<*F.x*> = {1} by FINSEQ_1:2,38;
A9: now
per cases;
case
A10: y=F.x;
A11: {x} c= (F|{x})"{y}
proof
let z be object;
A12: y in {y} by TARSKI:def 1;
assume
A13: z in {x};
then z=x by TARSKI:def 1;
then y=(F|{x}).z by A7,A10,A13,FUNCT_1:47;
hence thesis by A7,A13,A12,FUNCT_1:def 7;
end;
(F|{x})"{y} c= {x} by A7,RELAT_1:132;
then (F|{x})"{y} = {x} by A11;
then
A14: card((F|{x})"{y}) = 1 by CARD_1:30;
A15: {1} c= <*F.x*>"{y}
proof
let z be object;
A16: y in {y} by TARSKI:def 1;
assume
A17: z in {1};
then z=1 by TARSKI:def 1;
then y=<*F.x*>.z by A10;
hence thesis by A8,A17,A16,FUNCT_1:def 7;
end;
<*F.x*>"{y} c= {1} by A8,RELAT_1:132;
then <*F.x*>"{y} = {1} by A15;
hence card((F|{x})"{y}) = card(<*F.x*>"{y}) by A14,CARD_1:30;
end;
case
A18: y <> F.x;
A19: now
set z = the Element of <*F.x*>"{y};
assume
A20: <*F.x*>"{y} <> {};
then <*F.x*>.z in {y} by FUNCT_1:def 7;
then
A21: <*F.x*>.z=y by TARSKI:def 1;
z in {1} by A8,A20,FUNCT_1:def 7;
then z=1 by TARSKI:def 1;
hence contradiction by A18,A21;
end;
now
set z = the Element of (F|{x})"{y};
assume
A22: (F|{x})"{y} <> {};
then (F|{x}).z in {y} by FUNCT_1:def 7;
then
A23: (F|{x}).z=y by TARSKI:def 1;
A24: z in {x} by A7,A22,FUNCT_1:def 7;
then z=x by TARSKI:def 1;
hence contradiction by A7,A18,A24,A23,FUNCT_1:47;
end;
hence card((F|{x})"{y}) = card(<*F.x*>"{y}) by A19;
end;
end;
A25: (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 A2,XBOOLE_1:12
.= (F|X)"{y} by FUNCT_1:70;
(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 A5
.= {};
hence
card Coim(F|X,y) = card((F|Y)"{y}) + card(<*F.x*>"{y}) - card {} by A25
,A9,CARD_2:45
.= card Coim(A,y) by A6,FINSEQ_3:57;
end;
hence thesis by CLASSES1:def 10;
end;
hence thesis;
end;
theorem Th66:
for D be non empty set, d be Element of D, X be set,
F be PartFunc of D,REAL st
dom(F|X) is finite & d in dom(F|X) holds
FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent
proof
let D be non empty set, d be Element of D, X be set, F be PartFunc of D,REAL;
set dx = dom(F|X);
assume that
A1: dx is finite and
A2: d in dx;
set Y = X \ {d}, dy = dom(F|Y);
A3: dy=dom F /\ Y by RELAT_1:61;
A4: dx=dom F /\ X by RELAT_1:61;
A5: dy = dx \ {d}
proof
thus dy c= dx \ {d}
proof
let y be object;
assume
A6: y in dy;
then y in X \ {d} by A3,XBOOLE_0:def 4;
then
A7: not y in {d} by XBOOLE_0:def 5;
y in dom F by A3,A6,XBOOLE_0:def 4;
then y in dx by A3,A4,A6,XBOOLE_0:def 4;
hence thesis by A7,XBOOLE_0:def 5;
end;
let y be object;
assume
A8: y in dx \{d};
then
A9: not y in {d} by XBOOLE_0:def 5;
A10: y in dx by A8,XBOOLE_0:def 5;
then y in X by A4,XBOOLE_0:def 4;
then
A11: y in Y by A9,XBOOLE_0:def 5;
y in dom F by A4,A10,XBOOLE_0:def 4;
hence thesis by A3,A11,XBOOLE_0:def 4;
end;
F|dx = F|(dom F /\ X) by RELAT_1:61
.=(F|dom F)|X by RELAT_1:71
.=F|X by RELAT_1:68;
then FinS(F,dx\{d})^<*F.d*>, F|X are_fiberwise_equipotent by A1,A2,Th65;
hence thesis by A1,A5,Th63;
end;
theorem Th67:
for D be non empty set, F be PartFunc of D,REAL, X be set,
Y being finite set st Y = dom(F|X) holds len FinS(F,X) = card Y
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
let Y be finite set;
reconsider fs = dom FinS(F,X) as finite set;
A1: dom FinS(F,X) = Seg len FinS(F,X) by FINSEQ_1:def 3;
assume
A2: Y = dom(F|X);
FinS(F,X), F|X are_fiberwise_equipotent by A2,Def13;
hence card Y = card fs by A2,CLASSES1:81
.= len FinS(F,X) by A1,FINSEQ_1:57;
end;
theorem Th68:
for D be non empty set, F be PartFunc of D,REAL holds FinS(F,{}) = <*>REAL
proof
let D be non empty set, F be PartFunc of D,REAL;
dom(F|{}) = dom F /\ {} by RELAT_1:61
.= {};
then len FinS(F,{}) = 0 by Th67,CARD_1:27;
hence thesis;
end;
theorem Th69:
for D be non empty set, F be PartFunc of D,REAL, d be Element of
D st d in dom F holds FinS(F,{d}) = <* F.d *>
proof
let D be non empty set, F be PartFunc of D,REAL, d be Element of D;
assume d in dom F;
then {d} c= dom F by ZFMISC_1:31;
then
A1: {d} = dom F /\ {d} by XBOOLE_1:28
.= dom(F|{d}) by RELAT_1:61;
then FinS(F,{d}), F|{d} are_fiberwise_equipotent by Def13;
then
A2: rng FinS(F,{d}) = rng(F|{d}) by CLASSES1:75;
A3: rng(F|{d}) = {F.d}
proof
thus rng(F|{d}) c= {F.d}
proof
let x be object;
assume x in rng(F|{d});
then consider e be Element of D such that
A4: e in dom(F|{d}) and
A5: (F|{d}).e = x by PARTFUN1:3;
e=d by A1,A4,TARSKI:def 1;
then x=F.d by A4,A5,FUNCT_1:47;
hence thesis by TARSKI:def 1;
end;
let x be object;
A6: d in dom(F|{d}) by A1,TARSKI:def 1;
assume x in {F.d};
then x=F.d by TARSKI:def 1;
then x=(F|{d}).d by A6,FUNCT_1:47;
hence thesis by A6,FUNCT_1:def 3;
end;
len FinS(F,{d}) = card {d} by A1,Th67
.= 1 by CARD_1:30;
hence thesis by A2,A3,FINSEQ_1:39;
end;
theorem Th70:
for D be non empty set, F be PartFunc of D,REAL, X be set, d be
Element of D st dom(F|X) is finite & d in dom(F|X) & FinS(F,X).(len FinS(F,X))
= F.d holds FinS(F,X) = FinS(F,X\{d}) ^ <*F.d*>
proof
let D be non empty set, F be PartFunc of D,REAL, X be set, d be Element of D;
set dx = dom(F|X), fx = FinS(F,X), fy = FinS(F,X \{d});
assume that
A1: dx is finite and
A2: d in dx and
A3: fx.(len fx) = F.d;
A4: fx, F|X are_fiberwise_equipotent by A1,Def13;
then rng fx = rng(F|X) by CLASSES1:75;
then fx <> {} by A2,FUNCT_1:3,RELAT_1:38;
then 0+1<=len fx by NAT_1:13;
then max(0,len fx -1) = len fx - 1 by FINSEQ_2:4;
then reconsider n=len fx - 1 as Element of NAT by FINSEQ_2:5;
len fx = n+1;
then
A5: fx = fx|n ^ <*F.d*> by A3,RFINSEQ:7;
A6: fx|n is non-increasing by RFINSEQ:20;
fy ^ <*F.d*>, F|X are_fiberwise_equipotent by A1,A2,Th66;
then fx, fy^<*F.d*> are_fiberwise_equipotent by A4,CLASSES1:76;
then fy, fx|n are_fiberwise_equipotent by A5,RFINSEQ:1;
hence thesis by A5,A6,RFINSEQ:23;
end;
defpred P[Nat] means for D be non empty set, F be PartFunc of D,
REAL, X be set for Y be set, Z be finite set st Z = dom(F|Y) & dom(F|X) is
finite & Y c= X & $1 = card Z & (for d1,d2 be Element of D st d1 in dom(F|Y) &
d2 in dom(F|(X\Y)) holds F.d1>= F.d2) holds FinS(F,X) = FinS(F,Y) ^ FinS(F,X \
Y);
Lm3: P[ 0 ]
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
let Y be set;
let Z be finite set such that
A1: Z = dom(F|Y);
assume that
A2: dom(F|X) is finite and
Y c= X and
A3: 0 = card Z and
for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y)) holds F
.d1>=F.d2;
A4: dom(F|Y) = {} by A1,A3;
A5: dom(F|(X\Y))=dom F /\(X\Y) by RELAT_1:61;
dom(F|X) = dom F /\ X & dom(F|Y) = dom F /\ Y by RELAT_1:61;
then dom(F|(X\Y)) = dom(F|X) \ {} by A5,A4,XBOOLE_1:50
.= dom(F|X);
then
A6: FinS(F,X\Y) = FinS(F,dom(F|X)) by A2,Th63
.= FinS(F,X) by A2,Th63;
FinS(F,Y) = FinS(F,{}) by A4,Th63
.= {} by Th68;
hence thesis by A6,FINSEQ_1:34;
end;
Lm4: for n st P[n] holds P[n+1]
proof
let n;
assume
A1: P[n];
let D be non empty set, F be PartFunc of D,REAL, X be set;
let Y be set;
set dx = dom(F|X), dxy = dom(F|(X\Y)), fy = FinS(F,Y), fxy = FinS(F,X\Y);
let dy be finite set such that
A2: dy = dom(F|Y) and
A3: dom(F|X) is finite and
A4: Y c= X and
A5: n+1 = card dy and
A6: for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dxy holds F.d1>= F.d2;
A7: len fy = n+1 by A2,A5,Th67;
A8: F|Y, fy are_fiberwise_equipotent by A2,Def13;
then
A9: rng fy = rng(F|Y) by CLASSES1:75;
0+1<=n+1 by NAT_1:13;
then
A10: len fy in dom fy by A7,FINSEQ_3:25;
then fy.(len fy) in rng fy by FUNCT_1:def 3;
then consider d be Element of D such that
A11: d in dy and
A12: (F|Y).d = fy.(len fy) by A2,A9,PARTFUN1:3;
A13: dxy = dom F /\ (X\Y) by RELAT_1:61;
A14: dy = dom F /\ Y by A2,RELAT_1:61;
then
A15: d in Y by A11,XBOOLE_0:def 4;
then
A16: {d} c= X by A4,ZFMISC_1:31;
A17: d in dom F by A14,A11,XBOOLE_0:def 4;
then
A18: {d} c= dom F by ZFMISC_1:31;
A19: {d} c= Y by A15,ZFMISC_1:31;
A20: fxy ^ <*F.d*>, <*F.d*> ^ fxy are_fiberwise_equipotent by RFINSEQ:2;
set Yd = Y \ {d}, dyd = dom(F|Yd), xyd = dom(F|(X \ Yd));
A21: xyd = dom F /\ (X \ Yd) by RELAT_1:61;
A22: dyd = dom F /\ Yd by RELAT_1:61;
A23: dyd = dy \ {d}
proof
thus dyd c= dy \ {d}
proof
let y be object;
assume
A24: y in dyd;
then y in Y \ {d} by A22,XBOOLE_0:def 4;
then
A25: not y in {d} by XBOOLE_0:def 5;
y in dom F by A22,A24,XBOOLE_0:def 4;
then y in dy by A14,A22,A24,XBOOLE_0:def 4;
hence thesis by A25,XBOOLE_0:def 5;
end;
let y be object;
assume
A26: y in dy \{d};
then ( not y in {d})& y in Y by A14,XBOOLE_0:def 4,def 5;
then
A27: y in Yd by XBOOLE_0:def 5;
y in dom F by A14,A26,XBOOLE_0:def 4;
hence thesis by A22,A27,XBOOLE_0:def 4;
end;
A28: F.d = fy.(len fy) by A2,A11,A12,FUNCT_1:47;
then
A29: fy = fy|n ^ <*F.d*> by A7,RFINSEQ:7;
reconsider dyd as finite set by A23;
A30: X \ Yd = (X\Y) \/ X /\ {d} by XBOOLE_1:52
.= (X\Y) \/ {d} by A16,XBOOLE_1:28;
then
A31: xyd = dxy \/ dom F /\ {d} by A13,A21,XBOOLE_1:23
.= dxy \/ {d} by A18,XBOOLE_1:28;
A32: now
let d1,d2 be Element of D;
assume that
A33: d1 in dyd and
A34: d2 in xyd;
now
per cases by A31,A34,XBOOLE_0:def 3;
case
d2 in dxy;
hence F.d1>=F.d2 by A2,A6,A23,A33;
end;
case
d2 in {d};
then
A35: d2 = d by TARSKI:def 1;
(F|Y).d1 in rng(F|Y) by A2,A23,A33,FUNCT_1:def 3;
then F.d1 in rng(F|Y) by A2,A23,A33,FUNCT_1:47;
then consider m being Nat such that
A36: m in dom fy and
A37: fy.m = F.d1 by A9,FINSEQ_2:10;
A38: m<=len fy by A36,FINSEQ_3:25;
now
per cases;
case
m = len fy;
hence F.d1>=F.d2 by A2,A11,A12,A35,A37,FUNCT_1:47;
end;
case
m<> len fy;
then m<len fy by A38,XXREAL_0:1;
hence F.d1>=F.d2 by A10,A28,A35,A36,A37,RFINSEQ:19;
end;
end;
hence F.d1>=F.d2;
end;
end;
hence F.d1>=F.d2;
end;
dx = dom F /\ X by RELAT_1:61;
then
A39: dxy is finite by A3,A13,FINSET_1:1,XBOOLE_1:26;
then F|(X\Y) ,fxy are_fiberwise_equipotent by Def13;
then
A40: rng fxy = rng(F|(X\Y)) by CLASSES1:75;
A41: <*F.d*>^fxy is non-increasing
proof
set xfy = <*F.d*>^fxy;
let n;
assume that
A42: n in dom(<*F.d*>^fxy) and
A43: n+1 in dom(<*F.d*>^fxy);
A44: 1<=n by A42,FINSEQ_3:25;
then max(0,n-1)=n-1 by FINSEQ_2:4;
then reconsider n1=n-1 as Element of NAT by FINSEQ_2:5;
set r = xfy.n, s = xfy.(n+1);
A45: len <*F.d*> = 1 by FINSEQ_1:40;
then len xfy = 1 + len fxy by FINSEQ_1:22;
then
A46: len fxy = len xfy - 1;
A47: n+1<=len xfy by A43,FINSEQ_3:25;
then n1+1<=len fxy by A46,XREAL_1:19;
then
A48: n1+1 in dom fxy by A44,FINSEQ_3:25;
then fxy.(n1+1) in rng fxy by FUNCT_1:def 3;
then consider d1 be Element of D such that
A49: d1 in dxy & (F|(X\Y)).d1 = fxy.(n1+1) by A40,PARTFUN1:3;
1<n+1 by A44,NAT_1:13;
then
A50: xfy.(n+1) = fxy.(n+1-1) by A45,A47,FINSEQ_1:24
.= fxy.(n1+1);
A51: n<=len xfy by A42,FINSEQ_3:25;
then
A52: n1<=len fxy by A46,XREAL_1:9;
A53: F.d1 = fxy.(n1+1) & F.d>=F.d1 by A2,A6,A11,A49,FUNCT_1:47;
now
per cases;
suppose
n = 1;
hence r>=s by A50,A53,FINSEQ_1:41;
end;
suppose
n <> 1;
then
A54: 1<n by A44,XXREAL_0:1;
then 1+1<=n by NAT_1:13;
then 1<=n1 by XREAL_1:19;
then
A55: n1 in dom fxy by A52,FINSEQ_3:25;
xfy.n = fxy.n1 by A45,A51,A54,FINSEQ_1:24;
hence r>=s by A48,A50,A55,RFINSEQ:def 3;
end;
end;
hence r>=s;
end;
A56: <*F.d*>^fxy is FinSequence of REAL by RVSUM_1:145;
d in {d} by TARSKI:def 1;
then d in (X\Yd) by A30,XBOOLE_0:def 3;
then
A57: d in xyd by A21,A17,XBOOLE_0:def 4;
(X \ Yd) \ {d} = X \ (Yd \/ {d}) by XBOOLE_1:41
.= X \ (Y \/ {d}) by XBOOLE_1:39
.= X \ Y by A19,XBOOLE_1:12;
then fxy ^ <*F.d*>, F|(X\Yd) are_fiberwise_equipotent by A39,A31,A57,Th66;
then <*F.d*>^fxy, F|(X\Yd) are_fiberwise_equipotent by A20,CLASSES1:76;
then
A58: <*F.d*>^fxy = FinS(F,X\Yd) by A39,A31,A41,Def13,A56;
{d} c= dy by A11,ZFMISC_1:31;
then card dyd = card dy - card {d} by A23,CARD_2:44
.= n+1-1 by A5,CARD_1:30
.= n;
then FinS(F,X) = FinS(F,Yd) ^ FinS(F,X \ Yd) by A1,A3,A4,A32,XBOOLE_1:1;
then
A59: FinS(F,X) = FinS(F,Yd)^<*F.d*> ^ fxy by A58,FINSEQ_1:32;
A60: fy|n is non-increasing by RFINSEQ:20;
F|Y, FinS(F,Yd)^<*F.d*> are_fiberwise_equipotent by A2,A11,Th66;
then FinS(F,Yd)^<*F.d*>, fy are_fiberwise_equipotent by A8,CLASSES1:76;
then FinS(F,Yd), fy|n are_fiberwise_equipotent by A29,RFINSEQ:1;
hence thesis by A59,A29,A60,RFINSEQ:23;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|X
) is finite & Y c= X & (for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom
(F|(X\Y)) holds F.d1>=F.d2) holds FinS(F,X) = FinS(F,Y) ^ FinS(F,X \ Y)
proof
A1: for n holds P[n] from NAT_1:sch 2(Lm3,Lm4);
let D be non empty set, F be PartFunc of D,REAL, X be set;
let Y be set;
assume that
A2: dom(F|X) is finite and
A3: Y c= X and
A4: for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y))
holds F.d1>=F.d2;
F|Y c= F|X by A3,RELAT_1:75;
then reconsider dFY = dom(F|Y) as finite set by A2,FINSET_1:1,RELAT_1:11;
card dFY = card dFY;
hence thesis by A1,A2,A3,A4;
end;
theorem Th72:
for D be non empty set, F be PartFunc of D,REAL, r be Real, X be
set, d be Element of D st dom(F|X) is finite & d in dom(F|X) holds FinS(F-r,X).
(len FinS(F-r,X)) = (F-r).d iff FinS(F,X).(len FinS(F,X)) = F.d
proof
let D be non empty set, F be PartFunc of D,REAL, r be Real, X be set, d be
Element of D;
set dx = dom(F|X), drx = dom((F-r)|X), frx = FinS(F-r,X), fx = FinS(F,X);
assume that
A1: dx is finite and
A2: d in dx;
reconsider dx as finite set by A1;
A3: drx = dom(F-r) /\ X by RELAT_1:61
.= dom F /\ X by VALUED_1:3
.= dx by RELAT_1:61;
then fx, F|X are_fiberwise_equipotent by Def13;
then
A4: rng fx = rng(F|X) by CLASSES1:75;
then fx <> {} by A2,FUNCT_1:3,RELAT_1:38;
then 0+1<=len fx by NAT_1:13;
then
A5: len fx in dom fx by FINSEQ_3:25;
(F|X).d in rng(F|X) by A2,FUNCT_1:def 3;
then F.d in rng(F|X) by A2,FUNCT_1:47;
then consider n being Nat such that
A6: n in dom fx and
A7: fx.n = F.d by A4,FINSEQ_2:10;
A8: dom fx = Seg len fx by FINSEQ_1:def 3;
frx, (F-r)|X are_fiberwise_equipotent by A3,Def13;
then
A9: rng frx = rng((F-r)|X) by CLASSES1:75;
A10: len fx = card dx & dom frx = Seg len frx by Th67,FINSEQ_1:def 3;
A11: len frx = card dx by A3,Th67;
then frx.(len frx) in rng frx by A10,A8,A5,FUNCT_1:def 3;
then consider d1 be Element of D such that
A12: d1 in drx and
A13: ((F-r)|X).d1 = frx.(len frx) by A9,PARTFUN1:3;
(F|X).d1 = F.d1 by A3,A12,FUNCT_1:47;
then F.d1 in rng(F|X) by A3,A12,FUNCT_1:def 3;
then consider m being Nat such that
A14: m in dom fx and
A15: fx.m = F.d1 by A4,FINSEQ_2:10;
A16: dom(F-r) = dom F by VALUED_1:3;
A17: drx = dom(F-r) /\ X by RELAT_1:61;
then
A18: d1 in dom(F-r) by A12,XBOOLE_0:def 4;
A19: frx.(len frx) = (F-r).d1 by A12,A13,FUNCT_1:47
.= F.d1 - r by A16,A18,VALUED_1:3;
A20: d in dom(F-r) by A2,A3,A17,XBOOLE_0:def 4;
then
A21: (F-r).d = F.d - r by A16,VALUED_1:3;
A22: n<=len fx by A6,FINSEQ_3:25;
thus frx.(len frx) = (F-r).d implies fx.(len fx) = F.d
proof
fx.(len fx) in rng fx by A5,FUNCT_1:def 3;
then consider d1 be Element of D such that
A23: d1 in dx and
A24: (F|X).d1 = fx.(len fx) by A4,PARTFUN1:3;
A25: d1 in dom(F-r) by A3,A17,A23,XBOOLE_0:def 4;
A26: F.d1 = fx.(len fx) by A23,A24,FUNCT_1:47;
((F-r)|X).d1 = (F-r).d1 by A3,A23,FUNCT_1:47
.= F.d1 - r by A16,A25,VALUED_1:3;
then F.d1-r in rng((F-r)|X) by A3,A23,FUNCT_1:def 3;
then consider m being Nat such that
A27: m in dom frx and
A28: frx.m = F.d1-r by A9,FINSEQ_2:10;
A29: m<=len frx by A27,FINSEQ_3:25;
assume that
A30: frx.(len frx) = (F-r).d and
A31: fx.(len fx) <> F.d;
n<len fx by A7,A22,A31,XXREAL_0:1;
then
A32: F.d>=F.d1 by A5,A6,A7,A26,RFINSEQ:19;
now
per cases;
case
len frx = m;
then F.d1+-r=F.d-r by A16,A20,A30,A28,VALUED_1:3;
hence contradiction by A31,A23,A24,FUNCT_1:47;
end;
case
len frx <>m;
then m<len frx by A29,XXREAL_0:1;
then F.d1-r>=F.d-r by A11,A10,A8,A21,A5,A30,A27,A28,RFINSEQ:19;
then F.d1>=F.d by XREAL_1:9;
hence contradiction by A31,A26,A32,XXREAL_0:1;
end;
end;
hence contradiction;
end;
assume that
A33: fx.(len fx) = F.d and
A34: frx.(len frx) <> (F-r).d;
((F-r)|X).d in rng((F-r)|X) by A2,A3,FUNCT_1:def 3;
then (F-r).d in rng((F-r)|X) by A2,A3,FUNCT_1:47;
then consider n1 be Nat such that
A35: n1 in dom frx and
A36: frx.n1 = F.d -r by A9,A21,FINSEQ_2:10;
n1<=len frx by A35,FINSEQ_3:25;
then n1<len frx by A21,A34,A36,XXREAL_0:1;
then F.d-r>=F.d1-r by A11,A10,A8,A5,A19,A35,A36,RFINSEQ:19;
then
A37: F.d>=F.d1 by XREAL_1:9;
A38: m<=len fx by A14,FINSEQ_3:25;
now
per cases;
case
len fx = m;
hence contradiction by A16,A20,A33,A34,A19,A15,VALUED_1:3;
end;
case
len fx <> m;
then m<len fx by A38,XXREAL_0:1;
then F.d1>=F.d by A5,A33,A14,A15,RFINSEQ:19;
hence contradiction by A21,A34,A19,A37,XXREAL_0:1;
end;
end;
hence contradiction;
end;
theorem Th73:
for D be non empty set, F be PartFunc of D,REAL, r be Real, X be
set, Z being finite set st Z = dom(F|X) holds FinS(F-r, X) = FinS(F,X) - (card
Z |->r)
proof
let D be non empty set, F be PartFunc of D,REAL, r be Real;
let X be set;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
defpred P[Nat] means for X be set, G being finite set st G = dom(
F|X) & $1= card(G) holds FinS(F-r, X) = FinS(F,X) - (card(G)|->r);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let X be set, G be finite set;
assume
A3: G = dom(F|X);
set frx = FinS(F-rr,X), fx = FinS(F,X);
A4: dom((F-r)|X) = dom(F-r) /\ X by RELAT_1:61
.=dom F /\ X by VALUED_1:3
.=dom(F|X) by RELAT_1:61;
then
A5: len frx = card G by A3,Th67;
A6: FinS(F-r,X), (F-r)|X are_fiberwise_equipotent by A3,A4,Def13;
then
A7: rng FinS(F-r,X) = rng((F-r)|X) by CLASSES1:75;
assume
A8: n+1= card(G);
then
A9: len fx = n+1 by A3,Th67;
0+1<=n+1 by NAT_1:13;
then len frx in dom frx by A8,A5,FINSEQ_3:25;
then frx.(len frx) in rng frx by FUNCT_1:def 3;
then consider d be Element of D such that
A10: d in dom((F-r)|X) and
A11: ((F-r)|X).d = frx.(len frx) by A7,PARTFUN1:3;
set Y = X \ {d}, dx = dom(F|X), dy = dom(F|Y), fry = FinS(F-r,Y), fy =
FinS(F,Y), n1r = (n+1) |-> rr, nr = n |-> rr;
A12: {d} c= dx by A4,A10,ZFMISC_1:31;
(F-r).d = frx.(len frx) by A10,A11,FUNCT_1:47;
then
A13: fx.(len fx) = F.d by A3,A4,A10,Th72;
len fx = card G by A3,Th67;
then
A14: fx = fx|n ^ <*F.d*> by A8,A13,RFINSEQ:7;
fx = fy ^ <*F.d*> by A3,A4,A10,A13,Th70;
then
A15: fy = fx|n by A14,FINSEQ_1:33;
A16: dom(fy - nr)=Seg len(fy - nr) by FINSEQ_1:def 3;
A17: dy=dom F /\ Y by RELAT_1:61;
A18: dx=dom F /\ X by RELAT_1:61;
A19: dy = dx \ {d}
proof
thus dy c= dx \ {d}
proof
let y be object;
assume
A20: y in dy;
then y in X \ {d} by A17,XBOOLE_0:def 4;
then
A21: not y in {d} by XBOOLE_0:def 5;
y in dom F by A17,A20,XBOOLE_0:def 4;
then y in dx by A17,A18,A20,XBOOLE_0:def 4;
hence thesis by A21,XBOOLE_0:def 5;
end;
let y be object;
assume
A22: y in dx \{d};
then
A23: not y in {d} by XBOOLE_0:def 5;
A24: y in dx by A22,XBOOLE_0:def 5;
then y in X by A18,XBOOLE_0:def 4;
then
A25: y in Y by A23,XBOOLE_0:def 5;
y in dom F by A18,A24,XBOOLE_0:def 4;
hence thesis by A17,A25,XBOOLE_0:def 4;
end;
then reconsider dx,dy as finite set by A3;
A26: card dy = card dx - card {d} by A12,A19,CARD_2:44
.= n+1-1 by A3,A8,CARD_1:30
.= n;
then len nr = n & len fy = n by Th67,CARD_1:def 7;
then
A27: len (fy - nr) = n by FINSEQ_2:72;
(F-r).d = frx.(len frx) by A10,A11,FUNCT_1:47;
then
A28: frx = frx|n ^ <*(F-r).d*> by A8,A5,RFINSEQ:7;
fry^<*(F-r).d*>, (F-r)|X are_fiberwise_equipotent by A3,A4,A10,Th66;
then fry^<*(F-r).d*>, frx are_fiberwise_equipotent by A6,CLASSES1:76;
then
frx|n is non-increasing & fry, frx|n are_fiberwise_equipotent by A28,
RFINSEQ:1,20;
then
A29: fry = frx|n by RFINSEQ:23;
len n1r = n+1 by CARD_1:def 7;
then
A30: len (fx - n1r) = n+1 by A9,FINSEQ_2:72;
then
A31: dom (fx - n1r) = Seg(n+1) by FINSEQ_1:def 3;
dom((F-r)|X) = dom(F-r) /\ X by RELAT_1:61;
then d in dom(F-r) by A10,XBOOLE_0:def 4;
then d in dom F by VALUED_1:3;
then (F-r).d = F.d - r by VALUED_1:3;
then
A32: <*(F-r).d*> = <*F.d*> - <*r*> by RVSUM_1:29;
A33: n<n+1 by NAT_1:13;
A34: dom fx = Seg len fx by FINSEQ_1:def 3;
reconsider Fd = <*F.d*>, rr = <*r*> as FinSequence of REAL by RVSUM_1:145;
len <*F.d*> =1 & len <*r*> = 1 by FINSEQ_1:40;
then
A35: len (Fd - rr) = 1 by FINSEQ_2:72;
then
A36: len ((fy - nr)^(<*F.d*> - <*r*>)) = n+1 by A27,FINSEQ_1:22;
1 in Seg 1 by FINSEQ_1:1;
then
A37: 1 in dom(<*F.d*> - <*r*>) by A35,FINSEQ_1:def 3;
A38: <*F.d*>.1=F.d & <*r*>.1=r;
A39: now
let m be Nat;
assume
A40: m in dom (fx - n1r);
per cases;
suppose
A41: m=n+1;
then
A42: n1r.m = r by FINSEQ_1:4,FUNCOP_1:7;
((fy - nr)^(<*F.d*> - <*r*>)).m = (<*F.d*> - <*r*>).(n+1-n) by A27,A36
,A33,A41,FINSEQ_1:24
.= F.d - r by A38,A37,VALUED_1:13;
hence
(fx - n1r).m = ((fy - nr)^(<*F.d*> - <*r*>)).m by A13,A9,A40,A41,A42,
VALUED_1:13;
end;
suppose
A43: m<>n+1;
m<=n+1 by A31,A40,FINSEQ_1:1;
then m<n+1 by A43,XXREAL_0:1;
then
A44: m<=n by NAT_1:13;
reconsider s=fx.m as Element of REAL by XREAL_0:def 1;
A45: n<=n+1 by NAT_1:11;
A46: n1r.m=r by A31,A40,FUNCOP_1:7;
A47: 1<=m by A31,A40,FINSEQ_1:1;
then
A48: m in Seg n by A44,FINSEQ_1:1;
then
A49: m in dom(fy - nr) by A27,FINSEQ_1:def 3;
1<=n by A47,A44,XXREAL_0:2;
then n in Seg(n+1) by A45,FINSEQ_1:1;
then
A50: (fx|n).m = fx.m by A9,A34,A48,RFINSEQ:6;
((fy - nr)^(<*F.d*> - <*r*>)).m = (fy - nr).m & nr.m = r by A27,A16,A48
,FINSEQ_1:def 7,FUNCOP_1:7;
hence ((fy - nr)^(<*F.d*> - <*r*>)).m = s-r by A15,A50,A49,VALUED_1:13
.=(fx - n1r).m by A40,A46,VALUED_1:13;
end;
end;
fry = fy - nr by A2,A26;
hence thesis by A8,A28,A29,A32,A30,A36,A39,FINSEQ_2:9;
end;
A51: P[ 0 ]
proof
let X be set, G be finite set;
assume
A52: G = dom(F|X);
assume 0=card(G);
then
A53: dom(F|X) = {} by A52;
then FinS(F,X) = FinS(F,{}) by Th63
.= <*>REAL by Th68;
then
A54: FinS(F,X) - (card(G)|->rr) = <*>REAL by FINSEQ_2:73;
dom((F-r)|X) = dom(F-r) /\ X by RELAT_1:61
.=dom F /\ X by VALUED_1:3
.=dom(F|X) by RELAT_1:61;
hence FinS(F-r,X) = FinS(F-r,{}) by A53,Th63
.= FinS(F,X) - (card(G)|->r) by A54,Th68;
end;
A55: for n holds P[n] from NAT_1:sch 2(A51,A1);
let G be finite set;
assume G = dom(F|X);
hence thesis by A55;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X be set st dom(F|X)
is finite & (for d be Element of D st d in dom(F|X) holds F.d>=0) holds FinS(
max+ F, X) = FinS(F, X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set;
assume that
A1: dom(F|X) is finite and
A2: for d be Element of D st d in dom(F|X) holds F.d>=0;
now
let d be Element of D;
assume
A3: d in dom(F|X);
then F.d>=0 by A2;
hence (F|X).d>=0 by A3,FUNCT_1:47;
end;
then
A4: (F|X) = max+ (F|X) by Th46
.= (max+ F)|X by Th44;
hence FinS(F,X) = FinS((max+ F)|X,X) by A1,Th64
.= FinS(max+ F,X) by A1,A4,Th64;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
Z be finite set st Z = dom(F|X) & rng(F|X) = {r} holds FinS(F, X) = card(Z) |->
r
proof
let D be non empty set, F be PartFunc of D,REAL, X be set, r be Real;
let dx be finite set such that
A1: dx = dom(F|X);
set fx = FinS(F,X);
assume
A2: rng(F|X) = {r};
F|X, fx are_fiberwise_equipotent by A1,Def13;
then
A3: rng fx = {r} by A2,CLASSES1:75;
A4: dom fx = Seg len fx by FINSEQ_1:def 3;
len fx = card dx by A1,Th67;
hence thesis by A3,A4,FUNCOP_1:9;
end;
theorem Th76:
for D be non empty set, F be PartFunc of D,REAL, X,Y be set st
dom(F|(X \/ Y)) is finite & X misses Y holds FinS(F,X \/ Y), FinS(F,X) ^ FinS(F
,Y) are_fiberwise_equipotent
proof
let D be non empty set, F be PartFunc of D,REAL, X,Y be set;
assume
A1: dom(F|(X \/ Y)) is finite;
F|Y c= F|(X \/ Y) by RELAT_1:75,XBOOLE_1:7;
then reconsider dfy = dom(F|Y) as finite set by A1,FINSET_1:1,RELAT_1:11;
defpred P[Nat] means for Y be set, Z being finite set st Z = dom(
F|Y) & dom(F|(X \/ Y)) is finite & X /\ Y = {} & $1 = card Z holds FinS(F,X \/
Y), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent;
A2: card dfy = card dfy;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let Y be set, Z be finite set;
assume that
A5: Z = dom(F|Y) and
A6: dom(F|(X \/ Y)) is finite and
A7: X /\ Y = {} and
A8: n+1 = card Z;
set x = the Element of dom(F|Y);
reconsider x as Element of D by A5,A8,CARD_1:27,TARSKI:def 3;
set y1 = Y\{x};
A9: dom(F|Y)= dom F /\ Y by RELAT_1:61;
now
assume
A10: x in X;
x in Y by A5,A8,A9,CARD_1:27,XBOOLE_0:def 4;
hence contradiction by A7,A10,XBOOLE_0:def 4;
end;
then X \ {x} = X by ZFMISC_1:57;
then
A11: (X \/ Y) \ {x} = X \/ y1 by XBOOLE_1:42;
A12: dom(F|y1) = dom F /\ y1 by RELAT_1:61;
A13: dom(F|y1) = dom(F|Y) \ {x}
proof
thus dom(F|y1) c= dom(F|Y) \ {x}
proof
let y be object;
assume
A14: y in dom(F|y1);
then y in Y \ {x} by A12,XBOOLE_0:def 4;
then
A15: not y in {x} by XBOOLE_0:def 5;
y in dom F by A12,A14,XBOOLE_0:def 4;
then y in dom(F|Y) by A12,A9,A14,XBOOLE_0:def 4;
hence thesis by A15,XBOOLE_0:def 5;
end;
let y be object;
assume
A16: y in dom(F|Y) \{x};
then
A17: not y in {x} by XBOOLE_0:def 5;
A18: y in dom(F|Y) by A16,XBOOLE_0:def 5;
then y in Y by A9,XBOOLE_0:def 4;
then
A19: y in y1 by A17,XBOOLE_0:def 5;
y in dom F by A9,A18,XBOOLE_0:def 4;
hence thesis by A12,A19,XBOOLE_0:def 4;
end;
then reconsider dFy = dom(F|y1) as finite set by A5;
{x} c= dom(F|Y) by A5,A8,CARD_1:27,ZFMISC_1:31;
then
A20: card dFy = n+1 - card {x} by A5,A8,A13,CARD_2:44
.= n+1-1 by CARD_1:30
.= n;
X \/ y1 c= X \/ Y by XBOOLE_1:13;
then dom F /\(X \/ y1) c= dom F /\ (X \/ Y) by XBOOLE_1:27;
then dom(F|(X \/ y1)) c= dom F /\ (X \/ Y) by RELAT_1:61;
then
A21: dom(F|(X \/ y1)) c= dom(F|(X \/ Y)) by RELAT_1:61;
A22: FinS(F,X \/ Y), F|(X \/ Y) are_fiberwise_equipotent by A6,Def13;
dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by RELAT_1:61
.= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23
.= dom(F|X) \/ dom F /\ Y by RELAT_1:61
.= dom(F|X) \/ dom(F|Y) by RELAT_1:61;
then x in dom(F|(X \/ Y)) by A5,A8,CARD_1:27,XBOOLE_0:def 3;
then FinS(F,X \/ y1)^<*F.x*>, F|(X \/ Y) are_fiberwise_equipotent by A6,A11
,Th66;
then
A23: FinS(F,X \/ y1)^<*F.x*>, FinS(F,X \/ Y) are_fiberwise_equipotent by A22,
CLASSES1:76;
X /\ y1 c= X /\ Y by XBOOLE_1:27;
then FinS(F,X \/ y1), FinS(F,X) ^ FinS(F,y1) are_fiberwise_equipotent by A4
,A6,A7,A21,A20,XBOOLE_1:3;
then FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ FinS(F,y1) ^ <*F.x*>
are_fiberwise_equipotent by RFINSEQ:1;
then
A24: FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ (FinS(F,y1) ^ <*F.x*>)
are_fiberwise_equipotent by FINSEQ_1:32;
FinS(F,y1)^<*F.x*>, F|Y are_fiberwise_equipotent & FinS(F,Y), F|Y
are_fiberwise_equipotent by A5,A8,Def13,Th66,CARD_1:27;
then FinS(F,y1)^<*F.x*>,FinS(F,Y) are_fiberwise_equipotent by CLASSES1:76;
then
A25: FinS(F,y1)^<*F.x*> ^ FinS(F,X), FinS(F,Y) ^ FinS(F,X)
are_fiberwise_equipotent by RFINSEQ:1;
FinS(F,X)^(FinS(F,y1)^<*F.x*>),FinS(F,y1)^<*F.x*> ^ FinS(F,X)
are_fiberwise_equipotent by RFINSEQ:2;
then
FinS(F,Y) ^ FinS(F,X), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent
& FinS (F,X)^(FinS(F,y1)^<*F.x*>), FinS(F,Y)^FinS(F,X) are_fiberwise_equipotent
by A25,CLASSES1:76,RFINSEQ:2;
then FinS(F,X)^(FinS(F,y1)^<*F.x*>), FinS(F,X)^FinS(F,Y)
are_fiberwise_equipotent by CLASSES1:76;
then FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ FinS(F,Y)
are_fiberwise_equipotent by A24,CLASSES1:76;
hence thesis by A23,CLASSES1:76;
end;
A26: P[ 0 ]
proof
let Y be set, Z be finite set;
assume that
A27: Z = dom(F|Y) and
A28: dom(F|(X \/ Y)) is finite and
X /\ Y = {} and
A29: 0 = card Z;
A30: dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by RELAT_1:61
.= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23
.= dom(F|X) \/ dom F /\ Y by RELAT_1:61
.= dom(F|X) \/ dom(F|Y) by RELAT_1:61;
then
A31: dom(F|X) is finite by A28,FINSET_1:1,XBOOLE_1:7;
A32: dom(F|Y) = {} by A27,A29;
then FinS(F,X \/ Y) = FinS(F,dom(F|X)) by A28,A30,Th63
.= FinS(F,X) by A31,Th63
.= FinS(F,X)^<*>REAL by FINSEQ_1:34
.= FinS(F,X)^FinS(F,dom(F|Y)) by A32,Th68
.= FinS(F,X)^ FinS(F,Y) by A27,Th63;
hence thesis;
end;
A33: for n holds P[n] from NAT_1:sch 2(A26,A3);
assume X /\ Y = {};
hence thesis by A1,A33,A2;
end;
definition
let D be non empty set, F be PartFunc of D,REAL, X be set;
func Sum(F,X) -> Real equals
Sum FinS(F,X);
correctness;
end;
theorem Th77:
for D be non empty set, F be PartFunc of D,REAL, X be set, r
st dom(F|X) is finite holds Sum(r(#)F,X) = r * Sum(F,X)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set, r;
set x = dom(F|X);
reconsider rr = r as Real;
assume
A1: dom(F|X) is finite;
then reconsider FX = F|X as finite Function by FINSET_1:10;
dom((r(#)F)|X) = dom(r(#)(F|X)) by RFUNCT_1:49
.= dom(F|X) by VALUED_1:def 5;
then reconsider rFX = (r(#)F)|X as finite Function by A1,FINSET_1:10;
consider b be FinSequence such that
A2: F|x, b are_fiberwise_equipotent by A1,RFINSEQ:5;
rng(F|x) = rng b by A2,CLASSES1:75;
then reconsider b as FinSequence of REAL by FINSEQ_1:def 4;
x = dom F /\ X by RELAT_1:61;
then
A3: F|x = (F|dom F)|X by RELAT_1:71
.=F|X by RELAT_1:68;
then
A4: rng b = rng(F|X) by A2,CLASSES1:75;
A5: now
let x be Element of REAL;
A6: len(r*b) = len b by FINSEQ_2:33;
now
per cases;
case
A7: not x in rng(r*b);
A8: now
assume x in rng((r(#)F)|X);
then x in rng(r(#)(F|X)) by RFUNCT_1:49;
then consider d be Element of D such that
A9: d in dom(r(#)(F|X)) and
A10: (r(#)(F|X)).d = x by PARTFUN1:3;
d in dom(F|X) by A9,VALUED_1:def 5;
then (F|X).d in rng(F|X) by FUNCT_1:def 3;
then consider n be Nat such that
A11: n in dom b and
A12: b.n=(F|X).d by A4,FINSEQ_2:10;
x=r*(F|X).d by A9,A10,VALUED_1:def 5;
then
A13: x=(r*b).n by A12,RVSUM_1:44;
n in dom (r*b) by A6,A11,FINSEQ_3:29;
hence contradiction by A7,A13,FUNCT_1:def 3;
end;
(r*b)"{x} = {} by A7,Lm2;
hence card((r*b)"{x}) = card(rFX"{x}) by A8,Lm2;
end;
case
x in rng(r*b);
then consider n be Nat such that
n in dom(r*b) and
A14: (r*b).n = x by FINSEQ_2:10;
reconsider p=b.n as Real;
A15: x = r*p by A14,RVSUM_1:44;
now
per cases;
case
A16: r=0;
then
A17: (r*b)"{x} = dom b by A15,RFINSEQ:25;
dom(FX) =(r(#)(F|X))"{x} by A15,A16,Th7
.=((r(#)F)|X)"{x} by RFUNCT_1:49;
hence card((r*b)"{x}) = card(rFX"{x}) by A2,A3,A17,CLASSES1:81;
end;
case
A18: r<>0;
then
A19: Coim(rr*b,x) = Coim(b,x/rr) by RFINSEQ:24;
Coim((r(#)F)|X,x) = (r(#)(F|X))"{x} by RFUNCT_1:49
.= Coim(FX,x/r) by A18,Th6;
hence card Coim(r*b,x) = card Coim(rFX,x) by A2,A3,A19,
CLASSES1:def 10;
end;
end;
hence card((r*b)"{x}) = card(rFX"{x});
end;
end;
hence card Coim(r*b,x) = card Coim(rFX,x);
end;
rng(r*b) c=REAL & rng((r(#)F)|X) c= REAL;
then
A20: r*b, (r(#)F)|X are_fiberwise_equipotent by A5,CLASSES1:79;
F|X, FinS(F,X) are_fiberwise_equipotent by A1,Def13;
then
A21: Sum b = Sum(F,X) by A2,A3,CLASSES1:76,RFINSEQ:9;
dom((r(#)F)|X) = dom(r(#)F) /\ X by RELAT_1:61
.= dom F /\ X by VALUED_1:def 5
.= dom(F|X) by RELAT_1:61;
then (r(#)F)|X, FinS(r(#)F,X) are_fiberwise_equipotent by A1,Def13;
hence Sum(r(#)F,X) = Sum(r*b) by A20,CLASSES1:76,RFINSEQ:9
.= r* Sum(F,X) by A21,RVSUM_1:87;
end;
theorem Th78:
for D be non empty set, F,G be PartFunc of D,REAL, X be set, Y
being finite set st Y = dom(F|X) & dom(F|X) = dom(G|X) holds Sum(F+G,X) = Sum(F
,X) + Sum(G,X)
proof
let D be non empty set;
let F,G be PartFunc of D,REAL, X be set, Y be finite set such that
A1: Y = dom(F|X);
defpred P[Nat] means for F,G be PartFunc of D,REAL, X be set, Y
being finite set st card(Y) = $1 & Y = dom(F|X) & dom(F|X) = dom(G|X) holds Sum
(F+G,X) = Sum(F,X) + Sum(G,X);
A2: card(Y)=card(Y);
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let F,G be PartFunc of D,REAL, X be set, dx be finite set;
set gx = dom(G|X);
assume that
A5: card(dx) = n+1 and
A6: dx = dom(F|X) and
A7: dom(F|X) = dom(G|X);
set x = the Element of dx;
reconsider x as Element of D by A5,A6,CARD_1:27,TARSKI:def 3;
A8: dx=dom F /\ X by A6,RELAT_1:61;
then
A9: x in dom F by A5,CARD_1:27,XBOOLE_0:def 4;
set Y = X\{x}, dy = dom(F|Y), gy = dom(G|Y);
A10: gx=dom G /\ X by RELAT_1:61;
then x in dom G by A5,A6,A7,CARD_1:27,XBOOLE_0:def 4;
then x in dom F /\ dom G by A9,XBOOLE_0:def 4;
then
A11: x in dom(F+G) by VALUED_1:def 1;
A12: dy=dom F /\ Y by RELAT_1:61;
A13: dy = dx \ {x}
proof
thus dy c= dx \ {x}
proof
let y be object;
assume
A14: y in dy;
then y in X \ {x} by A12,XBOOLE_0:def 4;
then
A15: not y in {x} by XBOOLE_0:def 5;
y in dom F by A12,A14,XBOOLE_0:def 4;
then y in dx by A12,A8,A14,XBOOLE_0:def 4;
hence thesis by A15,XBOOLE_0:def 5;
end;
let y be object;
assume
A16: y in dx \{x};
then ( not y in {x})& y in X by A8,XBOOLE_0:def 4,def 5;
then
A17: y in Y by XBOOLE_0:def 5;
y in dom F by A8,A16,XBOOLE_0:def 4;
hence thesis by A12,A17,XBOOLE_0:def 4;
end;
then reconsider dy as finite set;
A18: gy= dom G /\ Y by RELAT_1:61;
A19: dy = gy
proof
thus dy c= gy
proof
let y be object;
assume
A20: y in dy;
then y in dom F by A12,XBOOLE_0:def 4;
then y in gx by A6,A7,A12,A8,A20,XBOOLE_0:def 4;
then
A21: y in dom G by A10,XBOOLE_0:def 4;
y in Y by A12,A20,XBOOLE_0:def 4;
hence thesis by A18,A21,XBOOLE_0:def 4;
end;
let y be object;
assume
A22: y in gy;
then y in dom G by A18,XBOOLE_0:def 4;
then y in dx by A6,A7,A18,A10,A22,XBOOLE_0:def 4;
then
A23: y in dom F by A8,XBOOLE_0:def 4;
y in Y by A18,A22,XBOOLE_0:def 4;
hence thesis by A12,A23,XBOOLE_0:def 4;
end;
{x} c= dx by A5,CARD_1:27,ZFMISC_1:31;
then card(dy) = card(dx) - card {x} by A13,CARD_2:44
.=n+1-1 by A5,CARD_1:30
.= n;
then
A24: Sum(F+G,Y) = Sum(F,Y) + Sum(G,Y) by A4,A19;
A25: dom((F+G)|X) = dom(F|X + G|X) by RFUNCT_1:44
.= dx /\ gx by A6,VALUED_1:def 1;
then
A26: FinS(F+G,X), (F+G)|X are_fiberwise_equipotent by Def13;
x in X by A5,A8,CARD_1:27,XBOOLE_0:def 4;
then x in dom(F+G) /\ X by A11,XBOOLE_0:def 4;
then x in dom ((F+G)|X) by RELAT_1:61;
then
A27: FinS(F+G,Y)^<*(F+G).x*>, (F+G)|X are_fiberwise_equipotent by A25,Th66;
reconsider Fx = <*F.x*>, Gx = <*G.x*>, FGx = <*(F+G).x*>
as FinSequence of REAL by RVSUM_1:145;
FinS(F,Y)^<*F.x*>, F|X are_fiberwise_equipotent & FinS(F,X), F|X
are_fiberwise_equipotent by A5,A6,Def13,Th66,CARD_1:27;
then
A28: Sum(F,X) = Sum (FinS(F,Y) ^ Fx) by CLASSES1:76,RFINSEQ:9
.= Sum(F,Y) + F.x by RVSUM_1:74;
FinS(G,Y)^<*G.x*>, G|X are_fiberwise_equipotent & FinS(G,X), G|X
are_fiberwise_equipotent by A5,A6,A7,Def13,Th66,CARD_1:27;
then Sum(G,X) = Sum (FinS(G,Y)^Gx) by CLASSES1:76,RFINSEQ:9
.= Sum(G,Y) + G.x by RVSUM_1:74;
hence Sum(F,X)+ Sum(G,X) = Sum FinS(F+G,Y) + (F.x + G.x) by A24,A28
.= Sum FinS(F+G,Y) + (F+G).x by A11,VALUED_1:def 1
.= Sum(FinS(F+G,Y)^FGx) by RVSUM_1:74
.= Sum(F+G,X) by A27,A26,CLASSES1:76,RFINSEQ:9;
end;
A29: P[ 0 ]
proof
let F,G be PartFunc of D,REAL, X be set, Y be finite set;
assume that
A30: card(Y) = 0 and
A31: Y = dom(F|X) and
A32: dom(F|X) = dom(G|X);
dom(F|X) = {} by A30,A31;
then
A33: rng(F|X) = {} by RELAT_1:42;
(F+G)|X = F|X + G|X by RFUNCT_1:44;
then dom((F+G)|X) = dom(F|X) /\ dom(G|X) by VALUED_1:def 1
.= {} by A30,A31,A32;
then
rng ((F+G)|X) = {} & FinS(F+G,X), (F+G)|X are_fiberwise_equipotent by Def13
,RELAT_1:42;
then
A34: rng FinS(F+G,X) = {} by CLASSES1:75;
FinS(F,X), F|X are_fiberwise_equipotent by A31,Def13;
then rng FinS(F,X) = {} by A33,CLASSES1:75;
then
A35: Sum(F,X) = 0 by RELAT_1:41,RVSUM_1:72;
dom(G|X) = {} by A30,A31,A32;
then
A36: rng(G|X) = {} by RELAT_1:42;
FinS(G,X), G|X are_fiberwise_equipotent by A31,A32,Def13;
then rng FinS(G,X) = {} by A36,CLASSES1:75;
then Sum(F,X) + Sum(G,X) = 0+0 by A35,RELAT_1:41,RVSUM_1:72;
hence thesis by A34,RELAT_1:41,RVSUM_1:72;
end;
A37: for n holds P[n] from NAT_1:sch 2(A29,A3);
assume dom(F|X) = dom(G|X);
hence thesis by A1,A37,A2;
end;
theorem
for D be non empty set, F,G be PartFunc of D,REAL, X be set st dom(F|X
) is finite & dom(F|X) = dom(G|X) holds Sum(F-G,X) = Sum(F,X) - Sum (G,X)
proof
let D be non empty set, F,G be PartFunc of D,REAL, X be set;
assume
A1: dom(F|X) is finite & dom(F|X) = dom(G|X);
dom(((-1)(#)G)|X) = dom((-1)(#)G) /\ X by RELAT_1:61
.= dom G /\ X by VALUED_1:def 5
.= dom(G|X) by RELAT_1:61;
hence Sum(F-G,X) = Sum(F,X) + Sum((-1)(#)G,X) by A1,Th78
.= Sum(F,X) +(-1)* Sum(G,X) by A1,Th77
.= Sum(F,X) - Sum(G,X);
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
Y being finite set st Y = dom(F|X) holds Sum(F-r,X) = Sum(F,X) - r*card(Y)
proof
let D be non empty set, F be PartFunc of D,REAL, X be set, r be Real;
set fx = FinS(F,X);
let Y be finite set;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
set dr = card(Y) |-> rr;
assume
A1: Y = dom(F|X);
then len fx = card(Y) by Th67;
then reconsider xf = fx, rd = dr as Element of (card(Y))-tuples_on REAL by
FINSEQ_2:92;
FinS(F-r,X) = fx - dr by A1,Th73;
hence Sum(F-r,X) = Sum xf - Sum rd by RVSUM_1:90
.= Sum(F,X) - r*card(Y) by RVSUM_1:80;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL holds Sum(F,{}) = 0 by Th68,
RVSUM_1:72;
theorem
for D be non empty set, F be PartFunc of D,REAL, d be Element of D st
d in dom F holds Sum(F,{d}) = F.d
proof
let D be non empty set, F be PartFunc of D,REAL, d be Element of D;
reconsider Fd = F.d as Element of REAL by XREAL_0:def 1;
assume
d in dom F;
hence Sum(F,{d}) = Sum <*Fd*> by Th69
.= F.d by FINSOP_1:11;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(
X \/ Y)) is finite & X misses Y holds Sum(F, X \/ Y) = Sum(F,X) + Sum (F,Y)
proof
let D be non empty set, F be PartFunc of D,REAL, X,Y be set;
assume dom(F|(X \/ Y)) is finite & X misses Y;
hence Sum(F, X \/ Y) = Sum (FinS(F,X) ^ FinS(F,Y)) by Th76,RFINSEQ:9
.= Sum(F,X) + Sum(F,Y) by RVSUM_1:75;
end;
theorem
for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(
X \/ Y)) is finite & dom(F|X) misses dom(F|Y) holds Sum(F, X \/ Y) = Sum(F,X) +
Sum(F,Y)
proof
let D be non empty set, F be PartFunc of D,REAL, X,Y be set;
assume that
A1: dom(F|(X \/ Y)) is finite and
A2: dom(F|X) misses dom(F|Y);
A3: dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by RELAT_1:61
.= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23
.= dom(F|X) \/ dom F /\ Y by RELAT_1:61
.= dom(F|X) \/ dom(F|Y) by RELAT_1:61;
then dom(F|X) is finite by A1,FINSET_1:1,XBOOLE_1:7;
then
A4: FinS(F,X) = FinS(F,dom(F| X)) by Th63;
dom(F|Y) is finite by A1,A3,FINSET_1:1,XBOOLE_1:7;
then
A5: FinS(F,Y) = FinS(F,dom(F|Y)) by Th63;
A6: dom(F| dom(F|(X \/ Y))) = dom F /\ dom(F|(X \/ Y)) by RELAT_1:61
.= dom F /\ (dom F /\ (X \/ Y)) by RELAT_1:61
.= dom F /\ dom F /\ (X \/ Y) by XBOOLE_1:16
.= dom(F|(X \/ Y)) by RELAT_1:61;
FinS(F,X \/ Y) = FinS(F,dom(F|(X \/ Y))) by A1,Th63;
hence Sum(F, X \/ Y) = Sum (FinS(F,X) ^ FinS(F,Y)) by A1,A2,A3,A4,A5,A6,Th76,
RFINSEQ:9
.= Sum(F,X) + Sum(F,Y) by RVSUM_1:75;
end;