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