:: Circled Sets, Circled Hull, and Circled Family
:: by Fahui Zhai , Jianbing Cao and Xiquan Liang
::
:: Received August 30, 2005
:: Copyright (c) 2005-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, XBOOLE_0, RLVECT_1, SUBSET_1, ARYTM_1, RLTOPSP1, REAL_1,
COMPLEX1, XXREAL_0, RELAT_1, TARSKI, ARYTM_3, RUSUB_4, RLSUB_1, STRUCT_0,
SUPINF_2, SETFAM_1, CARD_1, PRE_TOPC, RLVECT_2, FINSEQ_1, FUNCT_1,
CARD_3, NAT_1, FUNCT_2, VALUED_1, ORDINAL4, PARTFUN1, CIRCLED1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, XREAL_0, FUNCT_1, SETFAM_1, PARTFUN1, FUNCT_2, XXREAL_0,
REAL_1, DOMAIN_1, STRUCT_0, PRE_TOPC, RLVECT_1, RUSUB_4, CONVEX1,
FINSEQ_1, RLSUB_1, RLVECT_2, RVSUM_1, RLTOPSP1, RUSUB_5;
constructors SETFAM_1, DOMAIN_1, REAL_1, BINOP_2, COMPLEX1, FINSOP_1, RVSUM_1,
RUSUB_5, CONVEX1, RLTOPSP1, RELSET_1, NUMBERS;
registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0,
RLVECT_1, RLTOPSP1, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, RLTOPSP1;
equalities XBOOLE_0, RVSUM_1;
expansions TARSKI, XBOOLE_0, RLTOPSP1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, SETFAM_1, XCMPLX_0, FUNCT_1,
RLVECT_1, RUSUB_4, CONVEX1, RLTOPSP1, RVSUM_1, FINSEQ_1, RLSUB_1,
RUSUB_5, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, CARD_2, XREAL_1, FINSOP_1,
PARTFUN1, RLVECT_4, XREAL_0;
schemes XBOOLE_0, FINSEQ_1, SUBSET_1;
begin :: Circled Sets
Lm1: for V being non empty RLSStruct, M,N being Subset of V, x,y being VECTOR
of V st x in M & y in N holds x-y in M - N
proof
let V be non empty RLSStruct, M,N be Subset of V, x,y be VECTOR of V;
M-N = {u - v where u,v is VECTOR of V: u in M & v in N} by RUSUB_5:def 2;
hence thesis;
end;
theorem Th1:
for V being RealLinearSpace, A,B being circled Subset of V holds
A-B is circled
proof
let V be RealLinearSpace,A,B be circled Subset of V;
A1: A-B = {u - v where u,v is VECTOR of V: u in A & v in B} by RUSUB_5:def 2;
let r be Real;
assume |.r.| <= 1;
then
A2: r*A c= A & r*B c= B by RLTOPSP1:def 6;
let x be object;
assume
A3: x in r*(A-B);
r*(A-B) = {r * v where v is VECTOR of V: v in A - B} by CONVEX1:def 1;
then consider x9 being VECTOR of V such that
A4: x = r*x9 and
A5: x9 in A-B by A3;
consider u,v being VECTOR of V such that
A6: x9 = u-v and
A7: u in A & v in B by A1,A5;
reconsider r as Real;
A8: r*u in r*A & r*v in r*B by A7,RLTOPSP1:1;
x = r*u-r*v by A4,A6,RLVECT_1:34;
hence thesis by A2,A8,Lm1;
end;
registration
let V be RealLinearSpace, M,N be circled Subset of V;
cluster M - N -> circled;
coherence by Th1;
end;
definition
let V be non empty RLSStruct, M be Subset of V;
redefine attr M is circled means :: redefines circled (RLTOPSP1, definition)
:Def1:
for u being VECTOR of V, r being Real st |.r.| <= 1 & u in M holds r*u in M;
compatibility
proof
thus M is circled implies for u being VECTOR of V, r being Real st |.r.|
<= 1 & u in M holds r*u in M
proof
assume
A1: M is circled;
let u be VECTOR of V, r be Real;
assume |.r.| <= 1;
then
A2: r * M c= M by A1;
assume u in M;
then r*u in r * M by RLTOPSP1:1;
hence thesis by A2;
end;
assume
A3: for u being VECTOR of V, r being Real st |.r.| <= 1 & u in M
holds r*u in M;
let r be Real;
assume
A4: |.r.| <= 1;
reconsider r as Real;
for x being Element of V st x in r * M holds x in M
proof
let x be Element of V;
assume x in r * M;
then consider u be Element of V such that
A5: x = u and
A6: u in r*M;
u in {r * w where w is Element of V : w in M} by A6,CONVEX1:def 1;
then ex w1 be Element of V st u = r * w1 & w1 in M;
hence thesis by A3,A4,A5;
end;
hence thesis;
end;
end;
theorem Th2:
for V be RealLinearSpace, M being Subset of V, r being Real st M
is circled holds r * M is circled
proof
let V be RealLinearSpace, M be Subset of V, r be Real;
assume
A1: M is circled;
for u being VECTOR of V, p being Real st |.p.| <= 1 & u in r * M holds p
*u in r*M
proof
let u be VECTOR of V, p be Real;
assume that
A2: |.p.| <= 1 and
A3: u in r * M;
u in {r * w where w is Element of V: w in M} by A3,CONVEX1:def 1;
then consider u9 be Element of V such that
A4: u = r * u9 and
A5: u9 in M;
A6: p*u = r*p*u9 by A4,RLVECT_1:def 7
.= r*(p*u9) by RLVECT_1:def 7;
p*u9 in M by A1,A2,A5;
hence thesis by A6,RLTOPSP1:1;
end;
hence thesis;
end;
theorem Th3:
for V be RealLinearSpace, M1,M2 being Subset of V, r1,r2 being
Real st M1 is circled & M2 is circled holds r1*M1 + r2*M2 is circled
proof
let V be RealLinearSpace, M1,M2 be Subset of V, r1,r2 be Real;
assume that
A1: M1 is circled and
A2: M2 is circled;
let u be VECTOR of V, p be Real;
assume that
A3: |.p.| <= 1 and
A4: u in r1*M1 + r2*M2;
u in {x+y where x,y is VECTOR of V : x in r1*M1 & y in r2*M2} by A4,
RUSUB_4:def 9;
then consider u1,u2 be VECTOR of V such that
A5: u = u1 + u2 and
A6: u1 in r1*M1 and
A7: u2 in r2*M2;
u1 in {r1*x where x is VECTOR of V : x in M1} by A6,CONVEX1:def 1;
then consider x1 be VECTOR of V such that
A8: u1 = r1*x1 and
A9: x1 in M1;
A10: p*u1 = r1*p*x1 by A8,RLVECT_1:def 7
.= r1*(p*x1) by RLVECT_1:def 7;
u2 in {r2*x where x is VECTOR of V : x in M2} by A7,CONVEX1:def 1;
then consider x2 be VECTOR of V such that
A11: u2 = r2*x2 and
A12: x2 in M2;
A13: p*u2 = r2*p*x2 by A11,RLVECT_1:def 7
.= r2*(p*x2) by RLVECT_1:def 7;
reconsider r1,r2 as Real;
p*x2 in M2 by A2,A3,A12;
then
A14: p*u2 in r2*M2 by A13,RLTOPSP1:1;
p*x1 in M1 by A1,A3,A9;
then
A15: p*u1 in r1*M1 by A10,RLTOPSP1:1;
p*(u1+u2) = p*u1 + p*u2 by RLVECT_1:def 5;
then
p*(u1+u2) in {x+y where x,y is VECTOR of V: x in r1*M1 & y in r2*M2} by A15
,A14;
hence thesis by A5,RUSUB_4:def 9;
end;
theorem
for V be RealLinearSpace, M1,M2,M3 being Subset of V, r1,r2,r3 being
Real st M1 is circled & M2 is circled & M3 is circled holds r1*M1 + r2*M2 + r3*
M3 is circled
proof
let V be RealLinearSpace, M1,M2,M3 be Subset of V, r1,r2,r3 be Real;
assume that
A1: M1 is circled & M2 is circled and
A2: M3 is circled;
r1*M1 + r2*M2 is circled by A1,Th3;
then 1*(r1*M1 + r2*M2) + r3*M3 is circled by A2,Th3;
hence thesis by CONVEX1:32;
end;
theorem
for V being RealLinearSpace holds Up((0).V) is circled
proof
let V be RealLinearSpace, u be VECTOR of V, r be Real;
assume that
|.r.| <= 1 and
A1: u in Up((0).V);
u in the carrier of (0).V by A1,RUSUB_4:def 5;
then u in {0.V} by RLSUB_1:def 3;
then u = 0.V by TARSKI:def 1;
then r * u = 0.V;
then r * u in {0.V} by TARSKI:def 1;
then r * u in the carrier of (0).V by RLSUB_1:def 3;
hence thesis by RUSUB_4:def 5;
end;
theorem Th6:
for V being RealLinearSpace holds Up((Omega).V) is circled
proof
let V be RealLinearSpace, u be VECTOR of V, r be Real;
(Omega).V = the RLSStruct of V by RLSUB_1:def 4;
then r * u in the carrier of (Omega).V;
hence thesis by RUSUB_4:def 5;
end;
theorem
for V being RealLinearSpace, M,N being circled Subset of V holds M /\
N is circled
proof
let V be RealLinearSpace, M,N be circled Subset of V, x be VECTOR of V, r be
Real;
assume that
A1: |.r.| <= 1 and
A2: x in M /\ N;
x in N by A2,XBOOLE_0:def 4;
then
A3: r * x in N by A1,Def1;
x in M by A2,XBOOLE_0:def 4;
then r * x in M by A1,Def1;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
for V being RealLinearSpace, M,N being circled Subset of V holds M \/
N is circled
proof
let V be RealLinearSpace, M,N be circled Subset of V, x be VECTOR of V, r be
Real;
assume that
A1: |.r.| <= 1 and
A2: x in M \/ N;
x in M or x in N by A2,XBOOLE_0:def 3;
then r * x in M or r * x in N by A1,Def1;
hence thesis by XBOOLE_0:def 3;
end;
begin :: Circled Hull and Circled Family
definition
let V be non empty RLSStruct, M be Subset of V;
func Circled-Family M -> Subset-Family of V means
:Def2:
for N being Subset of V holds N in it iff N is circled & M c= N;
existence
proof
defpred P[Subset of V] means $1 is circled & M c= $1;
thus ex F be Subset-Family of V st for N being Subset of V holds N in F
iff P[N] from SUBSET_1:sch 3;
end;
uniqueness
proof
let SF,SG be Subset-Family of V;
assume that
A1: for N being Subset of V holds N in SF iff N is circled & M c= N and
A2: for N being Subset of V holds N in SG iff N is circled & M c= N;
for Y being Subset of V holds Y in SF iff Y in SG
proof
let Y be Subset of V;
hereby
assume Y in SF;
then Y is circled & M c= Y by A1;
hence Y in SG by A2;
end;
assume Y in SG;
then Y is circled & M c= Y by A2;
hence thesis by A1;
end;
hence thesis by SETFAM_1:31;
end;
end;
definition
let V be RealLinearSpace, M be Subset of V;
func Cir M -> circled Subset of V equals
meet Circled-Family M;
coherence
proof
for N being Subset of V st N in Circled-Family M holds N is circled by Def2
;
then Circled-Family M is circled-membered;
hence thesis by RLTOPSP1:30;
end;
end;
registration
let V be RealLinearSpace, M be Subset of V;
cluster Circled-Family M -> non empty;
coherence
proof
A1: M c= Up((Omega).V)
proof
let u be object;
assume u in M;
then reconsider u as Element of V;
u in the carrier of the RLSStruct of V;
then u in the carrier of (Omega).V by RLSUB_1:def 4;
hence thesis by RUSUB_4:def 5;
end;
Up((Omega).V) is circled by Th6;
hence thesis by A1,Def2;
end;
end;
theorem Th9:
for V being RealLinearSpace, M1,M2 being Subset of V st M1 c= M2
holds Circled-Family M2 c= Circled-Family M1
proof
let V be RealLinearSpace, M1,M2 be Subset of V such that
A1: M1 c= M2;
let M be object;
assume
A2: M in Circled-Family M2;
then reconsider M as Subset of V;
M2 c= M by A2,Def2;
then
A3: M1 c= M by A1;
M is circled by A2,Def2;
hence thesis by A3,Def2;
end;
theorem
for V being RealLinearSpace, M1,M2 being Subset of V st M1 c= M2 holds
Cir M1 c= Cir M2
proof
let V be RealLinearSpace, M1,M2 be Subset of V;
assume M1 c= M2;
then Circled-Family M2 c= Circled-Family M1 by Th9;
then
A1: meet Circled-Family M1 c= meet Circled-Family M2 by SETFAM_1:6;
let x be object;
assume x in Cir M1;
hence thesis by A1;
end;
theorem Th11:
for V being RealLinearSpace, M being Subset of V holds M c= Cir( M)
proof
let V be RealLinearSpace, M be Subset of V, u be object;
assume
A1: u in M;
for Y being set holds Y in Circled-Family M implies u in Y
proof
let Y be set;
assume
A2: Y in Circled-Family M;
then reconsider Y as Subset of V;
M c= Y by A2,Def2;
hence thesis by A1;
end;
hence thesis by SETFAM_1:def 1;
end;
theorem Th12:
for V being RealLinearSpace, M being Subset of V, N being
circled Subset of V st M c= N holds Cir M c= N
proof
let V be RealLinearSpace, M be Subset of V, N be circled Subset of V;
assume M c= N;
then N in Circled-Family M by Def2;
hence thesis by SETFAM_1:3;
end;
theorem
for V being RealLinearSpace, M being circled Subset of V holds Cir M = M
by Th12,Th11;
theorem Th14:
for V being RealLinearSpace holds Cir ({}V) = {}
proof
let V be RealLinearSpace;
{}V in Circled-Family {}V by Def2;
hence thesis by SETFAM_1:4;
end;
theorem
for V being RealLinearSpace, M being Subset of V, r being Real holds r
*Cir M = Cir(r*M)
proof
let V be RealLinearSpace, M be Subset of V, r be Real;
thus r*Cir M c= Cir(r*M)
proof
let x be object;
per cases;
suppose
A1: r = 0;
per cases;
suppose
M = {};
then M = {}V;
then Cir M = {} by Th14;
hence thesis by CONVEX1:33;
end;
suppose
A2: M <> {};
then r * M = {0.V} by A1,CONVEX1:34;
then
A3: {0.V} c= Cir(r*M) by Th11;
Cir M <> {} by A2,Th11,XBOOLE_1:3;
then r*Cir M = {0.V} by A1,CONVEX1:34;
hence thesis by A3;
end;
end;
suppose
A4: r <> 0;
A5: r*Cir M = {r*v where v is Point of V: v in Cir M} by CONVEX1:def 1;
assume x in r*Cir M;
then consider v being Point of V such that
A6: x = r*v and
A7: v in Cir M by A5;
for W being set st W in Circled-Family (r*M) holds r*v in W
proof
let W be set;
assume
A8: W in Circled-Family (r*M);
then reconsider W as Subset of V;
r * M c= W by A8,Def2;
then r"*(r*M) c= r"*W by CONVEX1:39;
then (r"*r)*M c= r"*W by CONVEX1:37;
then 1*M c= r"*W by A4,XCMPLX_0:def 7;
then
A9: M c= r"*W by CONVEX1:32;
W is circled by A8,Def2;
then r"*W is circled by Th2;
then r"*W in Circled-Family M by A9,Def2;
then r"*W = {r"*w where w is Point of V: w in W} & v in r"*W by A7,
CONVEX1:def 1,SETFAM_1:def 1;
then consider w being Point of V such that
A10: v = r"*w and
A11: w in W;
r*v = (r*r")*w by A10,RLVECT_1:def 7
.= 1*w by A4,XCMPLX_0:def 7
.= w by RLVECT_1:def 8;
hence thesis by A11;
end;
hence thesis by A6,SETFAM_1:def 1;
end;
end;
r * M c= r*Cir M & r*Cir M is circled by Th2,Th11,CONVEX1:39;
hence thesis by Th12;
end;
begin :: Basic properties of Combination
definition
let V be RealLinearSpace, L be Linear_Combination of V;
attr L is circled means
:Def4:
ex F being FinSequence of the carrier of V st
F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st len f =
len F & Sum(f) = 1 & for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >=
0;
end;
theorem Th16:
for V being RealLinearSpace, L being Linear_Combination of V st
L is circled holds Carrier L <> {}
proof
let V be RealLinearSpace, L be Linear_Combination of V;
assume that
A1: L is circled and
A2: Carrier L = {};
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier L and
A4: ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 & for n
being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A1;
consider f being FinSequence of REAL such that
A5: len f = len F & Sum(f) = 1 & for n
being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A4;
len F = 0 by A2,A3,CARD_1:27,FINSEQ_4:62;
then f = <*>the carrier of V by A5;
hence contradiction by A5,RVSUM_1:72;
end;
theorem Th17:
for V being RealLinearSpace, L being Linear_Combination of V, v
being VECTOR of V st L is circled & L.v <= 0 holds not v in Carrier(L)
proof
let V be RealLinearSpace, L be Linear_Combination of V, v be VECTOR of V;
assume that
A1: L is circled and
A2: L.v <= 0;
per cases by A2;
suppose
L.v = 0;
hence thesis by RLVECT_2:19;
end;
suppose
A3: L.v < 0;
now
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A4: rng F = Carrier L and
A5: ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 &
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A1;
assume v in Carrier(L);
then consider n be object such that
A6: n in dom F and
A7: F.n = v by A4,FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
consider f being FinSequence of REAL such that
A8: len f = len F and
Sum f = 1 and
A9: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
n in Seg len F by A6,FINSEQ_1:def 3;
then
A10: n in dom f by A8,FINSEQ_1:def 3;
then L.v = f.n by A9,A7;
hence contradiction by A3,A9,A10;
end;
hence thesis;
end;
end;
theorem
for V being RealLinearSpace, L being Linear_Combination of V st L is
circled holds L <> ZeroLC(V)
by Th16,RLVECT_2:def 5;
reconsider jj=1, jd=1/2 as Element of REAL by XREAL_0:def 1;
registration
let V be RealLinearSpace;
cluster circled for Linear_Combination of V;
existence
proof
set u = the Element of V;
consider L being Linear_Combination of {u} such that
A1: L.u = jj by RLVECT_4:37;
take L;
L is circled
proof
take <*u*>;
A2: ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 & for
n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
reconsider f = <*jj*> as FinSequence of REAL;
take f;
A3: for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in {1} by FINSEQ_1:2,38;
then
A4: n = 1 by TARSKI:def 1;
then f.n = L.u by A1
.= L.(<*u*>.n) by A4;
hence thesis by A4;
end;
len <*jj*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39;
hence thesis by A3,FINSOP_1:11;
end;
u in {w where w is Element of V : L.w <> 0} by A1;
then u in Carrier L by RLVECT_2:def 4;
then Carrier L c= {u} & {u} c= Carrier L by RLVECT_2:def 6,ZFMISC_1:31;
then Carrier L = {u};
hence thesis by A2,FINSEQ_1:38,FINSEQ_3:93;
end;
hence thesis;
end;
end;
definition
let V be RealLinearSpace;
mode circled_Combination of V is circled Linear_Combination of V;
end;
registration
let V be RealLinearSpace, M be non empty Subset of V;
cluster circled for Linear_Combination of M;
existence
proof
consider u being object such that
A1: u in M by XBOOLE_0:def 1;
reconsider u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2: L.u = jj by RLVECT_4:37;
{u} c= M by A1,ZFMISC_1:31;
then reconsider L as Linear_Combination of M by RLVECT_2:21;
take L;
L is circled
proof
take <*u*>;
A3: ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 & for
n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
reconsider f = <*jj*> as FinSequence of REAL;
take f;
A4: for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in {1} by FINSEQ_1:2,38;
then
A5: n = 1 by TARSKI:def 1;
thus thesis by A2,A5;
end;
len <*jj*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39;
hence thesis by A4,FINSOP_1:11;
end;
u in {w where w is Element of V : L.w <> 0} by A2;
then u in Carrier L by RLVECT_2:def 4;
then Carrier L c= {u} & {u} c= Carrier L by RLVECT_2:def 6,ZFMISC_1:31;
then Carrier L = {u};
hence thesis by A3,FINSEQ_1:38,FINSEQ_3:93;
end;
hence thesis;
end;
end;
definition
let V be RealLinearSpace, M be non empty Subset of V;
mode circled_Combination of M is circled Linear_Combination of M;
end;
definition
let V be RealLinearSpace;
defpred P[object] means $1 is circled_Combination of V;
func circledComb V -> set means
for L being object holds L in it iff L is circled_Combination of V;
existence
proof
consider A being set such that
A1: for x being object holds x in A iff x in Funcs(the carrier of V, REAL
) & P[x] from XBOOLE_0:sch 1;
take A;
let L be object;
thus L in A implies L is circled_Combination of V by A1;
assume L is circled_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st (for x being object holds x in X1 iff P[x])
& (
for x being object holds x in X2 iff P[x])
holds X1 = X2 from XBOOLE_0:sch 3;
end;
end;
definition
let V be RealLinearSpace, M be non empty Subset of V;
defpred P[object] means $1 is circled_Combination of M;
func circledComb M -> set means
for L being object holds L in it iff L is circled_Combination of M;
existence
proof
consider A being set such that
A1: for x being object holds x in A iff x in Funcs(the carrier of V, REAL
) & P[x] from XBOOLE_0:sch 1;
take A;
let L be object;
thus L in A implies L is circled_Combination of M by A1;
assume L is circled_Combination of M;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V holds ex L being
circled_Combination of V st Sum L = v & for A being non empty Subset of V st v
in A holds L is circled_Combination of A
proof
let V be RealLinearSpace, v be VECTOR of V;
consider L being Linear_Combination of {v} such that
A1: L.v = jj by RLVECT_4:37;
consider F being FinSequence of the carrier of V such that
A2: F is one-to-one & rng F = Carrier(L) and
Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
v in Carrier L by A1,RLVECT_2:19;
then Carrier L c= {v} & {v} c= Carrier L by RLVECT_2:def 6,ZFMISC_1:31;
then
A3: {v} = Carrier L;
then F = <*v*> by A2,FINSEQ_3:97;
then
A4: F.1 = v;
deffunc F(set) = L.(F.$1);
consider f being FinSequence such that
A5: len f = len F & for n being Nat st n in dom f holds f.n = F(n) from
FINSEQ_1:sch 2;
A6: len F = 1 by A3,A2,FINSEQ_3:96;
then 1 in dom f by A5,FINSEQ_3:25;
then
A7: f.1 = L.(F.1) by A5;
then f = <*jj*> by A1,A5,A6,A4,FINSEQ_1:40;
then reconsider f as FinSequence of REAL;
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume
A9: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A1,A5,A6,A7,A4,A9,FINSEQ_1:2,TARSKI:def 1;
end;
f = <*jj*> by A1,A5,A6,A7,A4,FINSEQ_1:40;
then Sum(f) = 1 by FINSOP_1:11;
then reconsider L as circled_Combination of V by A2,A5,A8,Def4;
A10: for A being non empty Subset of V st v in A holds L is
circled_Combination of A
by ZFMISC_1:31,A3,RLVECT_2:def 6;
take L;
Sum(L) = 1 * v by A1,A3,RLVECT_2:35;
hence thesis by A10,RLVECT_1:def 8;
end;
theorem
for V being RealLinearSpace, v1,v2 being VECTOR of V st v1 <> v2 holds
ex L being circled_Combination of V st for A being non empty Subset of V st {v1
,v2} c= A holds L is circled_Combination of A
proof
let V be RealLinearSpace, v1,v2 be VECTOR of V;
assume
A1: v1 <> v2;
consider L being Linear_Combination of {v1,v2} such that
A2: L.v1 = jj/2 & L.v2 = jj/2 by A1,RLVECT_4:38;
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier(L) and
Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
deffunc F(set) = L.(F.$1);
consider f being FinSequence such that
A4: len f = len F & for n being Nat st n in dom f holds f.n = F(n) from
FINSEQ_1:sch 2;
v1 in Carrier(L) & v2 in Carrier(L) by A2,RLVECT_2:19;
then Carrier(L) c= {v1,v2} & {v1,v2} c= Carrier(L) by RLVECT_2:def 6
,ZFMISC_1:32;
then
A5: {v1,v2} = Carrier(L);
then
A6: len F = 2 by A1,A3,FINSEQ_3:98;
then 2 in dom f by A4,FINSEQ_3:25;
then
A7: f.2 = L.(F.2) by A4;
1 in dom f by A4,A6,FINSEQ_3:25;
then
A8: f.1 = L.(F.1) by A4;
now
per cases by A1,A5,A3,FINSEQ_3:99;
suppose
F = <*v1,v2*>;
then
A9: F.1 = v1 & F.2 = v2;
then f = <*jd,jd*> by A2,A4,A6,A8,A7,FINSEQ_1:44;
then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:31
.= {jd} by FINSEQ_1:38;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A10: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume
A11: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A2,A4,A6,A8,A7,A9,A11,FINSEQ_1:2,TARSKI:def 2;
end;
f = <*1/2,1/2*> by A2,A4,A6,A8,A7,A9,FINSEQ_1:44;
then Sum(f) = 1/2 + 1/2 by RVSUM_1:77
.= 1;
then reconsider L as circled_Combination of V by A3,A4,A10,Def4;
take L;
for A being non empty Subset of V st {v1,v2} c= A holds L is
circled_Combination of A by A5,RLVECT_2:def 6;
hence thesis;
end;
suppose
F = <*v2,v1*>;
then
A12: F.1 = v2 & F.2 = v1;
then
f = <*jd,jd*> by A2,A4,A6,A8,A7,FINSEQ_1:44;
then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:31
.= {jd} by FINSEQ_1:38;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A13: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume
A14: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A2,A4,A6,A8,A7,A12,A14,FINSEQ_1:2,TARSKI:def 2;
end;
f = <*1/2,1/2*> by A2,A4,A6,A8,A7,A12,FINSEQ_1:44;
then Sum(f) = 1/2 + 1/2 by RVSUM_1:77
.= 1;
then reconsider L as circled_Combination of V by A3,A4,A13,Def4;
take L;
for A being non empty Subset of V st {v1,v2} c= A holds L is
circled_Combination of A by A5,RLVECT_2:def 6;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, L1, L2 being circled_Combination of V, a,
b being Real st a * b > 0 holds Carrier(a*L1 + b*L2) = Carrier(a * L1) \/
Carrier(b * L2)
proof
let V be RealLinearSpace, L1, L2 be circled_Combination of V, a,b be Real;
assume a * b > 0;
then
A1: not (a>=0 & b<=0 or a<=0 & b>=0);
then
A2: Carrier L2 = Carrier(b * L2) by RLVECT_2:42;
A3: Carrier L1 = Carrier(a * L1) by A1,RLVECT_2:42;
for x being object st x in Carrier(a * L1) \/ Carrier(b * L2) holds x in
Carrier(a*L1 + b*L2)
proof
let x be object;
assume
A4: x in Carrier(a * L1) \/ Carrier(b * L2);
per cases by A4,XBOOLE_0:def 3;
suppose
A5: x in Carrier(a * L1);
then x in {v where v is Element of V : (a * L1).v <> 0} by RLVECT_2:def 4
;
then consider v being Element of V such that
A6: v = x and
A7: (a * L1).v <> 0;
A8: L1.v > 0 by A3,A5,A6,Th17;
v in Carrier(a*L1 + b*L2)
proof
per cases;
suppose
A9: v in Carrier L2;
then
A10: L2.v > 0 by Th17;
per cases by A1;
suppose
A11: a > 0 & b > 0;
then b*L2.v > 0 by A10,XREAL_1:129;
then (b*L2).v > 0 by RLVECT_2:def 11;
then
A12: (a*L1).v + (b*L2).v > (a*L1).v by XREAL_1:29;
a*L1.v > 0 by A8,A11,XREAL_1:129;
then (a*L1).v > 0 by RLVECT_2:def 11;
then (a*L1 + b*L2).v > 0 by A12,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
suppose
A13: a < 0 & b < 0;
then a*L1.v < 0 by A3,A5,A6,Th17,XREAL_1:132;
then (a*L1).v < 0 by RLVECT_2:def 11;
then
A14: (a*L1).v + (b*L2).v < (b*L2).v by XREAL_1:30;
b*L2.v < 0 by A9,A13,Th17,XREAL_1:132;
then (b*L2).v < 0 by RLVECT_2:def 11;
then (a*L1 + b*L2).v < 0 by A14,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
end;
suppose
not v in Carrier(L2);
then L2.v = 0 by RLVECT_2:19;
then b*L2.v = 0;
then (b*L2).v = 0 by RLVECT_2:def 11;
then (a*L1).v + (b*L2).v = (a*L1).v;
then (a*L1 + b*L2).v <> 0 by A7,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
end;
hence thesis by A6;
end;
suppose
A15: x in Carrier(b * L2);
then x in {v where v is Element of V : (b * L2).v <> 0} by RLVECT_2:def 4
;
then consider v being Element of V such that
A16: v = x and
A17: (b * L2).v <> 0;
A18: L2.v > 0 by A2,A15,A16,Th17;
v in Carrier(a*L1 + b*L2)
proof
per cases;
suppose
A19: v in Carrier(L1);
then
A20: L1.v > 0 by Th17;
per cases by A1;
suppose
A21: a > 0 & b > 0;
then b*L2.v > 0 by A18,XREAL_1:129;
then (b*L2).v > 0 by RLVECT_2:def 11;
then
A22: (a*L1).v + (b*L2).v > (a*L1).v by XREAL_1:29;
a*L1.v > 0 by A20,A21,XREAL_1:129;
then (a*L1).v > 0 by RLVECT_2:def 11;
then (a*L1 + b*L2).v > 0 by A22,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
suppose
A23: a < 0 & b < 0;
then a*L1.v < 0 by A19,Th17,XREAL_1:132;
then (a*L1).v < 0 by RLVECT_2:def 11;
then
A24: (a*L1).v + (b*L2).v < (b*L2).v by XREAL_1:30;
b*L2.v < 0 by A2,A15,A16,A23,Th17,XREAL_1:132;
then (b*L2).v < 0 by RLVECT_2:def 11;
then (a*L1 + b*L2).v < 0 by A24,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
end;
suppose
not v in Carrier(L1);
then L1.v = 0 by RLVECT_2:19;
then a*L1.v = 0;
then (a*L1).v = 0 by RLVECT_2:def 11;
then (a*L1).v + (b*L2).v = (b*L2).v;
then (a*L1 + b*L2).v <> 0 by A17,RLVECT_2:def 10;
hence thesis by RLVECT_2:19;
end;
end;
hence thesis by A16;
end;
end;
then
A25: Carrier(a * L1) \/ Carrier(b * L2) c= Carrier(a*L1 + b*L2);
Carrier(a*L1 + b*L2) c= Carrier(a*L1) \/ Carrier(b*L2) by RLVECT_2:37;
hence thesis by A25;
end;
theorem Th22:
for V being RealLinearSpace, v being VECTOR of V, L being
Linear_Combination of V st L is circled & Carrier(L) = {v} holds L.v = 1 & Sum(
L) = L.v * v
proof
let V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of V;
assume that
A1: L is circled and
A2: Carrier(L) = {v};
reconsider L as Linear_Combination of {v} by A2,RLVECT_2:def 6;
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier L and
A4: ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 & for n
being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A1;
A5: F = <*v*> by A2,A3,FINSEQ_3:97;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum(f) = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A4;
reconsider r = f/.1 as Element of REAL;
card Carrier(L) = 1 by A2,CARD_1:30;
then len F = 1 by A3,FINSEQ_4:62;
then
A9: dom f = Seg 1 by A6,FINSEQ_1:def 3;
then
A10: 1 in dom f by FINSEQ_1:2,TARSKI:def 1;
then
A11: f.1 = f/.1 by PARTFUN1:def 6;
then f = <* r *> by A9,FINSEQ_1:def 8;
then
A12: Sum f = r by FINSOP_1:11;
f.1 = L.(F.1) by A8,A10;
hence thesis by A7,A11,A12,A5,RLVECT_2:32;
end;
theorem Th23:
for V being RealLinearSpace, v1,v2 being VECTOR of V, L being
Linear_Combination of V st L is circled & Carrier(L) = {v1,v2} & v1 <> v2 holds
L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2
proof
let V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of V;
assume that
A1: L is circled and
A2: Carrier(L) = {v1,v2} and
A3: v1 <> v2;
reconsider L as Linear_Combination of {v1,v2} by A2,RLVECT_2:def 6;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L and
A5: ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 & for n
being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A1;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum(f) = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
len F = card {v1,v2} by A2,A4,FINSEQ_4:62;
then
A9: len f = 2 by A3,A6,CARD_2:57;
then
A10: dom f = {1,2} by FINSEQ_1:2,def 3;
then
A11: 1 in dom f by TARSKI:def 2;
then
A12: f.1 = L.(F.1) by A8;
then f/.1 = L.(F.1) by A11,PARTFUN1:def 6;
then reconsider r1 = L.(F.1) as Element of REAL;
A13: 2 in dom f by A10,TARSKI:def 2;
then
A14: f.2 = L.(F.2) by A8;
then f/.2 = L.(F.2) by A13,PARTFUN1:def 6;
then reconsider r2 = L.(F.2) as Element of REAL;
A15: f = <*r1,r2*> by A9,A12,A14,FINSEQ_1:44;
now
per cases by A2,A3,A4,FINSEQ_3:99;
suppose
F = <*v1,v2*>;
then F.1 = v1 & F.2 = v2;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A7,A8,A11,A13,A12,A14
,A15,RVSUM_1:77;
end;
suppose
F = <*v2,v1*>;
then F.1 = v2 & F.2 = v1;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A7,A8,A11,A13,A12,A14
,A15,RVSUM_1:77;
end;
end;
hence thesis by A3,RLVECT_2:33;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V, L being
Linear_Combination of {v} st L is circled holds L.v = 1 & Sum(L) = L.v * v
proof
let V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of {v};
Carrier L c= {v} by RLVECT_2:def 6;
then
A1: Carrier L = {} or Carrier(L) = {v} by ZFMISC_1:33;
assume L is circled;
hence thesis by A1,Th16,Th22;
end;
theorem
for V being RealLinearSpace, v1,v2 being VECTOR of V, L being
Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds L.v1 + L.v2 = 1
& L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2
proof
let V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of {
v1,v2};
assume that
A1: v1 <> v2 and
A2: L is circled;
A3: Carrier L c= {v1,v2} & Carrier L <> {} by A2,Th16,RLVECT_2:def 6;
now
per cases by A3,ZFMISC_1:36;
suppose
A4: Carrier L = {v1};
then not v2 in Carrier(L) by A1,TARSKI:def 1;
then not v2 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v2 = 0;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A2,A4,Th22;
end;
suppose
A5: Carrier L = {v2};
then not v1 in Carrier(L) by A1,TARSKI:def 1;
then not v1 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v1 = 0;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A2,A5,Th22;
end;
suppose
Carrier(L) = {v1,v2};
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A1,A2,Th23;
end;
end;
hence thesis by A1,RLVECT_2:33;
end;