let X be LinearTopSpace; 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; for V being Subset of X holds x + (Cl V) = Cl (x + V)
let V be Subset of X; x + (Cl V) = Cl (x + V)
thus
x + (Cl V) c= Cl (x + V)
XBOOLE_0:def 10 Cl (x + V) c= x + (Cl V)proof
let v be
object ;
TARSKI:def 3 ( not v in x + (Cl V) or v in Cl (x + V) )
assume A1:
v in x + (Cl V)
;
v in Cl (x + V)
then reconsider v =
v as
Point of
X ;
now for G being Subset of X st G is open & v in G holds
x + V meets GA2:
x + (Cl V) = { (x + u) where u is Point of X : u in Cl V }
by RUSUB_4:def 8;
A3:
x + V = { (x + u) where u is Point of X : u in V }
by RUSUB_4:def 8;
let G be
Subset of
X;
( G is open & v in G implies x + V meets G )assume that A4:
G is
open
and A5:
v in G
;
x + V meets GA6:
(- x) + G = { ((- x) + u) where u is Point of X : u in G }
by RUSUB_4:def 8;
then A7:
(- x) + v in (- x) + G
by A5;
consider u being
Point of
X such that A8:
v = x + u
and A9:
u in Cl V
by A1, A2;
(- x) + v =
((- x) + x) + u
by A8, RLVECT_1:def 3
.=
(0. X) + u
by RLVECT_1:5
.=
u
;
then
V meets (- x) + G
by A4, A9, A7, PRE_TOPC:24;
then consider z being
object 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 A6, A11;
A14:
x + z in x + V
by A3, A10;
x + z =
(x + (- x)) + w
by A12, RLVECT_1:def 3
.=
(0. X) + w
by RLVECT_1:5
.=
w
;
hence
x + V meets G
by A13, A14, XBOOLE_0:3;
verum end;
hence
v in Cl (x + V)
by PRE_TOPC:24;
verum
end;
x + V c= x + (Cl V)
by Th8, PRE_TOPC:18;
hence
Cl (x + V) c= x + (Cl V)
by TOPS_1:5; verum