:: CIRCLED1 semantic presentation

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;

theorem Th1: :: CIRCLED1:1

for V being RealLinearSpace
for A, B being circled Subset of V holds A - B is circled

proof end;

registration

let V be RealLinearSpace;
let M, N be circled Subset of V;
cluster M - N -> circled ;
coherence by Th1;

end;

theorem Th2: :: CIRCLED1:2

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 & u in M holds
r * u in M )

proof 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 & u in M holds
r * u in M;
compatibility by Th2;

end;

:: deftheorem Def1 defines circled CIRCLED1:def 1 :

theorem Th3: :: CIRCLED1:3

for V being RealLinearSpace
for M being Subset of V
for r being Real st M is circled holds
r * M is circled

proof end;

theorem Th4: :: CIRCLED1:4

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

proof end;

theorem :: CIRCLED1:5

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

proof end;

theorem :: CIRCLED1:6

for V being RealLinearSpace holds Up ((0). V) is circled

proof end;

theorem Th7: :: CIRCLED1:7

for V being RealLinearSpace holds Up ((Omega). V) is circled

proof end;

theorem :: CIRCLED1:8

for V being RealLinearSpace
for M, N being circled Subset of V holds M /\ N is circled

proof end;

theorem :: CIRCLED1:9

for V being RealLinearSpace
for M, N being circled Subset of V holds M \/ N is circled

proof end;

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

proof end;

uniqueness

proof end;

end;

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

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

proof end;

end;

:: deftheorem defines Cir CIRCLED1:def 3 :

registration

let V be RealLinearSpace;
let M be Subset of V;
cluster Circled-Family M -> non empty ;
coherence

proof end;

end;

theorem Th10: :: CIRCLED1:10

for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Circled-Family M2 c= Circled-Family M1

proof end;

theorem :: CIRCLED1:11

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

proof end;

theorem Th12: :: CIRCLED1:12

for V being RealLinearSpace
for M being Subset of V holds M c= Cir M

proof end;

theorem Th13: :: CIRCLED1:13

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

proof end;

theorem :: CIRCLED1:14

for V being RealLinearSpace
for M being circled Subset of V holds Cir M = M

proof end;

theorem Th15: :: CIRCLED1:15

for V being RealLinearSpace holds Cir ({} V) = {}

proof end;

theorem :: CIRCLED1:16

for V being RealLinearSpace
for M being Subset of V
for r being Real holds r * (Cir M) = Cir (r * M)

proof end;

definition

let V be RealLinearSpace;
let L be Linear_Combination of V;
attr L is circled means :Def4: :: CIRCLED1:def 4
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;

:: deftheorem Def4 defines circled CIRCLED1:def 4 :

theorem Th17: :: CIRCLED1:17

for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
Carrier L <> {}

proof end;

theorem Th18: :: CIRCLED1:18

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

proof end;

theorem :: CIRCLED1:19

for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V

proof end;

theorem Th20: :: CIRCLED1:20

for V being RealLinearSpace ex L being Linear_Combination of V st L is circled

proof end;

registration

let V be RealLinearSpace;
cluster circled Linear_Combination of V;
existence by Th20;

end;

definition

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

end;

theorem Th21: :: CIRCLED1:21

for V being RealLinearSpace
for M being non empty Subset of V ex L being Linear_Combination of M st L is circled

proof end;

registration

let V be RealLinearSpace;
let M be non empty Subset of V;
cluster circled Linear_Combination of M;
existence by Th21;

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 S₁[ 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines circledComb CIRCLED1:def 5 :

definition

let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S₁[ 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines circledComb CIRCLED1:def 6 :

theorem :: CIRCLED1:22

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

proof end;

theorem :: CIRCLED1:23

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

proof end;

theorem :: CIRCLED1:24

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

proof end;

theorem Th25: :: CIRCLED1:25

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 )

proof end;

theorem Th26: :: CIRCLED1:26

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

proof end;

theorem :: CIRCLED1:27

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 )

proof end;

theorem :: CIRCLED1:28

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

proof end;