let V be non empty ComplexUnitarySpace-like CUNITSTR ; 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; 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; 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; ( 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 }
; M is convex
let x, y be VECTOR of V; CONVEX4:def 23 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; ( 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
and
A4:
y in M
; (s * x) + ((1r - s) * y) in M
A5:
ex u2 being VECTOR of V st
( y = u2 & Re (u2 .|. v) > r )
by A1, A4;
consider p being Real such that
A6:
s = p
and
A7:
0 < p
and
A8:
p < 1
by A2;
1 - p > 0
by A8, XREAL_1:50;
then A9:
(1 - p) * (Re (y .|. v)) > (1 - p) * r
by A5, XREAL_1:68;
ex u1 being VECTOR of V st
( x = u1 & Re (u1 .|. v) > r )
by A1, A3;
then
p * (Re (x .|. v)) > p * r
by A7, XREAL_1:68;
then A10:
(p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) > (p * r) + ((1 - p) * r)
by A9, XREAL_1:8;
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:8
.=
(p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v)))
by A6, Th42
.=
(p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v)))
by A6, Th42
;
hence
(s * x) + ((1r - s) * y) in M
by A1, A10; verum