:: Circled Sets, Circled Hull, and Circled Family
:: by Fahui Zhai , Jianbing Cao and Xiquan Liang
::
:: Received August 30, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

Lm1:  for V being non empty RLSStruct
for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
proofend;

theorem Th1: :: CIRCLED1:1
for V being RealLinearSpace
for A, B being circled Subset of V holds A - B is circled
proofend;

registration
let V be RealLinearSpace;
let M, N be circled Subset of V;
clusterM - N ->  circled ;
coherence
 M - N is circled by Th1;
end;

definition
let V be non empty RLSStruct ;
let M be Subset of V;
redefine attr M is circled  means :Def1: :: CIRCLED1:def 1
 for u being VECTOR of V
for r being Real st abs r <= 1 &amp; u in M holds
r * u in M;
compatibility
 ( M is circled iff for u being VECTOR of V
for r being Real st abs r <= 1 &amp; u in M holds
r * u in M )
proofend;
end;

:: deftheorem Def1 defines circled CIRCLED1:def_1_:_
 for V being non empty RLSStruct
for M being Subset of V holds
( M is circled iff for u being VECTOR of V
for r being Real st abs r <= 1 &amp; u in M holds
r * u in M );

theorem Th2: :: CIRCLED1:2
for V being RealLinearSpace
for M being Subset of V
for r being Real st M is circled holds
r * M is circled
proofend;

theorem Th3: :: CIRCLED1:3
for V being RealLinearSpace
for M1, M2 being Subset of V
for r1, r2 being Real st M1 is circled &amp; M2 is circled holds
(r1 * M1) + (r2 * M2) is circled
proofend;

theorem :: CIRCLED1:4
for V being RealLinearSpace
for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is circled &amp; M2 is circled &amp; M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
proofend;

theorem :: CIRCLED1:5
for V being RealLinearSpace holds Up ((0). V) is circled
proofend;

theorem Th6: :: CIRCLED1:6
for V being RealLinearSpace holds Up ((Omega). V) is circled
proofend;

theorem :: CIRCLED1:7
for V being RealLinearSpace
for M, N being circled Subset of V holds M /\ N is circled
proofend;

theorem :: CIRCLED1:8
for V being RealLinearSpace
for M, N being circled Subset of V holds M \/ N is circled
proofend;

begin

definition
let V be non empty RLSStruct ;
let M be Subset of V;
func Circled-Family M ->  Subset-Family of V means :Def2: :: CIRCLED1:def 2
 for N being Subset of V holds
( N in it iff ( N is circled &amp; M c= N ) );
existence
 ex b1 being Subset-Family of V st
for N being Subset of V holds
( N in b1 iff ( N is circled &amp; M c= N ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of V st ( for N being Subset of V holds
( N in b1 iff ( N is circled &amp; M c= N ) ) ) &amp; ( for N being Subset of V holds
( N in b2 iff ( N is circled &amp; M c= N ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Circled-Family CIRCLED1:def_2_:_
 for V being non empty RLSStruct
for M being Subset of V
for b3 being Subset-Family of V holds
( b3 = Circled-Family M iff for N being Subset of V holds
( N in b3 iff ( N is circled &amp; M c= N ) ) );

definition
let V be RealLinearSpace;
let M be Subset of V;
func Cir M ->  circled Subset of V equals :: CIRCLED1:def 3
 meet (Circled-Family M);
coherence
 meet (Circled-Family M) is circled Subset of V
proofend;
end;

:: deftheorem  defines Cir CIRCLED1:def_3_:_
 for V being RealLinearSpace
for M being Subset of V holds Cir M = meet (Circled-Family M);

registration
let V be RealLinearSpace;
let M be Subset of V;
cluster Circled-Family M ->  non empty ;
coherence
 not Circled-Family M is empty
proofend;
end;

theorem Th9: :: CIRCLED1:9
for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Circled-Family M2 c= Circled-Family M1
proofend;

theorem :: CIRCLED1:10
for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Cir M1 c= Cir M2
proofend;

theorem Th11: :: CIRCLED1:11
for V being RealLinearSpace
for M being Subset of V holds M c= Cir M
proofend;

theorem Th12: :: CIRCLED1:12
for V being RealLinearSpace
for M being Subset of V
for N being circled Subset of V st M c= N holds
Cir M c= N
proofend;

theorem :: CIRCLED1:13
for V being RealLinearSpace
for M being circled Subset of V holds Cir M = M
proofend;

theorem Th14: :: CIRCLED1:14
for V being RealLinearSpace holds Cir ({} V) = {}
proofend;

theorem :: CIRCLED1:15
for V being RealLinearSpace
for M being Subset of V
for r being Real holds r * (Cir M) = Cir (r * M)
proofend;

begin

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
attrL is circled  means :Def4: :: CIRCLED1:def 4
 ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) );
end;

:: deftheorem Def4 defines circled CIRCLED1:def_4_:_
 for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is circled iff ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) ) );

theorem Th16: :: CIRCLED1:16
for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
Carrier L <> {}
proofend;

theorem Th17: :: CIRCLED1:17
for V being RealLinearSpace
for L being Linear_Combination of V
for v being VECTOR of V st L is circled &amp; L . v <= 0 holds
not v in Carrier L
proofend;

theorem :: CIRCLED1:18
for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V
proofend;

registration
let V be RealLinearSpace;
clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of V;
existence
 ex b1 being Linear_Combination of V st b1 is circled
proofend;
end;

definition
let V be RealLinearSpace;
mode circled_Combination of V is circled Linear_Combination of V;
end;

registration
let V be RealLinearSpace;
let M be non empty Subset of V;
clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of M;
existence
 ex b1 being Linear_Combination of M st b1 is circled
proofend;
end;

definition
let V be RealLinearSpace;
let 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 S1[ set ] means $1 is circled_Combination of V;
func circledComb V ->  set  means :: CIRCLED1:def 5
 for L being set holds
( L in it iff L is circled_Combination of V );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is circled_Combination of V )
proofend;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is circled_Combination of V ) ) &amp; ( for L being set holds
( L in b2 iff L is circled_Combination of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines circledComb CIRCLED1:def_5_:_
 for V being RealLinearSpace
for b2 being set holds
( b2 = circledComb V iff for L being set holds
( L in b2 iff L is circled_Combination of V ) );

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S1[ set ] means $1 is circled_Combination of M;
func circledComb M ->  set  means :: CIRCLED1:def 6
 for L being set holds
( L in it iff L is circled_Combination of M );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is circled_Combination of M )
proofend;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is circled_Combination of M ) ) &amp; ( for L being set holds
( L in b2 iff L is circled_Combination of M ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines circledComb CIRCLED1:def_6_:_
 for V being RealLinearSpace
for M being non empty Subset of V
for b3 being set holds
( b3 = circledComb M iff for L being set holds
( L in b3 iff L is circled_Combination of M ) );

theorem :: CIRCLED1:19
for V being RealLinearSpace
for v being VECTOR of V ex L being circled_Combination of V st
( Sum L = v &amp; ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
proofend;

theorem :: CIRCLED1:20
for V being RealLinearSpace
for 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
proofend;

theorem :: CIRCLED1:21
for V being RealLinearSpace
for L1, L2 being circled_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
proofend;

theorem Th22: :: CIRCLED1:22
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is circled &amp; Carrier L = {v} holds
( L . v = 1 &amp; Sum L = (L . v) * v )
proofend;

theorem Th23: :: CIRCLED1:23
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is circled &amp; Carrier L = {v1,v2} &amp; v1 <> v2 holds
( (L . v1) + (L . v2) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;

theorem :: CIRCLED1:24
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of {v} st L is circled holds
( L . v = 1 &amp; Sum L = (L . v) * v )
proofend;

theorem :: CIRCLED1:25
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of {v1,v2} st v1 <> v2 &amp; L is circled holds
( (L . v1) + (L . v2) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;