let X be LinearTopSpace; :: thesis: for K being compact Subset of X
for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V
let K be compact Subset of X; :: thesis: for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V
let C be closed Subset of X; :: thesis: ( K misses C implies ex V being a_neighborhood of 0. X st K + V misses C + V )
assume A1:
K misses C
; :: thesis: ex V being a_neighborhood of 0. X st K + V misses C + V
per cases
( K = {} or K <> {} )
;
suppose A3:
K <> {}
;
:: thesis: ex V being a_neighborhood of 0. X st K + V misses C + Vset xV =
{ [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) } ;
then reconsider xV =
{ [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) } as non
empty set ;
defpred S1[
set ,
set ]
means ex
v1,
v2 being
Point of
X ex
V1,
V2 being
open a_neighborhood of
0. X st
( $1
= [v1,V1] & $2
= [v2,V2] &
v1 + V1 = v2 + V2 );
A14:
for
x being
set st
x in xV holds
S1[
x,
x]
A15:
for
x,
y being
set st
S1[
x,
y] holds
S1[
y,
x]
;
A16:
for
x,
y,
z being
set st
S1[
x,
y] &
S1[
y,
z] holds
S1[
x,
z]
proof
let x,
y,
z be
set ;
:: thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given v1,
v2 being
Point of
X,
V1,
V2 being
open a_neighborhood of
0. X such that A17:
x = [v1,V1]
and A18:
y = [v2,V2]
and A19:
v1 + V1 = v2 + V2
;
:: thesis: ( not S1[y,z] or S1[x,z] )
given w1,
w2 being
Point of
X,
W1,
W2 being
open a_neighborhood of
0. X such that A20:
y = [w1,W1]
and A21:
z = [w2,W2]
and A22:
w1 + W1 = w2 + W2
;
:: thesis: S1[x,z]
take
v1
;
:: thesis: ex v2 being Point of X ex V1, V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [v2,V2] & v1 + V1 = v2 + V2 )
take
w2
;
:: thesis: ex V1, V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take
V1
;
:: thesis: ex V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take
W2
;
:: thesis: ( x = [v1,V1] & z = [w2,W2] & v1 + V1 = w2 + W2 )
(
v2 = w1 &
V2 = W1 )
by A18, A20, ZFMISC_1:33;
hence
(
x = [v1,V1] &
z = [w2,W2] &
v1 + V1 = w2 + W2 )
by A17, A19, A21, A22;
:: thesis: verum
end; consider eqR being
Equivalence_Relation of
xV such that A23:
for
x,
y being
set holds
(
[x,y] in eqR iff (
x in xV &
y in xV &
S1[
x,
y] ) )
from EQREL_1:sch 1(A14, A15, A16);
then consider g being
Function such that A24:
dom g = Class eqR
and A25:
for
X being
set st
X in Class eqR holds
g . X in X
by WELLORD2:28;
A26:
rng g c= xV
set xVV =
rng g;
set F =
{ (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } ;
{ (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } c= bool the
carrier of
X
then reconsider F =
{ (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g } as
Subset-Family of
X ;
A28:
F is
Cover of
K
proof
let x be
set ;
:: according to TARSKI:def 3,
SETFAM_1:def 12 :: thesis: ( not x in K or x in union F )
assume A29:
x in K
;
:: thesis: x in union F
then reconsider x =
x as
Point of
X ;
consider Vx being
open a_neighborhood of
0. X such that A30:
Vx is
symmetric
and A31:
((x + Vx) + Vx) + Vx misses C
by A4, A29;
x + (0. X) in x + Vx
by Lm1, CONNSP_2:6;
then A32:
x in x + Vx
by RLVECT_1:10;
[x,Vx] in xV
by A29, A30, A31;
then A33:
Class eqR,
[x,Vx] in Class eqR
by EQREL_1:def 5;
then
g . (Class eqR,[x,Vx]) in Class eqR,
[x,Vx]
by A25;
then
[(g . (Class eqR,[x,Vx])),[x,Vx]] in eqR
by EQREL_1:27;
then consider v1,
v2 being
Point of
X,
V1,
V2 being
open a_neighborhood of
0. X such that A34:
g . (Class eqR,[x,Vx]) = [v1,V1]
and A35:
[x,Vx] = [v2,V2]
and A36:
v1 + V1 = v2 + V2
by A23;
A37:
(
x = v2 &
Vx = V2 )
by A35, ZFMISC_1:33;
g . (Class eqR,[x,Vx]) in rng g
by A24, A33, FUNCT_1:def 5;
then
x + Vx in F
by A34, A36, A37;
hence
x in union F
by A32, TARSKI:def 4;
:: thesis: verum
end;
F is
open
then consider G being
Subset-Family of
X such that A38:
G c= F
and A39:
G is
Cover of
K
and A40:
G is
finite
by A28, COMPTS_1:def 7;
A41:
for
A being
Subset of
X st
A in G holds
ex
x being
Point of
X ex
Vx being
open a_neighborhood of
0. X st
(
A = x + Vx &
[x,Vx] in rng g )
A42:
for
x being
Point of
X for
Vx being
open a_neighborhood of
0. X st
x + Vx in G &
[x,Vx] in rng g holds
(
x in K &
Vx is
symmetric &
((x + Vx) + Vx) + Vx misses C )
proof
let x be
Point of
X;
:: thesis: for Vx being open a_neighborhood of 0. X st x + Vx in G & [x,Vx] in rng g holds
( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )let Vx be
open a_neighborhood of
0. X;
:: thesis: ( x + Vx in G & [x,Vx] in rng g implies ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) )
assume that A43:
x + Vx in G
and A44:
[x,Vx] in rng g
;
:: thesis: ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
x + Vx in F
by A38, A43;
then consider v being
Point of
X,
Vv being
open a_neighborhood of
0. X such that A45:
x + Vx = v + Vv
and A46:
[v,Vv] in rng g
;
[v,Vv] in xV
by A26, A46;
then consider u being
Point of
X,
Vu being
open a_neighborhood of
0. X such that A47:
[u,Vu] = [v,Vv]
and A48:
(
u in K &
Vu is
symmetric &
((u + Vu) + Vu) + Vu misses C )
;
[[x,Vx],[v,Vv]] in eqR
by A23, A26, A44, A45, A46;
then
[x,Vx] in Class eqR,
[v,Vv]
by EQREL_1:27;
then A49:
Class eqR,
[v,Vv] = Class eqR,
[x,Vx]
by A26, A46, EQREL_1:31;
consider A being
set such that A50:
A in dom g
and A51:
[x,Vx] = g . A
by A44, FUNCT_1:def 5;
consider B being
set such that A52:
B in dom g
and A53:
[v,Vv] = g . B
by A46, FUNCT_1:def 5;
consider a being
set such that A54:
a in xV
and A55:
A = Class eqR,
a
by A24, A50, EQREL_1:def 5;
consider b being
set such that A56:
b in xV
and A57:
B = Class eqR,
b
by A24, A52, EQREL_1:def 5;
[x,Vx] in Class eqR,
a
by A24, A25, A50, A51, A55;
then A58:
Class eqR,
a = Class eqR,
[x,Vx]
by A54, EQREL_1:31;
[v,Vv] in Class eqR,
b
by A24, A25, A52, A53, A57;
then
[x,Vx] = [v,Vv]
by A49, A51, A53, A55, A56, A57, A58, EQREL_1:31;
then
(
x = v &
Vx = Vv &
v = u &
Vv = Vu )
by A47, ZFMISC_1:33;
hence
(
x in K &
Vx is
symmetric &
((x + Vx) + Vx) + Vx misses C )
by A48;
:: thesis: verum
end; set FVx =
{ Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } ;
{ Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } c= bool the
carrier of
X
then reconsider FVx =
{ Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) } as
Subset-Family of
X ;
take V =
meet FVx;
:: thesis: ( V is a_neighborhood of 0. X & K + V misses C + V )A59:
FVx is
open
then A66:
0. X in V
by A60, SETFAM_1:def 1;
defpred S2[
set ,
set ]
means ex
x being
Point of
X ex
Vx being
open a_neighborhood of
0. X st
( $1
= x + Vx &
x + Vx in G &
[x,Vx] in rng g & $2
= Vx );
A67:
for
x being
set st
x in G holds
ex
y being
set st
(
y in FVx &
S2[
x,
y] )
consider f being
Function of
G,
FVx such that A71:
for
x being
set st
x in G holds
S2[
x,
f . x]
from FUNCT_2:sch 1(A67);
A72:
dom f = G
by A60, FUNCT_2:def 1;
A73:
FVx c= rng f
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in FVx or z in rng f )
assume
z in FVx
;
:: thesis: z in rng f
then consider Vx being
open a_neighborhood of
0. X such that A74:
z = Vx
and A75:
ex
x being
Point of
X st
(
x + Vx in G &
[x,Vx] in rng g )
;
consider x being
Point of
X such that A76:
x + Vx in G
and A77:
[x,Vx] in rng g
by A75;
consider v being
Point of
X,
Vv being
open a_neighborhood of
0. X such that A78:
x + Vx = v + Vv
and
v + Vv in G
and A79:
[v,Vv] in rng g
and A80:
f . (x + Vx) = Vv
by A71, A76;
[[x,Vx],[v,Vv]] in eqR
by A23, A26, A77, A78, A79;
then
[x,Vx] in Class eqR,
[v,Vv]
by EQREL_1:27;
then A81:
Class eqR,
[v,Vv] = Class eqR,
[x,Vx]
by A26, A79, EQREL_1:31;
consider A being
set such that A82:
A in dom g
and A83:
[x,Vx] = g . A
by A77, FUNCT_1:def 5;
consider B being
set such that A84:
B in dom g
and A85:
[v,Vv] = g . B
by A79, FUNCT_1:def 5;
consider a being
set such that A86:
a in xV
and A87:
A = Class eqR,
a
by A24, A82, EQREL_1:def 5;
consider b being
set such that A88:
b in xV
and A89:
B = Class eqR,
b
by A24, A84, EQREL_1:def 5;
[x,Vx] in Class eqR,
a
by A24, A25, A82, A83, A87;
then A90:
Class eqR,
a = Class eqR,
[x,Vx]
by A86, EQREL_1:31;
[v,Vv] in Class eqR,
b
by A24, A25, A84, A85, A89;
then
[x,Vx] = [v,Vv]
by A81, A83, A85, A87, A88, A89, A90, EQREL_1:31;
then
(
x = v &
Vx = Vv )
by ZFMISC_1:33;
hence
z in rng f
by A72, A74, A76, A80, FUNCT_1:12;
:: thesis: verum
end;
f " FVx is
finite
by A40, FINSET_1:13;
then
FVx is
finite
by A73, FINSET_1:27;
then
V is
open
by A59, TOPS_2:27;
then
Int V = V
by TOPS_1:55;
hence
V is
a_neighborhood of
0. X
by A66, CONNSP_2:def 1;
:: thesis: K + V misses C + Vset FxVxV =
{ ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ;
set FxVxVx =
{ ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ;
A91:
K + V c= union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in K + V or z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } )
assume A92:
z in K + V
;
:: thesis: z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
K + V = { (u + v) where u, v is Point of X : ( u in K & v in V ) }
by RUSUB_4:def 10;
then consider u,
v being
Point of
X such that A93:
z = u + v
and A94:
u in K
and A95:
v in V
by A92;
consider Vu being
Subset of
X such that A96:
u in Vu
and A97:
Vu in G
by A39, A94, Th2;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A98:
(
Vu = x + Vx &
[x,Vx] in rng g )
by A41, A97;
A99:
z in (x + Vx) + V
by A93, A95, A96, A98, Th3;
(x + Vx) + V in { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by A97, A98;
hence
z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by A99, TARSKI:def 4;
:: thesis: verum
end; A100:
union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } c= union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } or z in union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } )
assume
z in union { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
;
:: thesis: z in union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
then consider Y being
set such that A101:
z in Y
and A102:
Y in { ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by TARSKI:def 4;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A103:
Y = (x + Vx) + V
and A104:
(
x + Vx in G &
[x,Vx] in rng g )
by A102;
(x + Vx) + V = { (u + v) where u, v is Point of X : ( u in x + Vx & v in V ) }
by RUSUB_4:def 10;
then consider u,
v being
Point of
X such that A105:
z = u + v
and A106:
u in x + Vx
and A107:
v in V
by A101, A103;
Vx in FVx
by A104;
then
v in Vx
by A107, SETFAM_1:def 1;
then A108:
u + v in (x + Vx) + Vx
by A106, Th3;
(x + Vx) + Vx in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by A104;
hence
z in union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by A105, A108, TARSKI:def 4;
:: thesis: verum
end; now let Z be
set ;
:: thesis: ( ( Z in {{} } implies ex A, B being set st
( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B ) ) & ( ex A, B being set st
( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B ) implies Z in {{} } ) )hereby :: thesis: ( ex A, B being set st
( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B ) implies Z in {{} } )
assume
Z in {{} }
;
:: thesis: ex A, B being set st
( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B )then A109:
Z = {}
by TARSKI:def 1;
reconsider A =
C + V as
set ;
consider y being
Point of
X such that A110:
y in K
by A3, SUBSET_1:10;
consider W being
Subset of
X such that
y in W
and A111:
W in G
by A39, A110, Th2;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A112:
(
W = x + Vx &
[x,Vx] in rng g )
by A41, A111;
A113:
Vx is
symmetric
by A42, A111, A112;
A114:
((x + Vx) + Vx) + Vx misses C
by A42, A111, A112;
reconsider B =
(x + Vx) + Vx as
set ;
take A =
A;
:: thesis: ex B being set st
( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B )take B =
B;
:: thesis: ( A in {(C + V)} & B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B )thus
A in {(C + V)}
by TARSKI:def 1;
:: thesis: ( B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } & Z = A /\ B )thus
B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by A111, A112;
:: thesis: Z = A /\ Bnow assume
A meets B
;
:: thesis: contradictionthen consider z being
set such that A115:
z in A
and A116:
z in B
by XBOOLE_0:3;
reconsider z =
z as
Point of
X by A115;
C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) }
by RUSUB_4:def 10;
then consider u,
v being
Point of
X such that A117:
z = u + v
and A118:
u in C
and A119:
v in V
by A115;
Vx in FVx
by A111, A112;
then
v in Vx
by A119, SETFAM_1:def 1;
then
- v in Vx
by A113, Th26;
then A120:
z + (- v) in ((x + Vx) + Vx) + Vx
by A116, Th3;
z + (- v) =
u + (v + (- v))
by A117, RLVECT_1:def 6
.=
u + (0. X)
by RLVECT_1:16
.=
u
by RLVECT_1:10
;
hence
contradiction
by A114, A118, A120, XBOOLE_0:3;
:: thesis: verum end; hence
Z = A /\ B
by A109, XBOOLE_0:def 7;
:: thesis: verum
end; given A,
B being
set such that A121:
A in {(C + V)}
and A122:
B in { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
and A123:
Z = A /\ B
;
:: thesis: Z in {{} }A124:
A = C + V
by A121, TARSKI:def 1;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A125:
B = (x + Vx) + Vx
and A126:
(
x + Vx in G &
[x,Vx] in rng g )
by A122;
A127:
Vx is
symmetric
by A42, A126;
A128:
((x + Vx) + Vx) + Vx misses C
by A42, A126;
now assume
A meets B
;
:: thesis: contradictionthen consider z being
set such that A129:
z in A
and A130:
z in B
by XBOOLE_0:3;
reconsider z =
z as
Point of
X by A121, A129;
C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) }
by RUSUB_4:def 10;
then consider u,
v being
Point of
X such that A131:
z = u + v
and A132:
u in C
and A133:
v in V
by A124, A129;
Vx in FVx
by A126;
then
v in Vx
by A133, SETFAM_1:def 1;
then
- v in Vx
by A127, Th26;
then A134:
z + (- v) in ((x + Vx) + Vx) + Vx
by A125, A130, Th3;
z + (- v) =
u + (v + (- v))
by A131, RLVECT_1:def 6
.=
u + (0. X)
by RLVECT_1:16
.=
u
by RLVECT_1:10
;
hence
contradiction
by A128, A132, A134, XBOOLE_0:3;
:: thesis: verum end; then
A /\ B = {}
by XBOOLE_0:def 7;
hence
Z in {{} }
by A123, TARSKI:def 1;
:: thesis: verum end; then
INTERSECTION {(C + V)},
{ ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } = {{} }
by SETFAM_1:def 5;
then
union (INTERSECTION {(C + V)},{ ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ) = {}
by ZFMISC_1:31;
then
(C + V) /\ (union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) } ) = {}
by SETFAM_1:36;
then
C + V misses union { ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g ) }
by XBOOLE_0:def 7;
hence
K + V misses C + V
by A91, A100, XBOOLE_1:1, XBOOLE_1:63;
:: thesis: verum end;