let X be LinearTopSpace; :: thesis: for A being Subset of X holds Cl A = meet { (A + V) where V is a_neighborhood of 0. X : verum }
let A be Subset of X; :: thesis: Cl A = meet { (A + V) where V is a_neighborhood of 0. X : verum }
set AV = { (A + V) where V is a_neighborhood of 0. X : verum } ;
set V = the a_neighborhood of 0. X;
A1: for x being Point of X
for V being a_neighborhood of 0. X holds
( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
proof
let x be Point of X; :: thesis: for V being a_neighborhood of 0. X holds
( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
let V be a_neighborhood of 0. X; :: thesis: ( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
A2: A + ((- 1) * (Int V)) = { (a + v) where a, v is Point of X : ( a in A & v in (- 1) * (Int V) ) } by RUSUB_4:def 9;
hereby :: thesis: ( x in A + ((- 1) * (Int V)) implies A meets x + (Int V) )
assume A meets x + (Int V) ; :: thesis: x in A + ((- 1) * (Int V))
then x in A + (- (Int V)) by Th24;
hence x in A + ((- 1) * (Int V)) ; :: thesis: verum
end;
assume x in A + ((- 1) * (Int V)) ; :: thesis: A meets x + (Int V)
then consider a, v being Point of X such that
A3: x = a + v and
A4: a in A and
A5: v in (- 1) * (Int V) by A2;
consider v9 being Point of X such that
A6: v = (- 1) * v9 and
A7: v9 in Int V by A5;
- v = (- 1) * v by RLVECT_1:16
.= ((- 1) * (- 1)) * v9 by A6, RLVECT_1:def 7
.= v9 by RLVECT_1:def 8 ;
then A8: x + v9 = a + (v + (- v)) by A3, RLVECT_1:def 3
.= a + (0. X) by RLVECT_1:5
.= a ;
x + (Int V) = { (x + w) where w is Point of X : w in Int V } by RUSUB_4:def 8;
then x + v9 in x + (Int V) by A7;
hence A meets x + (Int V) by A4, A8, XBOOLE_0:3; :: thesis: verum
end;
{ (A + V) where V is a_neighborhood of 0. X : verum } c= bool the carrier of X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (A + V) where V is a_neighborhood of 0. X : verum } or x in bool the carrier of X )
assume x in { (A + V) where V is a_neighborhood of 0. X : verum } ; :: thesis: x in bool the carrier of X
then ex V being a_neighborhood of 0. X st x = A + V ;
hence x in bool the carrier of X ; :: thesis: verum
end;
then reconsider AV9 = { (A + V) where V is a_neighborhood of 0. X : verum } as Subset-Family of X ;
A9: for x being Point of X holds
( x in Cl A iff for V being a_neighborhood of 0. X holds A meets x + (Int V) )
proof
let x be Point of X; :: thesis: ( x in Cl A iff for V being a_neighborhood of 0. X holds A meets x + (Int V) )
hereby :: thesis: ( ( for V being a_neighborhood of 0. X holds A meets x + (Int V) ) implies x in Cl A )
assume A10: x in Cl A ; :: thesis: for V being a_neighborhood of 0. X holds A meets x + (Int V)
let V be a_neighborhood of 0. X; :: thesis: A meets x + (Int V)
0. X in Int V by CONNSP_2:def 1;
then x + (0. X) in x + (Int V) by Lm1;
then x in x + (Int V) ;
hence A meets x + (Int V) by A10, TOPS_1:12; :: thesis: verum
end;
assume A11: for V being a_neighborhood of 0. X holds A meets x + (Int V) ; :: thesis: x in Cl A
now :: thesis: for V being Subset of X st V is open & x in V holds
A meets V
let V be Subset of X; :: thesis: ( V is open & x in V implies A meets V )
assume that
A12: V is open and
A13: x in V ; :: thesis: A meets V
A14: Int ((- x) + V) = (- x) + V by A12, TOPS_1:23;
(- x) + x in (- x) + V by A13, Lm1;
then 0. X in (- x) + V by RLVECT_1:5;
then (- x) + V is a_neighborhood of 0. X by A14, CONNSP_2:def 1;
then A meets x + ((- x) + V) by A11, A14;
then A meets (x + (- x)) + V by Th6;
then A meets (0. X) + V by RLVECT_1:5;
hence A meets V by Th5; :: thesis: verum
end;
hence x in Cl A by TOPS_1:12; :: thesis: verum
end;
A15: A + the a_neighborhood of 0. X in { (A + V) where V is a_neighborhood of 0. X : verum } ;
thus Cl A c= meet { (A + V) where V is a_neighborhood of 0. X : verum } :: according to XBOOLE_0:def 10 :: thesis: meet { (A + V) where V is a_neighborhood of 0. X : verum } c= Cl A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in meet { (A + V) where V is a_neighborhood of 0. X : verum } )
assume A16: x in Cl A ; :: thesis: x in meet { (A + V) where V is a_neighborhood of 0. X : verum }
then reconsider x = x as Point of X ;
now :: thesis: for Y being set st Y in { (A + V) where V is a_neighborhood of 0. X : verum } holds
x in Y
let Y be set ; :: thesis: ( Y in { (A + V) where V is a_neighborhood of 0. X : verum } implies x in Y )
assume Y in { (A + V) where V is a_neighborhood of 0. X : verum } ; :: thesis: x in Y
then consider V being a_neighborhood of 0. X such that
A17: Y = A + V ;
A18: A + V = { (a + v) where a, v is Point of X : ( a in A & v in V ) } by RUSUB_4:def 9;
A19: (- 1) * V is a_neighborhood of 0. X by Th55;
then A meets x + (Int ((- 1) * V)) by A9, A16;
then ( A + ((- 1) * (Int ((- 1) * V))) = { (a + v) where a, v is Point of X : ( a in A & v in (- 1) * (Int ((- 1) * V)) ) } & x in A + ((- 1) * (Int ((- 1) * V))) ) by A1, A19, RUSUB_4:def 9;
then consider a, v being Point of X such that
A20: ( x = a + v & a in A ) and
A21: v in (- 1) * (Int ((- 1) * V)) ;
consider v9 being Point of X such that
A22: v = (- 1) * v9 and
A23: v9 in Int ((- 1) * V) by A21;
Int ((- 1) * V) c= (- 1) * V by TOPS_1:16;
then v9 in (- 1) * V by A23;
then consider v99 being Point of X such that
A24: v9 = (- 1) * v99 and
A25: v99 in V ;
v = ((- 1) * (- 1)) * v99 by A22, A24, RLVECT_1:def 7
.= v99 by RLVECT_1:def 8 ;
hence x in Y by A17, A18, A20, A25; :: thesis: verum
end;
hence x in meet { (A + V) where V is a_neighborhood of 0. X : verum } by A15, SETFAM_1:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (A + V) where V is a_neighborhood of 0. X : verum } or x in Cl A )
assume A26: x in meet { (A + V) where V is a_neighborhood of 0. X : verum } ; :: thesis: x in Cl A
meet AV9 c= the carrier of X ;
then reconsider x = x as Point of X by A26;
now :: thesis: for V being a_neighborhood of 0. X holds A meets x + (Int V)
let V be a_neighborhood of 0. X; :: thesis: A meets x + (Int V)
0. X in Int V by CONNSP_2:def 1;
then Int V is a_neighborhood of 0. X by CONNSP_2:3;
then (- 1) * (Int V) is a_neighborhood of 0. X by Th55;
then A + ((- 1) * (Int V)) in { (A + V) where V is a_neighborhood of 0. X : verum } ;
then x in A + ((- 1) * (Int V)) by A26, SETFAM_1:def 1;
hence A meets x + (Int V) by A1; :: thesis: verum
end;
hence x in Cl A by A9; :: thesis: verum