let X be LinearTopSpace; for U being a_neighborhood of 0. X st U is convex holds
ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
let U be a_neighborhood of 0. X; ( U is convex implies ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U ) )
assume A1:
U is convex
; ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
set V = U /\ (- U);
- U is a_neighborhood of 0. X
by Th55;
then reconsider V = U /\ (- U) as a_neighborhood of 0. X by CONNSP_2:2;
take
V
; ( V is circled & V is convex & V c= U )
A2:
- U is convex
by A1, CONVEX1:1;
thus
V is circled
( V is convex & V c= U )proof
0. X in V
by CONNSP_2:4;
then A3:
0. X in - U
by XBOOLE_0:def 4;
A4:
0. X in U
by CONNSP_2:4;
let r be
Real;
RLTOPSP1:def 6 ( |.r.| <= 1 implies r * V c= V )
assume A5:
|.r.| <= 1
;
r * V c= V
let u be
object ;
TARSKI:def 3 ( not u in r * V or u in V )
assume
u in r * V
;
u in V
then consider v being
Point of
X such that A6:
u = r * v
and A7:
v in V
;
A8:
v in - U
by A7, XBOOLE_0:def 4;
A9:
v in U
by A7, XBOOLE_0:def 4;
per cases
( r < 0 or r >= 0 )
;
suppose A10:
r < 0
;
u in Vthen A11:
- r <= 1
by A5, ABSVALUE:def 1;
then
((- r) * v) + ((1 - (- r)) * (0. X)) in - U
by A2, A8, A3, A10;
then
((- r) * v) + (0. X) in - U
;
then
(- r) * v in - U
;
then consider u9 being
Point of
X such that A12:
(- r) * v = (- 1) * u9
and A13:
u9 in U
;
((- r) * v) + ((1 - (- r)) * (0. X)) in U
by A1, A9, A4, A10, A11;
then
((- r) * v) + (0. X) in U
;
then
(- r) * v in U
;
then
(- 1) * (((- 1) * r) * v) in (- 1) * U
;
then A14:
((- 1) * ((- 1) * r)) * v in (- 1) * U
by RLVECT_1:def 7;
u9 =
((- 1) * (- 1)) * u9
by RLVECT_1:def 8
.=
(- 1) * ((- 1) * u9)
by RLVECT_1:def 7
.=
((- r) * (- 1)) * v
by A12, RLVECT_1:def 7
.=
r * v
;
hence
u in V
by A6, A13, A14, XBOOLE_0:def 4;
verum end; suppose A15:
r >= 0
;
u in VA16:
r <= 1
by A5, ABSVALUE:def 1;
then
(r * v) + ((1 - r) * (0. X)) in - U
by A2, A8, A3, A15;
then
(r * v) + (0. X) in - U
;
then A17:
r * v in - U
;
(r * v) + ((1 - r) * (0. X)) in U
by A1, A9, A4, A15, A16;
then
(r * v) + (0. X) in U
;
then
r * v in U
;
hence
u in V
by A6, A17, XBOOLE_0:def 4;
verum end;
end;
thus
V is convex
by A1, A2; V c= U
thus
V c= U
by XBOOLE_1:17; verum