let V be non empty ComplexUnitarySpace-like CUNITSTR ; :: thesis: 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 : Re (u .|. v) >= r } holds
M is convex
let M be Subset of V; :: thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds
M is convex
let v be VECTOR of V; :: thesis: for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds
M is convex
let r be Real; :: thesis: ( M = { u where u is VECTOR of V : Re (u .|. v) >= r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : Re (u .|. v) >= r } ; :: thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & x in M & y in M holds
(z * x) + ((1r - z) * y) in M
let s be Complex; :: thesis: ( ex r being Real st
( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M )
assume that
A2: ex p being Real st
( s = p & 0 < p & p < 1 ) and
A3: ( x in M & y in M ) ; :: thesis: (s * x) + ((1r - s) * y) in M
consider p being Real such that
A4: ( s = p & 0 < p & p < 1 ) by A2;
ex u1 being VECTOR of V st
( x = u1 & Re (u1 .|. v) >= r ) by A1, A3;
then A8: p * (Re (x .|. v)) >= p * r by A4, XREAL_1:66;
A6: ex u2 being VECTOR of V st
( y = u2 & Re (u2 .|. v) >= r ) by A1, A3;
A7: Re (((s * x) + ((1r - s) * y)) .|. v) = Re (((s * x) .|. v) + (((1r - s) * y) .|. v)) by CSSPACE:def 13
.= Re ((s * (x .|. v)) + (((1r - s) * y) .|. v)) by CSSPACE:def 13
.= Re ((s * (x .|. v)) + ((1r - s) * (y .|. v))) by CSSPACE:def 13
.= (Re (s * (x .|. v))) + (Re ((1r - s) * (y .|. v))) by COMPLEX1:19
.= (p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v))) by A4, Th101
.= (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) by A4, Th101 ;
1 - p > 0 by A4, XREAL_1:52;
then (1 - p) * (Re (y .|. v)) >= (1 - p) * r by A6, XREAL_1:66;
then (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) >= (p * r) + ((1 - p) * r) by A8, XREAL_1:9;
hence (s * x) + ((1r - s) * y) in M by A1, A7; :: thesis: verum