let G be TopologicaladdGroup; G is regular
ex p being Point of G st
for A being Subset of G st A is open & p in A holds
ex B being Subset of G st
( p in B & B is open & Cl B c= A )
proof
set e =
0_ G;
take
0_ G
;
for A being Subset of G st A is open & 0_ G in A holds
ex B being Subset of G st
( 0_ G in B & B is open & Cl B c= A )
let A be
Subset of
G;
( A is open & 0_ G in A implies ex B being Subset of G st
( 0_ G in B & B is open & Cl B c= A ) )
assume
(
A is
open &
0_ G in A )
;
ex B being Subset of G st
( 0_ G in B & B is open & Cl B c= A )
then
0_ G in Int A
by TOPS_1:23;
then A1:
A is
a_neighborhood of
0_ G
by CONNSP_2:def 1;
0_ G = (0_ G) + (- (0_ G))
by Def5;
then consider C being
open a_neighborhood of
0_ G,
B being
open a_neighborhood of
- (0_ G) such that A2:
C + B c= A
by A1, Th36;
- (- (0_ G)) = 0_ G
;
then
- B is
a_neighborhood of
0_ G
by Th53;
then reconsider W =
C /\ (- B) as
a_neighborhood of
0_ G by CONNSP_2:2;
- W c= - (- B)
by ThB8, XBOOLE_1:17;
then A3:
C + (- W) c= C + B
by Th4;
take
W
;
( 0_ G in W & W is open & Cl W c= A )
A4:
Int W = W
by TOPS_1:23;
hence
(
0_ G in W &
W is
open )
by CONNSP_2:def 1;
Cl W c= A
let p be
object ;
TARSKI:def 3 ( not p in Cl W or p in A )
assume A5:
p in Cl W
;
p in A
then reconsider r =
p as
Point of
G ;
r = r + (0_ G)
by Def4;
then
p in r + W
by A4, CONNSP_2:def 1, Th27;
then
r + W meets W
by A5, PRE_TOPC:def 7;
then consider a being
object such that A6:
a in (r + W) /\ W
by XBOOLE_0:4;
A7:
a in W
by A6, XBOOLE_0:def 4;
A8:
a in r + W
by A6, XBOOLE_0:def 4;
reconsider a =
a as
Point of
G by A6;
consider b being
Element of
G such that A9:
a = r + b
and A10:
b in W
by A8, Th27;
A11:
(
W c= C &
- b in - W )
by A10, XBOOLE_1:17;
r =
r + (0_ G)
by Def4
.=
r + (b + (- b))
by Def5
.=
a + (- b)
by A9, RLVECT_1:def 3
;
then
p in C + (- W)
by A7, A11;
hence
p in A
by A2, A3;
verum
end;
hence
G is regular
by TOPGRP_1:36; verum