:: CIRCLED1 semantic presentation

Lemma1: for b₁ being non empty RLSStruct
for b₂, b₃ being Subset of b₁
for b₄, b₅ being VECTOR of b₁ st b₄ in b₂ & b₅ in b₃ holds
b₄ - b₅ in b₂ - b₃

proof end;

theorem Th1: :: CIRCLED1:1

for b₁ being RealLinearSpace
for b₂, b₃ being circled Subset of b₁ holds b₂ - b₃ is circled

proof end;

registration

let c₁ be RealLinearSpace;
let c₂, c₃ be circled Subset of c₁;
cluster a₂ - a₃ -> circled ;
coherence by Th1;

end;

theorem Th2: :: CIRCLED1:2

for b₁ being non empty RLSStruct
for b₂ being Subset of b₁ holds
( b₂ is circled iff for b₃ being VECTOR of b₁
for b₄ being Real st abs b₄ <= 1 & b₃ in b₂ holds
b₄ * b₃ in b₂ )

proof end;

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is circled means :Def1: :: CIRCLED1:def 1
for b₁ being VECTOR of a₁
for b₂ being Real st abs b₂ <= 1 & b₁ in a₂ holds
b₂ * b₁ in a₂;
compatibility by Th2;

end;

:: deftheorem Def1 defines circled CIRCLED1:def 1 :

theorem Th3: :: CIRCLED1:3

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being Real st b₂ is circled holds
b₃ * b₂ is circled

proof end;

theorem Th4: :: CIRCLED1:4

for b₁ being RealLinearSpace
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Real st b₂ is circled & b₃ is circled holds
(b₄ * b₂) + (b₅ * b₃) is circled

proof end;

theorem Th5: :: CIRCLED1:5

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subset of b₁
for b₅, b₆, b₇ being Real st b₂ is circled & b₃ is circled & b₄ is circled holds
((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) is circled

proof end;

theorem Th6: :: CIRCLED1:6

for b₁ being RealLinearSpace holds Up ((0). b₁) is circled

proof end;

theorem Th7: :: CIRCLED1:7

for b₁ being RealLinearSpace holds Up ((Omega). b₁) is circled

proof end;

theorem Th8: :: CIRCLED1:8

for b₁ being RealLinearSpace
for b₂, b₃ being circled Subset of b₁ holds b₂ /\ b₃ is circled

proof end;

theorem Th9: :: CIRCLED1:9

for b₁ being RealLinearSpace
for b₂, b₃ being circled Subset of b₁ holds b₂ \/ b₃ is circled

proof end;

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
func Circled-Family c₂ -> Subset-Family of a₁ means :Def2: :: CIRCLED1:def 2
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ( b₁ is circled & a₂ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
func Cir c₂ -> circled Subset of a₁ equals :: CIRCLED1:def 3
meet (Circled-Family a₂);
coherence

proof end;

end;

:: deftheorem Def3 defines Cir CIRCLED1:def 3 :

registration

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
cluster Circled-Family a₂ -> non empty ;
coherence

proof end;

end;

theorem Th10: :: CIRCLED1:10

for b₁ being RealLinearSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Circled-Family b₃ c= Circled-Family b₂

proof end;

theorem Th11: :: CIRCLED1:11

for b₁ being RealLinearSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Cir b₂ c= Cir b₃

proof end;

theorem Th12: :: CIRCLED1:12

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds b₂ c= Cir b₂

proof end;

theorem Th13: :: CIRCLED1:13

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being circled Subset of b₁ st b₂ c= b₃ holds
Cir b₂ c= b₃

proof end;

theorem Th14: :: CIRCLED1:14

for b₁ being RealLinearSpace
for b₂ being circled Subset of b₁ holds Cir b₂ = b₂

proof end;

theorem Th15: :: CIRCLED1:15

for b₁ being RealLinearSpace holds Cir ({} b₁) = {}

proof end;

theorem Th16: :: CIRCLED1:16

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being Real holds b₃ * (Cir b₂) = Cir (b₃ * b₂)

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Linear_Combination of c₁;
attr a₂ is circled means :Def4: :: CIRCLED1:def 4
ex b₁ being FinSequence of the carrier of a₁ st
( b₁ is one-to-one & rng b₁ = Carrier a₂ & ex b₂ being FinSequence of REAL st
( len b₂ = len b₁ & Sum b₂ = 1 & ( for b₃ being Nat st b₃ in dom b₂ holds
( b₂ . b₃ = a₂ . (b₁ . b₃) & b₂ . b₃ >= 0 ) ) ) );

end;

:: deftheorem Def4 defines circled CIRCLED1:def 4 :

theorem Th17: :: CIRCLED1:17

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ st b₂ is circled holds
Carrier b₂ <> {}

proof end;

theorem Th18: :: CIRCLED1:18

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being VECTOR of b₁ st b₂ is circled & b₂ . b₃ <= 0 holds
not b₃ in Carrier b₂

proof end;

theorem Th19: :: CIRCLED1:19

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ st b₂ is circled holds
b₂ <> ZeroLC b₁

proof end;

theorem Th20: :: CIRCLED1:20

for b₁ being RealLinearSpace ex b₂ being Linear_Combination of b₁ st b₂ is circled

proof end;

registration

let c₁ be RealLinearSpace;
cluster circled Linear_Combination of a₁;
existence by Th20;

end;

definition

let c₁ be RealLinearSpace;
mode circled_Combination of a₁ is circled Linear_Combination of a₁;

end;

theorem Th21: :: CIRCLED1:21

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ ex b₃ being Linear_Combination of b₂ st b₃ is circled

proof end;

registration

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
cluster circled Linear_Combination of a₂;
existence by Th21;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
mode circled_Combination of a₂ is circled Linear_Combination of a₂;

end;

definition

let c₁ be RealLinearSpace;
defpred S₁[ set ] means a₁ is circled_Combination of c₁;
func circledComb c₁ -> set means :: CIRCLED1:def 5
for b₁ being set holds
( b₁ in a₂ iff b₁ is circled_Combination of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines circledComb CIRCLED1:def 5 :

definition

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
defpred S₁[ set ] means a₁ is circled_Combination of c₂;
func circledComb c₂ -> set means :: CIRCLED1:def 6
for b₁ being set holds
( b₁ in a₃ iff b₁ is circled_Combination of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines circledComb CIRCLED1:def 6 :

theorem Th22: :: CIRCLED1:22

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ ex b₃ being circled_Combination of b₁ st
( Sum b₃ = b₂ & ( for b₄ being non empty Subset of b₁ st b₂ in b₄ holds
b₃ is circled_Combination of b₄ ) )

proof end;

theorem Th23: :: CIRCLED1:23

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st b₂ <> b₃ holds
ex b₄ being circled_Combination of b₁ st
for b₅ being non empty Subset of b₁ st {b₂,b₃} c= b₅ holds
b₄ is circled_Combination of b₅

proof end;

theorem Th24: :: CIRCLED1:24

for b₁ being RealLinearSpace
for b₂, b₃ being circled_Combination of b₁
for b₄, b₅ being Real st b₄ * b₅ > 0 holds
Carrier ((b₄ * b₂) + (b₅ * b₃)) = (Carrier (b₄ * b₂)) \/ (Carrier (b₅ * b₃))

proof end;

theorem Th25: :: CIRCLED1:25

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of b₁ st b₃ is circled & Carrier b₃ = {b₂} holds
( b₃ . b₂ = 1 & Sum b₃ = (b₃ . b₂) * b₂ )

proof end;

theorem Th26: :: CIRCLED1:26

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Linear_Combination of b₁ st b₄ is circled & Carrier b₄ = {b₂,b₃} & b₂ <> b₃ holds
( (b₄ . b₂) + (b₄ . b₃) = 1 & b₄ . b₂ >= 0 & b₄ . b₃ >= 0 & Sum b₄ = ((b₄ . b₂) * b₂) + ((b₄ . b₃) * b₃) )

proof end;

theorem Th27: :: CIRCLED1:27

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of {b₂} st b₃ is circled holds
( b₃ . b₂ = 1 & Sum b₃ = (b₃ . b₂) * b₂ )

proof end;

theorem Th28: :: CIRCLED1:28

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Linear_Combination of {b₂,b₃} st b₂ <> b₃ & b₄ is circled holds
( (b₄ . b₂) + (b₄ . b₃) = 1 & b₄ . b₂ >= 0 & b₄ . b₃ >= 0 & Sum b₄ = ((b₄ . b₂) * b₂) + ((b₄ . b₃) * b₃) )

proof end;