let X be LinearTopSpace; 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; 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; ( K misses C implies ex V being a_neighborhood of 0. X st K + V misses C + V )
assume A1:
K misses C
; ex V being a_neighborhood of 0. X st K + V misses C + V
per cases
( K = {} or K <> {} )
;
suppose A3:
K <> {}
;
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 ) } ;
defpred S1[
object ,
object ]
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 );
A13:
for
x,
y,
z being
object st
S1[
x,
y] &
S1[
y,
z] holds
S1[
x,
z]
proof
let x,
y,
z be
object ;
( 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 A14:
x = [v1,V1]
and A15:
y = [v2,V2]
and A16:
v1 + V1 = v2 + V2
;
( 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 A17:
y = [w1,W1]
and A18:
(
z = [w2,W2] &
w1 + W1 = w2 + W2 )
;
S1[x,z]
take
v1
;
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
;
ex V1, V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take
V1
;
ex V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take
W2
;
( x = [v1,V1] & z = [w2,W2] & v1 + V1 = w2 + W2 )
v2 = w1
by A15, A17, XTUPLE_0:1;
hence
(
x = [v1,V1] &
z = [w2,W2] &
v1 + V1 = w2 + W2 )
by A14, A15, A16, A17, A18, XTUPLE_0:1;
verum
end; 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 by A10;
A19:
for
x being
object st
x in xV holds
S1[
x,
x]
A20:
for
x,
y being
object st
S1[
x,
y] holds
S1[
y,
x]
;
consider eqR being
Equivalence_Relation of
xV such that A21:
for
x,
y being
object holds
(
[x,y] in eqR iff (
x in xV &
y in xV &
S1[
x,
y] ) )
from EQREL_1:sch 1(A19, A20, A13);
then consider g being
Function such that A22:
dom g = Class eqR
and A23:
for
X being
set st
X in Class eqR holds
g . X in X
by FUNCT_1:111;
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 ;
A24:
F is
Cover of
K
proof
let x be
object ;
TARSKI:def 3,
SETFAM_1:def 11 ( not x in K or x in union F )
assume A25:
x in K
;
x in union F
then reconsider x =
x as
Point of
X ;
consider Vx being
open a_neighborhood of
0. X such that A26:
(
Vx is
symmetric &
((x + Vx) + Vx) + Vx misses C )
by A4, A25;
[x,Vx] in xV
by A25, A26;
then A27:
Class (
eqR,
[x,Vx])
in Class eqR
by EQREL_1:def 3;
then A28:
g . (Class (eqR,[x,Vx])) in rng g
by A22, FUNCT_1:def 3;
x + (0. X) in x + Vx
by Lm1, CONNSP_2:4;
then A29:
x in x + Vx
;
g . (Class (eqR,[x,Vx])) in Class (
eqR,
[x,Vx])
by A23, A27;
then
[(g . (Class (eqR,[x,Vx]))),[x,Vx]] in eqR
by EQREL_1:19;
then consider v1,
v2 being
Point of
X,
V1,
V2 being
open a_neighborhood of
0. X such that A30:
g . (Class (eqR,[x,Vx])) = [v1,V1]
and A31:
[x,Vx] = [v2,V2]
and A32:
v1 + V1 = v2 + V2
by A21;
(
x = v2 &
Vx = V2 )
by A31, XTUPLE_0:1;
then
x + Vx in F
by A30, A32, A28;
hence
x in union F
by A29, TARSKI:def 4;
verum
end;
F is
open
then consider G being
Subset-Family of
X such that A33:
G c= F
and A34:
G is
Cover of
K
and A35:
G is
finite
by A24, COMPTS_1:def 4;
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 ;
defpred S2[
object ,
object ]
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 );
A36:
for
x being
object st
x in G holds
ex
y being
object st
(
y in FVx &
S2[
x,
y] )
consider f being
Function of
G,
FVx such that A39:
for
x being
object st
x in G holds
S2[
x,
f . x]
from FUNCT_2:sch 1(A36);
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 ) } ;
take V =
meet FVx;
( V is a_neighborhood of 0. X & K + V misses C + V )A40:
rng g c= xV
A43:
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 )
then A48:
dom f = G
by FUNCT_2:def 1;
A49:
FVx c= rng f
proof
let z be
object ;
TARSKI:def 3 ( not z in FVx or z in rng f )
assume
z in FVx
;
z in rng f
then consider Vx being
open a_neighborhood of
0. X such that A50:
z = Vx
and A51:
ex
x being
Point of
X st
(
x + Vx in G &
[x,Vx] in rng g )
;
consider x being
Point of
X such that A52:
x + Vx in G
and A53:
[x,Vx] in rng g
by A51;
consider v being
Point of
X,
Vv being
open a_neighborhood of
0. X such that A54:
x + Vx = v + Vv
and
v + Vv in G
and A55:
[v,Vv] in rng g
and A56:
f . (x + Vx) = Vv
by A39, A52;
[[x,Vx],[v,Vv]] in eqR
by A21, A40, A53, A54, A55;
then
[x,Vx] in Class (
eqR,
[v,Vv])
by EQREL_1:19;
then A57:
Class (
eqR,
[v,Vv])
= Class (
eqR,
[x,Vx])
by A40, A55, EQREL_1:23;
consider A being
object such that A58:
A in dom g
and A59:
[x,Vx] = g . A
by A53, FUNCT_1:def 3;
consider a being
object such that A60:
a in xV
and A61:
A = Class (
eqR,
a)
by A22, A58, EQREL_1:def 3;
[x,Vx] in Class (
eqR,
a)
by A22, A23, A58, A59, A61;
then A62:
Class (
eqR,
a)
= Class (
eqR,
[x,Vx])
by A60, EQREL_1:23;
consider B being
object such that A63:
B in dom g
and A64:
[v,Vv] = g . B
by A55, FUNCT_1:def 3;
consider b being
object such that A65:
b in xV
and A66:
B = Class (
eqR,
b)
by A22, A63, EQREL_1:def 3;
[v,Vv] in Class (
eqR,
b)
by A22, A23, A63, A64, A66;
then
[x,Vx] = [v,Vv]
by A57, A59, A64, A61, A65, A66, A62, EQREL_1:23;
then
Vx = Vv
by XTUPLE_0:1;
hence
z in rng f
by A48, A50, A52, A56, FUNCT_1:3;
verum
end; A67:
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;
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;
( x + Vx in G & [x,Vx] in rng g implies ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) )
assume that A68:
x + Vx in G
and A69:
[x,Vx] in rng g
;
( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
consider A being
object such that A70:
A in dom g
and A71:
[x,Vx] = g . A
by A69, FUNCT_1:def 3;
consider a being
object such that A72:
a in xV
and A73:
A = Class (
eqR,
a)
by A22, A70, EQREL_1:def 3;
[x,Vx] in Class (
eqR,
a)
by A22, A23, A70, A71, A73;
then A74:
Class (
eqR,
a)
= Class (
eqR,
[x,Vx])
by A72, EQREL_1:23;
x + Vx in F
by A33, A68;
then consider v being
Point of
X,
Vv being
open a_neighborhood of
0. X such that A75:
x + Vx = v + Vv
and A76:
[v,Vv] in rng g
;
[[x,Vx],[v,Vv]] in eqR
by A21, A40, A69, A75, A76;
then
[x,Vx] in Class (
eqR,
[v,Vv])
by EQREL_1:19;
then A77:
Class (
eqR,
[v,Vv])
= Class (
eqR,
[x,Vx])
by A40, A76, EQREL_1:23;
consider B being
object such that A78:
B in dom g
and A79:
[v,Vv] = g . B
by A76, FUNCT_1:def 3;
consider b being
object such that A80:
b in xV
and A81:
B = Class (
eqR,
b)
by A22, A78, EQREL_1:def 3;
[v,Vv] in Class (
eqR,
b)
by A22, A23, A78, A79, A81;
then A82:
[x,Vx] = [v,Vv]
by A77, A71, A79, A73, A80, A81, A74, EQREL_1:23;
then A83:
Vx = Vv
by XTUPLE_0:1;
[v,Vv] in xV
by A40, A76;
then consider u being
Point of
X,
Vu being
open a_neighborhood of
0. X such that A84:
[u,Vu] = [v,Vv]
and A85:
(
u in K &
Vu is
symmetric &
((u + Vu) + Vu) + Vu misses C )
;
Vv = Vu
by A84, XTUPLE_0:1;
hence
(
x in K &
Vx is
symmetric &
((x + Vx) + Vx) + Vx misses C )
by A84, A85, A82, A83, XTUPLE_0:1;
verum
end; now for Z being set holds
( ( 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 {{}} ) )let Z be
set ;
( ( 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 ( 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 {{}} )
reconsider A =
C + V as
set ;
assume
Z in {{}}
;
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 A86:
Z = {}
by TARSKI:def 1;
consider y being
Point of
X such that A87:
y in K
by A3, SUBSET_1:4;
consider W being
Subset of
X such that
y in W
and A88:
W in G
by A34, A87, Th2;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A89:
(
W = x + Vx &
[x,Vx] in rng g )
by A43, A88;
A90:
((x + Vx) + Vx) + Vx misses C
by A67, A88, A89;
reconsider B =
(x + Vx) + Vx as
set ;
take A =
A;
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;
( 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;
( 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 A88, A89;
Z = A /\ BA91:
Vx is
symmetric
by A67, A88, A89;
now not A meets BA92:
C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) }
by RUSUB_4:def 9;
assume
A meets B
;
contradictionthen consider z being
object such that A93:
z in A
and A94:
z in B
by XBOOLE_0:3;
reconsider z =
z as
Point of
X by A93;
consider u,
v being
Point of
X such that A95:
z = u + v
and A96:
u in C
and A97:
v in V
by A93, A92;
Vx in FVx
by A88, A89;
then
v in Vx
by A97, SETFAM_1:def 1;
then
- v in Vx
by A91, Th25;
then A98:
z + (- v) in ((x + Vx) + Vx) + Vx
by A94, Th3;
z + (- v) =
u + (v + (- v))
by A95, RLVECT_1:def 3
.=
u + (0. X)
by RLVECT_1:5
.=
u
;
hence
contradiction
by A90, A96, A98, XBOOLE_0:3;
verum end; hence
Z = A /\ B
by A86;
verum
end; given A,
B being
set such that A99:
A in {(C + V)}
and A100:
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 A101:
Z = A /\ B
;
Z in {{}}A102:
A = C + V
by A99, TARSKI:def 1;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A103:
B = (x + Vx) + Vx
and A104:
(
x + Vx in G &
[x,Vx] in rng g )
by A100;
A105:
((x + Vx) + Vx) + Vx misses C
by A67, A104;
A106:
Vx is
symmetric
by A67, A104;
now not A meets BA107:
C + V = { (u + v) where u, v is Point of X : ( u in C & v in V ) }
by RUSUB_4:def 9;
assume
A meets B
;
contradictionthen consider z being
object such that A108:
z in A
and A109:
z in B
by XBOOLE_0:3;
reconsider z =
z as
Point of
X by A99, A108;
consider u,
v being
Point of
X such that A110:
z = u + v
and A111:
u in C
and A112:
v in V
by A102, A108, A107;
Vx in FVx
by A104;
then
v in Vx
by A112, SETFAM_1:def 1;
then
- v in Vx
by A106, Th25;
then A113:
z + (- v) in ((x + Vx) + Vx) + Vx
by A103, A109, Th3;
z + (- v) =
u + (v + (- v))
by A110, RLVECT_1:def 3
.=
u + (0. X)
by RLVECT_1:5
.=
u
;
hence
contradiction
by A105, A111, A113, XBOOLE_0:3;
verum end; then
A /\ B = {}
;
hence
Z in {{}}
by A101, TARSKI:def 1;
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:25;
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:25;
then A114:
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 ) }
;
A115:
FVx is
open
f " FVx is
finite
by A35, FINSET_1:1;
then
FVx is
finite
by A49, FINSET_1:9;
then
V is
open
by A115, TOPS_2:20;
then A116:
Int V = V
by TOPS_1:23;
then
0. X in V
by A44, SETFAM_1:def 1;
hence
V is
a_neighborhood of
0. X
by A116, CONNSP_2:def 1;
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 ) } ;
A118:
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
object ;
TARSKI:def 3 ( 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 ) }
;
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 A119:
z in Y
and A120:
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 A121:
Y = (x + Vx) + V
and A122:
(
x + Vx in G &
[x,Vx] in rng g )
by A120;
A123:
(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 A122;
(x + Vx) + V = { (u + v) where u, v is Point of X : ( u in x + Vx & v in V ) }
by RUSUB_4:def 9;
then consider u,
v being
Point of
X such that A124:
z = u + v
and A125:
u in x + Vx
and A126:
v in V
by A119, A121;
Vx in FVx
by A122;
then
v in Vx
by A126, SETFAM_1:def 1;
then
u + v in (x + Vx) + Vx
by A125, Th3;
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 A124, A123, TARSKI:def 4;
verum
end;
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
object ;
TARSKI:def 3 ( 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 ) } )
A127:
K + V = { (u + v) where u, v is Point of X : ( u in K & v in V ) }
by RUSUB_4:def 9;
assume
z in K + V
;
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 ) }
then consider u,
v being
Point of
X such that A128:
z = u + v
and A129:
u in K
and A130:
v in V
by A127;
consider Vu being
Subset of
X such that A131:
u in Vu
and A132:
Vu in G
by A34, A129, Th2;
consider x being
Point of
X,
Vx being
open a_neighborhood of
0. X such that A133:
Vu = x + Vx
and A134:
[x,Vx] in rng g
by A43, A132;
A135:
(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 A132, A133, A134;
z in (x + Vx) + V
by A128, A130, A131, A133, Th3;
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 A135, TARSKI:def 4;
verum
end; hence
K + V misses C + V
by A118, A114, XBOOLE_1:1, XBOOLE_1:63;
verum end;