let G be TopologicalGroup; 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 =
1_ G;
take
1_ G
;
for A being Subset of G st A is open & 1_ G in A holds
ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
let A be
Subset of
G;
( A is open & 1_ G in A implies ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A ) )
assume
(
A is
open &
1_ G in A )
;
ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
then
1_ G in Int A
by TOPS_1:23;
then A1:
A is
a_neighborhood of
1_ G
by CONNSP_2:def 1;
1_ G = (1_ G) * ((1_ G) ")
by GROUP_1:def 5;
then consider C being
open a_neighborhood of
1_ G,
B being
open a_neighborhood of
(1_ G) " such that A2:
C * B c= A
by A1, Th36;
((1_ G) ") " = 1_ G
;
then
B " is
a_neighborhood of
1_ G
by Th53;
then reconsider W =
C /\ (B ") as
a_neighborhood of
1_ G by CONNSP_2:2;
W c= B "
by XBOOLE_1:17;
then
W " c= (B ") "
by Th8;
then
C * (W ") c= C * B
by Th4;
then A3:
C * (W ") c= A
by A2;
take
W
;
( 1_ G in W & W is open & Cl W c= A )
Int W = W
by TOPS_1:23;
hence A4:
(
1_ 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 * (1_ G)
by GROUP_1:def 4;
then
p in r * W
by A4, GROUP_2:27;
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, GROUP_2:27;
A11:
(
W c= C &
b " in W " )
by A10, XBOOLE_1:17;
r =
r * (1_ G)
by GROUP_1:def 4
.=
r * (b * (b "))
by GROUP_1:def 5
.=
a * (b ")
by A9, GROUP_1:def 3
;
then
p in C * (W ")
by A7, A11;
hence
p in A
by A3;
verum
end;
hence
G is regular
by Th35; verum