let X be LinearTopSpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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 Th56;
then reconsider V = U /\ (- U) as a_neighborhood of 0. X by CONNSP_2:4;
take
V
; :: thesis: ( V is circled & V is convex & V c= U )
A2:
- U is convex
by A1, CONVEX1:1;
thus
V is circled
:: thesis: ( V is convex & V c= U )proof
let r be
Real;
:: according to RLTOPSP1:def 6 :: thesis: ( abs r <= 1 implies r * V c= V )
assume A3:
abs r <= 1
;
:: thesis: r * V c= V
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in r * V or u in V )
assume
u in r * V
;
:: thesis: u in V
then consider v being
Point of
X such that A4:
u = r * v
and A5:
v in V
;
A6:
v in - U
by A5, XBOOLE_0:def 4;
A7:
v in U
by A5, XBOOLE_0:def 4;
0. X in V
by CONNSP_2:6;
then A8:
0. X in - U
by XBOOLE_0:def 4;
A9:
0. X in U
by CONNSP_2:6;
per cases
( r < 0 or r >= 0 )
;
suppose A10:
r < 0
;
:: thesis: u in Vthen A11:
- r <= 1
by A3, ABSVALUE:def 1;
((- r) * v) + ((1 - (- r)) * (0. X)) in - U
by A2, A6, A8, A11, Def1, A10;
then
((- r) * v) + (0. X) in - U
by RLVECT_1:23;
then
(- r) * v in - U
by RLVECT_1:def 7;
then consider u' being
Point of
X such that A13:
(- r) * v = (- 1) * u'
and A14:
u' in U
;
A15:
u' =
((- 1) * (- 1)) * u'
by RLVECT_1:def 9
.=
(- 1) * ((- 1) * u')
by RLVECT_1:def 9
.=
((- r) * (- 1)) * v
by A13, RLVECT_1:def 9
.=
r * v
;
((- r) * v) + ((1 - (- r)) * (0. X)) in U
by A1, A7, A9, A11, A10, Def1;
then
((- r) * v) + (0. X) in U
by RLVECT_1:23;
then
(- r) * v in U
by RLVECT_1:def 7;
then
(- 1) * (((- 1) * r) * v) in (- 1) * U
;
then
((- 1) * ((- 1) * r)) * v in (- 1) * U
by RLVECT_1:def 9;
hence
u in V
by A4, A14, A15, XBOOLE_0:def 4;
:: thesis: verum end; suppose A16:
r >= 0
;
:: thesis: u in VA17:
r <= 1
by A3, ABSVALUE:def 1;
then
(r * v) + ((1 - r) * (0. X)) in U
by A1, A7, A9, A16, Def1;
then
(r * v) + (0. X) in U
by RLVECT_1:23;
then A18:
r * v in U
by RLVECT_1:def 7;
(r * v) + ((1 - r) * (0. X)) in - U
by A2, A6, A8, A16, A17, Def1;
then
(r * v) + (0. X) in - U
by RLVECT_1:23;
then
r * v in - U
by RLVECT_1:def 7;
hence
u in V
by A4, A18, XBOOLE_0:def 4;
:: thesis: verum end;
end;
thus
V is convex
by A1, A2; :: thesis: V c= U
thus
V c= U
by XBOOLE_1:17; :: thesis: verum