let X be LinearTopSpace; :: thesis: for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
let x be Point of X; :: thesis: for V being Subset of X holds x + (Cl V) = Cl (x + V)
let V be Subset of X; :: thesis: x + (Cl V) = Cl (x + V)
thus
x + (Cl V) c= Cl (x + V)
:: according to XBOOLE_0:def 10 :: thesis: Cl (x + V) c= x + (Cl V)proof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in x + (Cl V) or v in Cl (x + V) )
assume A1:
v in x + (Cl V)
;
:: thesis: v in Cl (x + V)
then reconsider v =
v as
Point of
X ;
now let G be
Subset of
X;
:: thesis: ( G is open & v in G implies x + V meets G )assume that A2:
G is
open
and A3:
v in G
;
:: thesis: x + V meets GA4:
(- x) + G = { ((- x) + u) where u is Point of X : u in G }
by RUSUB_4:def 9;
A5:
x + V = { (x + u) where u is Point of X : u in V }
by RUSUB_4:def 9;
x + (Cl V) = { (x + u) where u is Point of X : u in Cl V }
by RUSUB_4:def 9;
then consider u being
Point of
X such that A6:
v = x + u
and A7:
u in Cl V
by A1;
A8:
(- x) + v in (- x) + G
by A3, A4;
(- x) + v =
((- x) + x) + u
by A6, RLVECT_1:def 6
.=
(0. X) + u
by RLVECT_1:16
.=
u
by RLVECT_1:10
;
then
V meets (- x) + G
by A7, A8, A2, PRE_TOPC:54;
then consider z being
set such that A10:
z in V
and A11:
z in (- x) + G
by XBOOLE_0:3;
reconsider z =
z as
Point of
X by A10;
consider w being
Point of
X such that A12:
z = (- x) + w
and A13:
w in G
by A4, A11;
A14:
x + z in x + V
by A5, A10;
x + z =
(x + (- x)) + w
by A12, RLVECT_1:def 6
.=
(0. X) + w
by RLVECT_1:16
.=
w
by RLVECT_1:10
;
hence
x + V meets G
by A13, A14, XBOOLE_0:3;
:: thesis: verum end;
hence
v in Cl (x + V)
by PRE_TOPC:54;
:: thesis: verum
end;
x + V c= x + (Cl V)
by Th8, PRE_TOPC:48;
hence
Cl (x + V) c= x + (Cl V)
by TOPS_1:31; :: thesis: verum