let X, Y be RealNormSpace; for x being Point of X
for r being Real
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let x be Point of X; for r being Real
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let r be Real; for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let T be LinearOperator of X,Y; for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let V be Subset of (LinearTopSpaceNorm Y); ( V = T .: (Ball (x,r)) implies V is convex )
reconsider V1 = T .: (Ball (x,r)) as Subset of Y ;
A1:
for u, v being Point of Y
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
proof
reconsider Bxr =
Ball (
x,
r) as
Subset of
(LinearTopSpaceNorm X) by NORMSP_2:def 4;
let u,
v be
Point of
Y;
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1let s be
Real;
( 0 < s & s < 1 & u in V1 & v in V1 implies (s * u) + ((1 - s) * v) in V1 )
assume that A2:
(
0 < s &
s < 1 )
and A3:
u in V1
and A4:
v in V1
;
(s * u) + ((1 - s) * v) in V1
consider z1 being
object such that A5:
z1 in the
carrier of
X
and A6:
z1 in Ball (
x,
r)
and A7:
u = T . z1
by A3, FUNCT_2:64;
reconsider zz1 =
z1 as
Point of
X by A5;
reconsider za1 =
zz1 as
Point of
(LinearTopSpaceNorm X) by NORMSP_2:def 4;
consider z2 being
object such that A8:
z2 in the
carrier of
X
and A9:
z2 in Ball (
x,
r)
and A10:
v = T . z2
by A4, FUNCT_2:64;
reconsider zz2 =
z2 as
Point of
X by A8;
A11:
(1 - s) * v = T . ((1 - s) * zz2)
by A10, LOPBAN_1:def 5;
reconsider za2 =
zz2 as
Point of
(LinearTopSpaceNorm X) by NORMSP_2:def 4;
(
s * za1 = s * zz1 &
(1 - s) * za2 = (1 - s) * zz2 )
by NORMSP_2:def 4;
then A12:
(s * za1) + ((1 - s) * za2) = (s * zz1) + ((1 - s) * zz2)
by NORMSP_2:def 4;
s * u = T . (s * zz1)
by A7, LOPBAN_1:def 5;
then A13:
(s * u) + ((1 - s) * v) = T . ((s * zz1) + ((1 - s) * zz2))
by A11, VECTSP_1:def 20;
Bxr is
convex
by Th12;
then
(s * za1) + ((1 - s) * za2) in Bxr
by A2, A6, A9;
hence
(s * u) + ((1 - s) * v) in V1
by A12, A13, FUNCT_2:35;
verum
end;
assume A14:
V = T .: (Ball (x,r))
; V is convex
for u, v being Point of (LinearTopSpaceNorm Y)
for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
hence
V is convex
; verum