let X be non empty Hausdorff TopSpace; :: thesis: 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; :: thesis: ( 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 )
; :: thesis: X | E is open
A2:
[#] (X | E) = E
by PRE_TOPC:29;
Int E = E
proof
thus
Int E c= E
by TOPS_1:44;
:: according to XBOOLE_0:def 10 :: thesis: E c= Int E
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in E or a in Int E )
assume A3:
a in E
;
:: thesis: a in Int E
then reconsider x =
a as
Point of
X ;
reconsider xx =
x as
Point of
(X | E) by A3, PRE_TOPC:29;
consider K being
a_neighborhood of
xx such that A4:
K is
compact
by A1, Def6;
A5:
xx in Int K
by CONNSP_2:def 1;
set UE =
{ G where G is Subset of X : ( G is open & G c= E ) } ;
Int K in the
topology of
(X | E)
by PRE_TOPC:def 5;
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 9;
A8:
G is
open
by A6, PRE_TOPC:def 5;
A9:
Int K c= G
by A7, XBOOLE_1:17;
E is
dense
by A1, A2, TEX_3:def 1;
then A11:
Cl (G /\ E) = Cl G
by A8, TOPS_1:81;
A12:
K c= [#] (X | E)
;
reconsider KK =
K as
Subset of
X by A2, XBOOLE_1:1;
for
P being
Subset of
(X | E) st
P = KK holds
P is
compact
by A4;
then
KK is
compact
by A12, COMPTS_1:11;
then A13:
Cl (G /\ E) c= KK
by A7, TOPS_1:44, TOPS_1:31;
G c= Cl G
by PRE_TOPC:48;
then
G c= K
by A11, A13, XBOOLE_1:1;
then
G c= E
by A2, XBOOLE_1:1;
then
G in { G where G is Subset of X : ( G is open & G c= E ) }
by A8;
then
a in union { G where G is Subset of X : ( G is open & G c= E ) }
by A5, A9, TARSKI:def 4;
hence
a in Int E
by TEX_4:4;
:: thesis: verum
end;
hence
X | E is open
by A2, TSEP_1:16; :: thesis: verum