let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds

V is convex

let V be Subset of (LinearTopSpaceNorm Y); :: thesis: ( 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

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

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; :: thesis: 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; :: thesis: 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; :: thesis: for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds

V is convex

let V be Subset of (LinearTopSpaceNorm Y); :: thesis: ( 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

assume A14:
V = T .: (Ball (x,r))
; :: thesis: V is convex
reconsider Bxr = Ball (x,r) as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

let u, v be Point of Y; :: thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds

(s * u) + ((1 - s) * v) in V1

let s be Real; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

end;let u, v be Point of Y; :: thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds

(s * u) + ((1 - s) * v) in V1

let s be Real; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

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

proof

hence
V is convex
; :: thesis: verum
let u, v be Point of (LinearTopSpaceNorm Y); :: thesis: for s being Real st 0 < s & s < 1 & u in V & v in V holds

(s * u) + ((1 - s) * v) in V

let s be Real; :: thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )

reconsider u1 = u as Point of Y by NORMSP_2:def 4;

reconsider v1 = v as Point of Y by NORMSP_2:def 4;

( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def 4;

then A15: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def 4;

assume ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (s * u) + ((1 - s) * v) in V

hence (s * u) + ((1 - s) * v) in V by A14, A1, A15; :: thesis: verum

end;(s * u) + ((1 - s) * v) in V

let s be Real; :: thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )

reconsider u1 = u as Point of Y by NORMSP_2:def 4;

reconsider v1 = v as Point of Y by NORMSP_2:def 4;

( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def 4;

then A15: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def 4;

assume ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (s * u) + ((1 - s) * v) in V

hence (s * u) + ((1 - s) * v) in V by A14, A1, A15; :: thesis: verum