let X be non empty Hausdorff TopSpace; for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open
let E be non empty Subset of X; ( X | E is dense & X | E is locally-compact implies X | E is open )
assume A1:
( X | E is dense & X | E is locally-compact )
; X | E is open
A2:
[#] (X | E) = E
by PRE_TOPC:8;
Int E = E
proof
thus
Int E c= E
by TOPS_1:16;
XBOOLE_0:def 10 E c= Int E
let a be
object ;
TARSKI:def 3 ( not a in E or a in Int E )
assume A3:
a in E
;
a in Int E
then reconsider x =
a as
Point of
X ;
reconsider xx =
x as
Point of
(X | E) by A3, PRE_TOPC:8;
set UE =
{ G where G is Subset of X : ( G is open & G c= E ) } ;
consider K being
a_neighborhood of
xx such that A4:
K is
compact
by A1;
reconsider KK =
K as
Subset of
X by A2, XBOOLE_1:1;
A5:
K c= [#] (X | E)
;
Int K in the
topology of
(X | E)
by PRE_TOPC:def 2;
then consider G being
Subset of
X such that A6:
G in the
topology of
X
and A7:
Int K = G /\ E
by A2, PRE_TOPC:def 4;
A8:
G is
open
by A6;
for
P being
Subset of
(X | E) st
P = KK holds
P is
compact
by A4;
then
KK is
compact
by A5, COMPTS_1:2;
then A9:
Cl (G /\ E) c= KK
by A7, TOPS_1:5, TOPS_1:16;
E is
dense
by A1, A2, TEX_3:def 1;
then A10:
Cl (G /\ E) = Cl G
by A8, TOPS_1:46;
G c= Cl G
by PRE_TOPC:18;
then
G c= K
by A10, A9;
then
G c= E
by A2, XBOOLE_1:1;
then A11:
G in { G where G is Subset of X : ( G is open & G c= E ) }
by A8;
A12:
xx in Int K
by CONNSP_2:def 1;
Int K c= G
by A7, XBOOLE_1:17;
then
a in union { G where G is Subset of X : ( G is open & G c= E ) }
by A12, A11, TARSKI:def 4;
hence
a in Int E
by TEX_4:3;
verum
end;
hence
X | E is open
by A2, TSEP_1:16; verum