:: by Fahui Zhai , Jianbing Cao and Xiquan Liang

::

:: Received August 30, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

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

proof end;

registration
end;

definition

let V be non empty RLSStruct ;

let M be Subset of V;

( M is circled iff for u being VECTOR of V

for r being Real st |.r.| <= 1 & u in M holds

r * u in M )

end;
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 |.r.| <= 1 & u in M holds

r * u in M;

compatibility for u being VECTOR of V

for r being Real st |.r.| <= 1 & u in M holds

r * u in M;

( M is circled iff for u being VECTOR of V

for r being Real st |.r.| <= 1 & u in M holds

r * u in M )

proof 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 |.r.| <= 1 & u in M holds

r * u in M );

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 |.r.| <= 1 & 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

for M being Subset of V

for r being Real st M is circled holds

r * M is circled

proof end;

theorem Th3: :: CIRCLED1:3

for V being RealLinearSpace

for M1, M2 being Subset of V

for r1, r2 being Real st M1 is circled & M2 is circled holds

(r1 * M1) + (r2 * M2) is circled

for M1, M2 being Subset of V

for r1, r2 being Real st M1 is circled & M2 is circled holds

(r1 * M1) + (r2 * M2) is circled

proof end;

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 & M2 is circled & M3 is circled holds

((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled

for M1, M2, M3 being Subset of V

for 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 end;

definition

let V be non empty RLSStruct ;

let M be Subset of V;

ex b_{1} being Subset-Family of V st

for N being Subset of V holds

( N in b_{1} iff ( N is circled & M c= N ) )

for b_{1}, b_{2} being Subset-Family of V st ( for N being Subset of V holds

( N in b_{1} iff ( N is circled & M c= N ) ) ) & ( for N being Subset of V holds

( N in b_{2} iff ( N is circled & M c= N ) ) ) holds

b_{1} = b_{2}

end;
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 & M c= N ) );

existence for N being Subset of V holds

( N in it iff ( N is circled & M c= N ) );

ex b

for N being Subset of V holds

( N in b

proof end;

uniqueness for b

( N in b

( N in b

b

proof end;

:: deftheorem Def2 defines Circled-Family CIRCLED1:def 2 :

for V being non empty RLSStruct

for M being Subset of V

for b_{3} being Subset-Family of V holds

( b_{3} = Circled-Family M iff for N being Subset of V holds

( N in b_{3} iff ( N is circled & M c= N ) ) );

for V being non empty RLSStruct

for M being Subset of V

for b

( b

( N in b

definition

let V be RealLinearSpace;

let M be Subset of V;

coherence

meet (Circled-Family M) is circled Subset of V

end;
let M be Subset of V;

coherence

meet (Circled-Family M) is circled Subset of V

proof end;

:: deftheorem defines Cir CIRCLED1:def 3 :

for V being RealLinearSpace

for M being Subset of V holds Cir M = meet (Circled-Family M);

for V being RealLinearSpace

for M being Subset of V holds Cir M = meet (Circled-Family M);

registration
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

for M1, M2 being Subset of V st M1 c= M2 holds

Circled-Family M2 c= Circled-Family M1

proof end;

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

for M being Subset of V

for N being circled Subset of V st M c= N holds

Cir M c= N

proof end;

theorem :: CIRCLED1:13

theorem :: CIRCLED1:15

for V being RealLinearSpace

for M being Subset of V

for r being Real holds r * (Cir M) = Cir (r * M)

for M being Subset of V

for r being Real holds r * (Cir M) = Cir (r * M)

proof 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 & 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 ) ) ) ) );

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 & 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 ) ) ) ) );

theorem Th16: :: CIRCLED1:16

for V being RealLinearSpace

for L being Linear_Combination of V st L is circled holds

Carrier L <> {}

for L being Linear_Combination of V st L is circled holds

Carrier L <> {}

proof end;

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 & L . v <= 0 holds

not v in Carrier L

for L being Linear_Combination of V

for v being VECTOR of V st L is circled & L . v <= 0 holds

not v in Carrier L

proof end;

theorem :: CIRCLED1:18

for V being RealLinearSpace

for L being Linear_Combination of V st L is circled holds

L <> ZeroLC V by Th16, RLVECT_2:def 5;

for 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;

ex b_{1} being Linear_Combination of V st b_{1} is circled

end;
cluster V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V60() V61() V62() circled for Linear_Combination of V;

existence ex b

proof end;

definition
end;

registration

let V be RealLinearSpace;

let M be non empty Subset of V;

ex b_{1} being Linear_Combination of M st b_{1} is circled

end;
let M be non empty Subset of V;

cluster V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V60() V61() V62() circled for Linear_Combination of M;

existence ex b

proof 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;
let M be non empty Subset of V;

mode circled_Combination of M is circled Linear_Combination of M;

definition

let V be RealLinearSpace;

defpred S_{1}[ object ] means $1 is circled_Combination of V;

ex b_{1} being set st

for L being object holds

( L in b_{1} iff L is circled_Combination of V )

for b_{1}, b_{2} being set st ( for L being object holds

( L in b_{1} iff L is circled_Combination of V ) ) & ( for L being object holds

( L in b_{2} iff L is circled_Combination of V ) ) holds

b_{1} = b_{2}

end;
defpred S

func circledComb V -> set means :: CIRCLED1:def 5

for L being object holds

( L in it iff L is circled_Combination of V );

existence for L being object holds

( L in it iff L is circled_Combination of V );

ex b

for L being object holds

( L in b

proof end;

uniqueness for b

( L in b

( L in b

b

proof end;

:: deftheorem defines circledComb CIRCLED1:def 5 :

for V being RealLinearSpace

for b_{2} being set holds

( b_{2} = circledComb V iff for L being object holds

( L in b_{2} iff L is circled_Combination of V ) );

for V being RealLinearSpace

for b

( b

( L in b

definition

let V be RealLinearSpace;

let M be non empty Subset of V;

defpred S_{1}[ object ] means $1 is circled_Combination of M;

ex b_{1} being set st

for L being object holds

( L in b_{1} iff L is circled_Combination of M )

for b_{1}, b_{2} being set st ( for L being object holds

( L in b_{1} iff L is circled_Combination of M ) ) & ( for L being object holds

( L in b_{2} iff L is circled_Combination of M ) ) holds

b_{1} = b_{2}

end;
let M be non empty Subset of V;

defpred S

func circledComb M -> set means :: CIRCLED1:def 6

for L being object holds

( L in it iff L is circled_Combination of M );

existence for L being object holds

( L in it iff L is circled_Combination of M );

ex b

for L being object holds

( L in b

proof end;

uniqueness for b

( L in b

( L in b

b

proof end;

:: deftheorem defines circledComb CIRCLED1:def 6 :

for V being RealLinearSpace

for M being non empty Subset of V

for b_{3} being set holds

( b_{3} = circledComb M iff for L being object holds

( L in b_{3} iff L is circled_Combination of M ) );

for V being RealLinearSpace

for M being non empty Subset of V

for b

( b

( L in b

theorem :: CIRCLED1:19

for V being RealLinearSpace

for v being VECTOR of V 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 ) )

for v being VECTOR of V 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 end;

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

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

proof end;

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))

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))

proof end;

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 & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

for v being VECTOR of V

for L being Linear_Combination of V st L is circled & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

proof end;

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 & 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) )

for v1, v2 being VECTOR of V

for 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 end;

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 & Sum L = (L . v) * v )

for v being VECTOR of V

for L being Linear_Combination of {v} st L is circled holds

( L . v = 1 & Sum L = (L . v) * v )

proof end;

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 & L is circled holds

( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )

for v1, v2 being VECTOR of V

for 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 end;