:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama

::

:: Received November 5, 2002

:: Copyright (c) 2002 Association of Mizar Users

begin

definition

let V be non empty RLSStruct ;

let M be Subset of V;

let r be Real;

func r * M -> Subset of V equals :: CONVEX1:def 1

{ (r * v) where v is Element of V : v in M } ;

coherence

{ (r * v) where v is Element of V : v in M } is Subset of V

end;
let M be Subset of V;

let r be Real;

func r * M -> Subset of V equals :: CONVEX1:def 1

{ (r * v) where v is Element of V : v in M } ;

coherence

{ (r * v) where v is Element of V : v in M } is Subset of V

proof end;

:: deftheorem defines * CONVEX1:def 1 :

for V being non empty RLSStruct

for M being Subset of V

for r being Real holds r * M = { (r * v) where v is Element of V : v in M } ;

definition

let V be non empty RLSStruct ;

let M be Subset of V;

attr M is convex means :Def2: :: CONVEX1:def 2

for u, v being VECTOR of V

for r being Real st 0 < r & r < 1 & u in M & v in M holds

(r * u) + ((1 - r) * v) in M;

end;
let M be Subset of V;

attr M is convex means :Def2: :: CONVEX1:def 2

for u, v being VECTOR of V

for r being Real st 0 < r & r < 1 & u in M & v in M holds

(r * u) + ((1 - r) * v) in M;

:: deftheorem Def2 defines convex CONVEX1:def 2 :

for V being non empty RLSStruct

for M being Subset of V holds

( M is convex iff for u, v being VECTOR of V

for r being Real st 0 < r & r < 1 & u in M & v in M holds

(r * u) + ((1 - r) * v) in M );

theorem :: CONVEX1:1

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V

for r being Real st M is convex holds

r * M is convex

for M being Subset of V

for r being Real st M is convex holds

r * M is convex

proof end;

theorem :: CONVEX1:2

for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M, N being Subset of V st M is convex & N is convex holds

M + N is convex

for M, N being Subset of V st M is convex & N is convex holds

M + N is convex

proof end;

theorem :: CONVEX1:3

for V being RealLinearSpace

for M, N being Subset of V st M is convex & N is convex holds

M - N is convex

for M, N being Subset of V st M is convex & N is convex holds

M - N is convex

proof end;

theorem Th4: :: CONVEX1:4

for V being non empty RLSStruct

for M being Subset of V holds

( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

for M being Subset of V holds

( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

proof end;

theorem :: CONVEX1:5

for V being non empty Abelian RLSStruct

for M being Subset of V st M is convex holds

for r being Real st 0 < r & r < 1 holds

((1 - r) * M) + (r * M) c= M

for M being Subset of V st M is convex holds

for r being Real st 0 < r & r < 1 holds

((1 - r) * M) + (r * M) c= M

proof end;

theorem :: CONVEX1:6

for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M, N being Subset of V st M is convex & N is convex holds

for r being Real holds (r * M) + ((1 - r) * N) is convex

for M, N being Subset of V st M is convex & N is convex holds

for r being Real holds (r * M) + ((1 - r) * N) is convex

proof end;

Lm1: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V holds 1 * M = M

proof end;

Lm2: for V being RealLinearSpace

for M being non empty Subset of V holds 0 * M = {(0. V)}

proof end;

Lm3: for V being non empty add-associative addLoopStr

for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)

proof end;

Lm4: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V

for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M

proof end;

Lm5: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M1, M2 being Subset of V

for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)

proof end;

theorem :: CONVEX1:7

for V being RealLinearSpace

for M being Subset of V

for v being VECTOR of V holds

( M is convex iff v + M is convex )

for M being Subset of V

for v being VECTOR of V holds

( M is convex iff v + M is convex )

proof end;

theorem :: CONVEX1:8

proof end;

theorem Th9: :: CONVEX1:9

proof end;

theorem Th10: :: CONVEX1:10

proof end;

theorem Th11: :: CONVEX1:11

for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M1, M2 being Subset of V

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

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

for M1, M2 being Subset of V

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

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

proof end;

theorem Th12: :: CONVEX1:12

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V

for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)

for M being Subset of V

for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)

proof end;

Lm6: for V being non empty RLSStruct

for M, N being Subset of V

for r being Real st M c= N holds

r * M c= r * N

proof end;

Lm7: for V being non empty RLSStruct

for M being empty Subset of V

for r being Real holds r * M = {}

proof end;

Lm8: for V being non empty addLoopStr

for M being empty Subset of V

for N being Subset of V holds M + N = {}

proof end;

Lm9: for V being non empty right_zeroed addLoopStr

for M being Subset of V holds M + {(0. V)} = M

proof end;

Lm10: for V being RealLinearSpace

for M being Subset of V

for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds

(r1 * M) + (r2 * M) c= (r1 + r2) * M

proof end;

theorem :: CONVEX1:13

for V being RealLinearSpace

for M being Subset of V

for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds

(r1 * M) + (r2 * M) = (r1 + r2) * M

for M being Subset of V

for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds

(r1 * M) + (r2 * M) = (r1 + r2) * M

proof end;

theorem :: CONVEX1:14

for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M1, M2, M3 being Subset of V

for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

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

for M1, M2, M3 being Subset of V

for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

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

proof end;

theorem Th15: :: CONVEX1:15

for V being non empty RLSStruct

for F being Subset-Family of V st ( for M being Subset of V st M in F holds

M is convex ) holds

meet F is convex

for F being Subset-Family of V st ( for M being Subset of V st M in F holds

M is convex ) holds

meet F is convex

proof end;

theorem Th16: :: CONVEX1:16

proof end;

registration

let V be non empty RLSStruct ;

cluster non empty convex Element of K10( the carrier of V);

existence

ex b_{1} being Subset of V st

( not b_{1} is empty & b_{1} is convex )

end;
cluster non empty convex Element of K10( the carrier of V);

existence

ex b

( not b

proof end;

registration

let V be non empty RLSStruct ;

cluster empty convex Element of K10( the carrier of V);

existence

ex b_{1} being Subset of V st

( b_{1} is empty & b_{1} is convex )

end;
cluster empty convex Element of K10( the carrier of V);

existence

ex b

( b

proof end;

theorem :: CONVEX1:17

for V being non empty RealUnitarySpace-like UNITSTR

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds

M is convex

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds

M is convex

proof end;

theorem :: CONVEX1:18

for V being non empty RealUnitarySpace-like UNITSTR

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds

M is convex

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds

M is convex

proof end;

theorem :: CONVEX1:19

for V being non empty RealUnitarySpace-like UNITSTR

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds

M is convex

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds

M is convex

proof end;

theorem :: CONVEX1:20

for V being non empty RealUnitarySpace-like UNITSTR

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds

M is convex

for M being Subset of V

for v being VECTOR of V

for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds

M is convex

proof end;

begin

definition

let V be RealLinearSpace;

let L be Linear_Combination of V;

attr L is convex means :Def3: :: CONVEX1:def 3

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;
let L be Linear_Combination of V;

attr L is convex means :Def3: :: CONVEX1:def 3

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

:: deftheorem Def3 defines convex CONVEX1:def 3 :

for V being RealLinearSpace

for L being Linear_Combination of V holds

( L is convex 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 Th21: :: CONVEX1:21

for V being RealLinearSpace

for L being Linear_Combination of V st L is convex holds

Carrier L <> {}

for L being Linear_Combination of V st L is convex holds

Carrier L <> {}

proof end;

theorem :: CONVEX1:22

for V being RealLinearSpace

for L being Linear_Combination of V

for v being VECTOR of V st L is convex & 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 convex & L . v <= 0 holds

not v in Carrier L

proof end;

theorem :: CONVEX1:23

proof end;

Lm11: for V being RealLinearSpace

for v being VECTOR of V

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

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

proof end;

Lm12: for V being RealLinearSpace

for v1, v2 being VECTOR of V

for L being Linear_Combination of V st L is convex & 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;

Lm13: for p being FinSequence

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds

p = <*z,y,x*>

proof end;

Lm14: for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds

Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

proof end;

Lm15: for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

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

proof end;

theorem :: CONVEX1:24

for V being RealLinearSpace

for v being VECTOR of V

for L being Linear_Combination of {v} st L is convex 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 convex holds

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

proof end;

theorem :: CONVEX1: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 convex 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 convex holds

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

proof end;

theorem :: CONVEX1:26

for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds

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

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds

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

proof end;

theorem :: CONVEX1:27

for V being RealLinearSpace

for v being VECTOR of V

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

L . v = 1 by Lm11;

for v being VECTOR of V

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

L . v = 1 by Lm11;

theorem :: CONVEX1:28

for V being RealLinearSpace

for v1, v2 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds

( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by Lm12;

for v1, v2 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds

( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by Lm12;

theorem :: CONVEX1:29

for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) by Lm15;

for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) by Lm15;

begin

definition

let V be non empty RLSStruct ;

let M be Subset of V;

func Convex-Family M -> Subset-Family of V means :Def4: :: CONVEX1:def 4

for N being Subset of V holds

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

existence

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

for N being Subset of V holds

( N in b_{1} iff ( N is convex & 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 convex & M c= N ) ) ) & ( for N being Subset of V holds

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

b_{1} = b_{2}

end;
let M be Subset of V;

func Convex-Family M -> Subset-Family of V means :Def4: :: CONVEX1:def 4

for N being Subset of V holds

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

existence

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 Def4 defines Convex-Family CONVEX1:def 4 :

for V being non empty RLSStruct

for M being Subset of V

for b

( b

( N in b

definition

let V be non empty RLSStruct ;

let M be Subset of V;

func conv M -> convex Subset of V equals :: CONVEX1:def 5

meet (Convex-Family M);

coherence

meet (Convex-Family M) is convex Subset of V

end;
let M be Subset of V;

func conv M -> convex Subset of V equals :: CONVEX1:def 5

meet (Convex-Family M);

coherence

meet (Convex-Family M) is convex Subset of V

proof end;

:: deftheorem defines conv CONVEX1:def 5 :

for V being non empty RLSStruct

for M being Subset of V holds conv M = meet (Convex-Family M);

theorem :: CONVEX1:30

for V being non empty RLSStruct

for M being Subset of V

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

conv M c= N

for M being Subset of V

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

conv M c= N

proof end;

begin

theorem :: CONVEX1:31

for p being FinSequence

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds

p = <*z,y,x*> by Lm13;

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds

p = <*z,y,x*> by Lm13;

theorem :: CONVEX1:32

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V holds 1 * M = M by Lm1;

for M being Subset of V holds 1 * M = M by Lm1;

theorem :: CONVEX1:33

for V being non empty RLSStruct

for M being empty Subset of V

for r being Real holds r * M = {} by Lm7;

for M being empty Subset of V

for r being Real holds r * M = {} by Lm7;

theorem :: CONVEX1:34

theorem :: CONVEX1:35

for V being non empty right_zeroed addLoopStr

for M being Subset of V holds M + {(0. V)} = M by Lm9;

for M being Subset of V holds M + {(0. V)} = M by Lm9;

theorem :: CONVEX1:36

for V being non empty add-associative addLoopStr

for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3;

for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3;

theorem :: CONVEX1:37

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M being Subset of V

for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M by Lm4;

for M being Subset of V

for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M by Lm4;

theorem :: CONVEX1:38

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for M1, M2 being Subset of V

for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5;

for M1, M2 being Subset of V

for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5;

theorem :: CONVEX1:39

for V being non empty RLSStruct

for M, N being Subset of V

for r being Real st M c= N holds

r * M c= r * N by Lm6;

for M, N being Subset of V

for r being Real st M c= N holds

r * M c= r * N by Lm6;

theorem :: CONVEX1:40

for V being non empty addLoopStr

for M being empty Subset of V

for N being Subset of V holds M + N = {} by Lm8;

for M being empty Subset of V

for N being Subset of V holds M + N = {} by Lm8;

begin

registration

let V be non empty RLSStruct ;

let M, N be convex Subset of V;

cluster M /\ N -> convex Subset of V;

coherence

for b_{1} being Subset of V st b_{1} = M /\ N holds

b_{1} is convex

end;
let M, N be convex Subset of V;

cluster M /\ N -> convex Subset of V;

coherence

for b

b

proof end;

registration

let V be RealLinearSpace;

let M be Subset of V;

cluster Convex-Family M -> non empty ;

coherence

not Convex-Family M is empty

end;
let M be Subset of V;

cluster Convex-Family M -> non empty ;

coherence

not Convex-Family M is empty

proof end;

theorem :: CONVEX1:41

proof end;