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 : Im (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 : Im (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 : Im (u .|. v) <= r } holds
M is convex
let r be Real; ( M = { u where u is VECTOR of V : Im (u .|. v) <= r } implies M is convex )
assume A1:
M = { u where u is VECTOR of V : Im (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 & Im (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) * (Im (y .|. v)) <= (1 - p) * r
by A5, XREAL_1:64;
ex u1 being VECTOR of V st
( x = u1 & Im (u1 .|. v) <= r )
by A1, A3;
then
p * (Im (x .|. v)) <= p * r
by A7, XREAL_1:64;
then A10:
(p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) <= (p * r) + ((1 - p) * r)
by A9, XREAL_1:7;
Im (((s * x) + ((1r - s) * y)) .|. v) =
Im (((s * x) .|. v) + (((1r - s) * y) .|. v))
by CSSPACE:def 13
.=
Im ((s * (x .|. v)) + (((1r - s) * y) .|. v))
by CSSPACE:def 13
.=
Im ((s * (x .|. v)) + ((1r - s) * (y .|. v)))
by CSSPACE:def 13
.=
(Im (s * (x .|. v))) + (Im ((1r - s) * (y .|. v)))
by COMPLEX1:8
.=
(p * (Im (x .|. v))) + (Im ((1r - s) * (y .|. v)))
by A6, Th43
.=
(p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v)))
by A6, Th43
;
hence
(s * x) + ((1r - s) * y) in M
by A1, A10; verum