let X, Y 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 Def2;
now ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= Gper 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 Th14;
then
Base-Appr G is
Cover of
[:A,{t}:]
by SETFAM_1:def 11;
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 Th22;
reconsider PK =
(Pr1 (X,Y)) .: K as
Subset-Family of
X ;
K is
open
by A4, TOPS_2:11;
then A7:
(Pr1 (X,Y)) .: K is
open
by Th19;
PK is
Cover of
A
by A5, Th21;
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 4;
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, Th23;
reconsider F =
(Pr1 (X,Y)) .: N as
Subset-Family of
X ;
A14:
N is
Cover of
[:A,{t}:]
proof
let e1,
e2 be
object ;
RELAT_1:def 3,
SETFAM_1:def 11 ( not [e1,e2] in [:A,{t}:] or [e1,e2] in union N )
A15:
A c= union M
by A9, SETFAM_1:def 11;
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]
;
[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:65;
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
object 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:8;
then
[e1,e2] `1 in X2
by A18, A21, A22, EQREL_1:50;
then
[e1,e2] in [:X2,Y2:]
by A25, A17, ZFMISC_1:87;
hence
[e1,e2] in union N
by A20, A22, TARSKI:def 4;
verum
end; then
F is
Cover of
A
by Th21;
then A26:
A c= union F
by SETFAM_1:def 11;
reconsider H =
(Pr2 (X,Y)) .: N as
Subset-Family of
Y ;
A27:
now for C being set st C in H holds
t in Clet 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 Th17;
D meets [:A,{t}:]
by A6, A11, A28;
then
D /\ [:A,{t}:] <> {}
;
then consider x being
Point of
[:X,Y:] such that A30:
x in D /\ [:A,{t}:]
;
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 5;
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:21;
x in D
by A30, XBOOLE_0:def 4;
hence
t in C
by A2, A29, A33, A32, FUNCT_2:35;
verum end;
[:A,{t}:] c= union N
by A14, SETFAM_1:def 11;
then
N <> {}
by A3, ZFMISC_1:2;
then
H <> {}
by Th20;
then A34:
t in meet H
by A27, SETFAM_1:def 1;
A35:
N c= Base-Appr G
by A4, A11;
then A36:
N is
open
by TOPS_2:11;
then
meet H is
open
by A12, Th19, TOPS_2:20;
then
t in Int (meet H)
by A34, TOPS_1:23;
then reconsider W =
meet H as
a_neighborhood of
t by CONNSP_2:def 1;
union F is
open
by A36, Th19, TOPS_2:19;
then
A c= Int (union F)
by A26, TOPS_1:23;
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 Th15;
verum end;
hence
ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
; verum