let Y, X be non empty TopSpace; for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let t be Point of Y; for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let A be Subset of X; ( A is compact implies for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G )
assume A1:
A is compact
; for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let G be a_neighborhood of [:A,{t}:]; ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
A2:
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:]
by Def5;
now per cases
( A <> {} X or A = {} X )
;
suppose A3:
A <> {} X
;
ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
[:A,{t}:] c= Int G
by CONNSP_2:def 2;
then
[:A,{t}:] c= union (Base-Appr G)
by Th55;
then
Base-Appr G is
Cover of
[:A,{t}:]
by SETFAM_1:def 12;
then consider K being
Subset-Family of
[:X,Y:] such that A4:
K c= Base-Appr G
and A5:
K is
Cover of
[:A,{t}:]
and A6:
for
c being
set st
c in K holds
c meets [:A,{t}:]
by Th63;
reconsider PK =
(Pr1 X,Y) .: K as
Subset-Family of
X ;
K is
open
by A4, Th51, TOPS_2:18;
then A7:
(Pr1 X,Y) .: K is
open
by Th60;
PK is
Cover of
A
by A5, Th62;
then consider M being
Subset-Family of
X such that A8:
M c= (Pr1 X,Y) .: K
and A9:
M is
Cover of
A
and A10:
M is
finite
by A1, A7, COMPTS_1:def 7;
consider N being
Subset-Family of
[:X,Y:] such that A11:
N c= K
and A12:
N is
finite
and A13:
(Pr1 X,Y) .: N = M
by A8, A10, Th64;
reconsider F =
(Pr1 X,Y) .: N as
Subset-Family of
X ;
A14:
N is
Cover of
[:A,{t}:]
proof
let e1,
e2 be
set ;
RELAT_1:def 3,
SETFAM_1:def 12 ( not [e1,e2] in [:A,{t}:] or [e1,e2] in union N )
A15:
A c= union M
by A9, SETFAM_1:def 12;
assume A16:
[e1,e2] in [:A,{t}:]
;
[e1,e2] in union N
then
[e1,e2] `2 in {t}
by MCART_1:10;
then
[e1,e2] `2 = t
by TARSKI:def 1;
then A17:
[e1,e2] = [([e1,e2] `1 ),t]
by A16, MCART_1:23;
[e1,e2] `1 in A
by A16, MCART_1:10;
then consider X1 being
set such that A18:
[e1,e2] `1 in X1
and A19:
X1 in M
by A15, TARSKI:def 4;
consider XY being
Subset of
[:X,Y:] such that A20:
XY in N
and A21:
(Pr1 X,Y) . XY = X1
by A13, A19, FUNCT_2:116;
XY in K
by A11, A20;
then
XY in Base-Appr G
by A4;
then consider X2 being
Subset of
X,
Y2 being
Subset of
Y such that A22:
XY = [:X2,Y2:]
and
[:X2,Y2:] c= G
and
X2 is
open
and
Y2 is
open
;
XY meets [:A,{t}:]
by A6, A11, A20;
then consider xy being
set such that A23:
xy in XY
and A24:
xy in [:A,{t}:]
by XBOOLE_0:3;
xy `2 in {t}
by A24, MCART_1:10;
then
xy `2 = t
by TARSKI:def 1;
then A25:
t in Y2
by A22, A23, MCART_1:10;
XY <> {}
by A18, A21, FUNCT_3:9;
then
[e1,e2] `1 in X2
by A18, A21, A22, Th13;
then
[e1,e2] in [:X2,Y2:]
by A25, A17, ZFMISC_1:106;
hence
[e1,e2] in union N
by A20, A22, TARSKI:def 4;
verum
end; then
F is
Cover of
A
by Th62;
then A26:
A c= union F
by SETFAM_1:def 12;
reconsider H =
(Pr2 X,Y) .: N as
Subset-Family of
Y ;
A27:
now let C be
set ;
( C in H implies t in C )assume
C in H
;
t in Cthen consider D being
Subset of
[:X,Y:] such that A28:
D in N
and A29:
C = (pr2 the carrier of X,the carrier of Y) .: D
by Th58;
D meets [:A,{t}:]
by A6, A11, A28;
then
D /\ [:A,{t}:] <> {}
by XBOOLE_0:def 7;
then consider x being
Point of
[:X,Y:] such that A30:
x in D /\ [:A,{t}:]
by SUBSET_1:10;
A31:
x in [:A,{t}:]
by A30, XBOOLE_0:def 4;
then
x `1 in A
by MCART_1:10;
then A32:
(pr2 the carrier of X,the carrier of Y) . (x `1 ),
t = t
by FUNCT_3:def 6;
x `2 in {t}
by A31, MCART_1:10;
then
x `2 = t
by TARSKI:def 1;
then A33:
x = [(x `1 ),t]
by A2, MCART_1:23;
x in D
by A30, XBOOLE_0:def 4;
hence
t in C
by A2, A29, A33, A32, FUNCT_2:43;
verum end;
[:A,{t}:] c= union N
by A14, SETFAM_1:def 12;
then
N <> {}
by A3, ZFMISC_1:2;
then
H <> {}
by Th61;
then A34:
t in meet H
by A27, SETFAM_1:def 1;
A35:
N c= Base-Appr G
by A4, A11, XBOOLE_1:1;
then A36:
N is
open
by Th51, TOPS_2:18;
then
meet H is
open
by A12, Th60, TOPS_2:27;
then
t in Int (meet H)
by A34, TOPS_1:55;
then reconsider W =
meet H as
a_neighborhood of
t by CONNSP_2:def 1;
union F is
open
by A36, Th60, TOPS_2:26;
then
A c= Int (union F)
by A26, TOPS_1:55;
then reconsider V =
union F as
a_neighborhood of
A by CONNSP_2:def 2;
take V =
V;
ex W being a_neighborhood of t st [:V,W:] c= Gtake W =
W;
[:V,W:] c= Ghence
[:V,W:] c= G
by Th56;
verum end;
hence
ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
; verum