:: Introduction to Real Linear Topological Spaces
:: by Czes{\l}aw Byli\'nski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem :: RLTOPSP1:1
for X being non empty RLSStruct
for M being Subset of X
for x being Point of X
for r being Real st x in M holds
r * x in r * M ;

registration
cluster non zero ext-real complex real for Element of REAL ;
existence
 not for b1 being Real holds b1 is zero
proofend;
end;

theorem Th2: :: RLTOPSP1:2
for T being non empty TopSpace
for X being non empty Subset of T
for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
proofend;

theorem Th3: :: RLTOPSP1:3
for X being non empty addLoopStr
for M, N being Subset of X
for x, y being Point of X st x in M & y in N holds
x + y in M + N
proofend;

Lm1:  for X being non empty addLoopStr
for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
proofend;

Lm2:  for X being non empty addLoopStr
for M, N being Subset of X holds  {  (x + N) where x is Point of X : x in M  }  is Subset-Family of X
proofend;

theorem Th4: :: RLTOPSP1:4
for X being non empty addLoopStr
for M, N being Subset of X
for F being Subset-Family of X st F =  {  (x + N) where x is Point of X : x in M  }  holds
M + N = union F
proofend;

theorem Th5: :: RLTOPSP1:5
for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X holds (0. X) + M = M
proofend;

theorem Th6: :: RLTOPSP1:6
for X being non empty add-associative addLoopStr
for x, y being Point of X
for M being Subset of X holds (x + y) + M = x + (y + M)
proofend;

theorem Th7: :: RLTOPSP1:7
for X being non empty add-associative addLoopStr
for x being Point of X
for M, N being Subset of X holds (x + M) + N = x + (M + N)
proofend;

theorem Th8: :: RLTOPSP1:8
for X being non empty addLoopStr
for M, N being Subset of X
for x being Point of X st M c= N holds
x + M c= x + N
proofend;

theorem Th9: :: RLTOPSP1:9
for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X
for x being Point of X st x in M holds
0. X in (- x) + M
proofend;

theorem Th10: :: RLTOPSP1:10
for X being non empty addLoopStr
for M, N, V being Subset of X st M c= N holds
M + V c= N + V
proofend;

Lm3:  for X being non empty addLoopStr
for M, N, V being Subset of X st M c= N holds
V + M c= V + N
proofend;

theorem Th11: :: RLTOPSP1:11
for X being non empty addLoopStr
for V1, V2, W1, W2 being Subset of X st V1 c= W1 & V2 c= W2 holds
V1 + V2 c= W1 + W2
proofend;

theorem Th12: :: RLTOPSP1:12
for X being non empty right_zeroed addLoopStr
for V1, V2 being Subset of X st 0. X in V2 holds
V1 c= V1 + V2
proofend;

theorem Th13: :: RLTOPSP1:13
for X being RealLinearSpace
for r being Real holds r * {(0. X)} = {(0. X)}
proofend;

theorem :: RLTOPSP1:14
for X being RealLinearSpace
for M being Subset of X
for r being non zero Real st 0. X in r * M holds
0. X in M
proofend;

theorem Th15: :: RLTOPSP1:15
for X being RealLinearSpace
for M, N being Subset of X
for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
proofend;

theorem :: RLTOPSP1:16
for X being non empty TopSpace
for x being Point of X
for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
proofend;

definition
let V be RealLinearSpace;
let M be Subset of V;
redefine attr M is convex  means :Def1: :: RLTOPSP1:def 1
 for u, v being Point of V
for r being Real st 0 <= r &amp; r <= 1 &amp; u in M &amp; v in M holds
(r * u) + ((1 - r) * v) in M;
compatibility
 ( M is convex iff for u, v being Point of V
for r being Real st 0 <= r &amp; r <= 1 &amp; u in M &amp; v in M holds
(r * u) + ((1 - r) * v) in M )
proofend;
end;

:: deftheorem Def1 defines convex RLTOPSP1:def_1_:_
 for V being RealLinearSpace
for M being Subset of V holds
( M is convex iff for u, v being Point of V
for r being Real st 0 <= r &amp; r <= 1 &amp; u in M &amp; v in M holds
(r * u) + ((1 - r) * v) in M );

Lm4:  for X being RealLinearSpace holds conv ({} X) = {}
proofend;

registration
let X be RealLinearSpace;
let M be empty Subset of X;
cluster conv M ->  empty ;
coherence
 conv M is empty
proofend;
end;

theorem :: RLTOPSP1:17
for X being RealLinearSpace
for M being convex Subset of X holds conv M = M
proofend;

theorem Th18: :: RLTOPSP1:18
for X being RealLinearSpace
for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
proofend;

theorem Th19: :: RLTOPSP1:19
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
Convex-Family M2 c= Convex-Family M1
proofend;

theorem Th20: :: RLTOPSP1:20
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
conv M1 c= conv M2
proofend;

theorem :: RLTOPSP1:21
for X being RealLinearSpace
for M being convex Subset of X
for r being Real st 0 <= r &amp; r <= 1 &amp; 0. X in M holds
r * M c= M
proofend;

definition
let X be RealLinearSpace;
let v, w be Point of X;
func LSeg (v,w) ->  Subset of X equals :: RLTOPSP1:def 2
 {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r &amp; r <= 1 )  }  ;
coherence
  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r &amp; r <= 1 )  }  is Subset of X
proofend;
commutativity
 for b1 being Subset of X
for v, w being Point of X st b1 =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r &amp; r <= 1 )  }  holds
b1 =  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r &amp; r <= 1 )  }
proofend;
end;

:: deftheorem  defines LSeg RLTOPSP1:def_2_:_
 for X being RealLinearSpace
for v, w being Point of X holds LSeg (v,w) =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r &amp; r <= 1 )  }  ;

registration
let X be RealLinearSpace;
let v, w be Point of X;
cluster LSeg (v,w) ->  non empty convex ;
coherence
 ( not LSeg (v,w) is empty &amp; LSeg (v,w) is convex )
proofend;
end;

theorem :: RLTOPSP1:22
for X being RealLinearSpace
for M being Subset of X holds
( M is convex iff for u, w being Point of X st u in M &amp; w in M holds
LSeg (u,w) c= M )
proofend;

definition
let V be non empty RLSStruct ;
let P be Subset-Family of V;
attrP is convex-membered  means :Def3: :: RLTOPSP1:def 3
 for M being Subset of V st M in P holds
M is convex ;
end;

:: deftheorem Def3 defines convex-membered RLTOPSP1:def_3_:_
 for V being non empty RLSStruct
for P being Subset-Family of V holds
( P is convex-membered iff for M being Subset of V st M in P holds
M is convex );

registration
let V be non empty RLSStruct ;
cluster non empty convex-membered for Element of bool (bool the carrier of V);
existence
 ex b1 being Subset-Family of V st
( not b1 is empty &amp; b1 is convex-membered )
proofend;
end;

theorem :: RLTOPSP1:23
for V being non empty RLSStruct
for F being convex-membered Subset-Family of V holds meet F is convex
proofend;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
func - A ->  Subset of X equals :: RLTOPSP1:def 4
(- 1) * A;
coherence
 (- 1) * A is Subset of X ;
end;

:: deftheorem  defines - RLTOPSP1:def_4_:_
 for X being non empty RLSStruct
for A being Subset of X holds - A = (- 1) * A;

theorem Th24: :: RLTOPSP1:24
for X being RealLinearSpace
for M, N being Subset of X
for v being Point of X holds
( v + M meets N iff v in N + (- M) )
proofend;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attrA is symmetric  means :Def5: :: RLTOPSP1:def 5
A = - A;
end;

:: deftheorem Def5 defines symmetric RLTOPSP1:def_5_:_
 for X being non empty RLSStruct
for A being Subset of X holds
( A is symmetric iff A = - A );

registration
let X be RealLinearSpace;
cluster non empty symmetric for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st
( not b1 is empty &amp; b1 is symmetric )
proofend;
end;

theorem Th25: :: RLTOPSP1:25
for X being RealLinearSpace
for A being symmetric Subset of X
for x being Point of X st x in A holds
- x in A
proofend;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attrA is circled  means :Def6: :: RLTOPSP1:def 6
 for r being Real st abs r <= 1 holds
r * A c= A;
end;

:: deftheorem Def6 defines circled RLTOPSP1:def_6_:_
 for X being non empty RLSStruct
for A being Subset of X holds
( A is circled iff for r being Real st abs r <= 1 holds
r * A c= A );

registration
let X be non empty RLSStruct ;
cluster empty  ->  circled for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is empty holds
b1 is circled
proofend;
end;

theorem Th26: :: RLTOPSP1:26
for X being RealLinearSpace holds {(0. X)} is circled
proofend;

registration
let X be RealLinearSpace;
cluster non empty circled for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st
( not b1 is empty &amp; b1 is circled )
proofend;
end;

theorem Th27: :: RLTOPSP1:27
for X being RealLinearSpace
for B being non empty circled Subset of X holds 0. X in B
proofend;

Lm5:  for X being RealLinearSpace
for A, B being circled Subset of X holds A + B is circled
proofend;

registration
let X be RealLinearSpace;
let A, B be circled Subset of X;
clusterA + B ->  circled ;
coherence
 A + B is circled by Lm5;
end;

theorem Th28: :: RLTOPSP1:28
for X being RealLinearSpace
for A being circled Subset of X
for r being Real st abs r = 1 holds
r * A = A
proofend;

Lm6:  for X being RealLinearSpace
for A being circled Subset of X holds A is symmetric
proofend;

registration
let X be RealLinearSpace;
cluster circled  ->  symmetric for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is circled holds
b1 is symmetric by Lm6;
end;

Lm7:  for X being RealLinearSpace
for M being circled Subset of X holds conv M is circled
proofend;

registration
let X be RealLinearSpace;
let M be circled Subset of X;
cluster conv M ->  circled ;
coherence
 conv M is circled by Lm7;
end;

definition
let X be non empty RLSStruct ;
let F be Subset-Family of X;
attrF is circled-membered  means :Def7: :: RLTOPSP1:def 7
 for V being Subset of X st V in F holds
V is circled ;
end;

:: deftheorem Def7 defines circled-membered RLTOPSP1:def_7_:_
 for X being non empty RLSStruct
for F being Subset-Family of X holds
( F is circled-membered iff for V being Subset of X st V in F holds
V is circled );

registration
let V be non empty RLSStruct ;
cluster non empty circled-membered for Element of bool (bool the carrier of V);
existence
 ex b1 being Subset-Family of V st
( not b1 is empty &amp; b1 is circled-membered )
proofend;
end;

theorem :: RLTOPSP1:29
for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds union F is circled
proofend;

theorem :: RLTOPSP1:30
for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds meet F is circled
proofend;

begin

definition
attrc1 is strict ;
struct RLTopStruct  ->  RLSStruct , TopStruct ;
aggrRLTopStruct(# carrier, ZeroF, addF, Mult, topology #) ->  RLTopStruct ;
end;

registration
let X be non empty set ;
let O be Element of X;
let F be BinOp of X;
let G be Function of [:REAL,X:],X;
let T be Subset-Family of X;
cluster RLTopStruct(# X,O,F,G,T #) ->  non empty ;
coherence
 not RLTopStruct(# X,O,F,G,T #) is empty ;
end;

registration
cluster non empty strict for RLTopStruct ;
existence
 ex b1 being RLTopStruct st
( b1 is strict &amp; not b1 is empty )
proofend;
end;

definition
let X be non empty RLTopStruct ;
attrX is add-continuous  means :Def8: :: RLTOPSP1:def 8
 for x1, x2 being Point of X
for V being Subset of X st V is open &amp; x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open &amp; V2 is open &amp; x1 in V1 &amp; x2 in V2 &amp; V1 + V2 c= V );
attrX is Mult-continuous  means :Def9: :: RLTOPSP1:def 9
 for a being Real
for x being Point of X
for V being Subset of X st V is open &amp; a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open &amp; x in W &amp; ( for s being Real st abs (s - a) < r holds
s * W c= V ) );
end;

:: deftheorem Def8 defines add-continuous RLTOPSP1:def_8_:_
 for X being non empty RLTopStruct holds
( X is add-continuous iff for x1, x2 being Point of X
for V being Subset of X st V is open &amp; x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open &amp; V2 is open &amp; x1 in V1 &amp; x2 in V2 &amp; V1 + V2 c= V ) );

:: deftheorem Def9 defines Mult-continuous RLTOPSP1:def_9_:_
 for X being non empty RLTopStruct holds
( X is Mult-continuous iff for a being Real
for x being Point of X
for V being Subset of X st V is open &amp; a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open &amp; x in W &amp; ( for s being Real st abs (s - a) < r holds
s * W c= V ) ) );

registration
cluster non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous for RLTopStruct ;
existence
 ex b1 being non empty RLTopStruct st
( b1 is strict &amp; b1 is add-continuous &amp; b1 is Mult-continuous &amp; b1 is TopSpace-like &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital )
proofend;
end;

definition
mode LinearTopSpace is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous RLTopStruct ;
end;

theorem Th31: :: RLTOPSP1:31
for X being LinearTopSpace
for x1, x2 being Point of X
for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
proofend;

theorem Th32: :: RLTOPSP1:32
for X being LinearTopSpace
for a being Real
for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
proofend;

definition
let X be non empty RLTopStruct ;
let a be Point of X;
func transl (a,X) ->  Function of X,X means :Def10: :: RLTOPSP1:def 10
 for x being Point of X holds it . x = a + x;
existence
 ex b1 being Function of X,X st
for x being Point of X holds b1 . x = a + x
proofend;
uniqueness
 for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = a + x ) &amp; ( for x being Point of X holds b2 . x = a + x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines transl RLTOPSP1:def_10_:_
 for X being non empty RLTopStruct
for a being Point of X
for b3 being Function of X,X holds
( b3 = transl (a,X) iff for x being Point of X holds b3 . x = a + x );

theorem Th33: :: RLTOPSP1:33
for X being non empty RLTopStruct
for a being Point of X
for V being Subset of X holds (transl (a,X)) .: V = a + V
proofend;

theorem Th34: :: RLTOPSP1:34
for X being LinearTopSpace
for a being Point of X holds rng (transl (a,X)) = [#] X
proofend;

Lm8:  for X being LinearTopSpace
for a being Point of X holds transl (a,X) is one-to-one
proofend;

theorem Th35: :: RLTOPSP1:35
for X being LinearTopSpace
for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
proofend;

Lm9:  for X being LinearTopSpace
for a being Point of X holds transl (a,X) is continuous
proofend;

registration
let X be LinearTopSpace;
let a be Point of X;
cluster transl (a,X) ->  being_homeomorphism ;
coherence
 transl (a,X) is being_homeomorphism
proofend;
end;

Lm10:  for X being LinearTopSpace
for E being Subset of X
for x being Point of X st E is open holds
x + E is open
proofend;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let x be Point of X;
clusterx + E ->  open ;
coherence
 x + E is open by Lm10;
end;

Lm11:  for X being LinearTopSpace
for E being open Subset of X
for K being Subset of X holds K + E is open
proofend;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let K be Subset of X;
clusterK + E ->  open ;
coherence
 K + E is open by Lm11;
end;

Lm12:  for X being LinearTopSpace
for D being closed Subset of X
for x being Point of X holds x + D is closed
proofend;

registration
let X be LinearTopSpace;
let D be closed Subset of X;
let x be Point of X;
clusterx + D ->  closed ;
coherence
 x + D is closed by Lm12;
end;

theorem Th36: :: RLTOPSP1:36
for X being LinearTopSpace
for V1, V2, V being Subset of X st V1 + V2 c= V holds
(Int V1) + (Int V2) c= Int V
proofend;

theorem Th37: :: RLTOPSP1:37
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Int V) = Int (x + V)
proofend;

theorem :: RLTOPSP1:38
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
proofend;

theorem :: RLTOPSP1:39
for X being LinearTopSpace
for x, v being Point of X
for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
proofend;

theorem :: RLTOPSP1:40
for X being LinearTopSpace
for x being Point of X
for V being a_neighborhood of x holds (- x) + V is a_neighborhood of 0. X
proofend;

definition
let X be non empty RLTopStruct ;
mode local_base of X is basis of 0. X;
end;

definition
let X be non empty RLTopStruct ;
attrX is locally-convex  means :Def11: :: RLTOPSP1:def 11
 ex P being local_base of X st P is convex-membered ;
end;

:: deftheorem Def11 defines locally-convex RLTOPSP1:def_11_:_
 for X being non empty RLTopStruct holds
( X is locally-convex iff ex P being local_base of X st P is convex-membered );

definition
let X be LinearTopSpace;
let E be Subset of X;
attrE is bounded  means :Def12: :: RLTOPSP1:def 12
 for V being a_neighborhood of 0. X ex s being Real st
( s > 0 &amp; ( for t being Real st t > s holds
E c= t * V ) );
end;

:: deftheorem Def12 defines bounded RLTOPSP1:def_12_:_
 for X being LinearTopSpace
for E being Subset of X holds
( E is bounded iff for V being a_neighborhood of 0. X ex s being Real st
( s > 0 &amp; ( for t being Real st t > s holds
E c= t * V ) ) );

registration
let X be LinearTopSpace;
cluster empty  ->  bounded for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is empty holds
b1 is bounded
proofend;
end;

registration
let X be LinearTopSpace;
cluster bounded for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st b1 is bounded
proofend;
end;

theorem Th41: :: RLTOPSP1:41
for X being LinearTopSpace
for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded
proofend;

theorem :: RLTOPSP1:42
for X being LinearTopSpace
for P being bounded Subset of X
for Q being Subset of X st Q c= P holds
Q is bounded
proofend;

theorem :: RLTOPSP1:43
for X being LinearTopSpace
for F being Subset-Family of X st F is finite &amp; F =  {  P where P is bounded Subset of X : verum  }  holds
union F is bounded
proofend;

theorem Th44: :: RLTOPSP1:44
for X being LinearTopSpace
for P being Subset-Family of X st P =  {  U where U is a_neighborhood of 0. X : verum  }  holds
P is local_base of X
proofend;

theorem :: RLTOPSP1:45
for X being LinearTopSpace
for O being local_base of X
for P being Subset-Family of X st P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  holds
P is basis of X
proofend;

definition
let X be non empty RLTopStruct ;
let r be Real;
func mlt (r,X) ->  Function of X,X means :Def13: :: RLTOPSP1:def 13
 for x being Point of X holds it . x = r * x;
existence
 ex b1 being Function of X,X st
for x being Point of X holds b1 . x = r * x
proofend;
uniqueness
 for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = r * x ) &amp; ( for x being Point of X holds b2 . x = r * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines mlt RLTOPSP1:def_13_:_
 for X being non empty RLTopStruct
for r being Real
for b3 being Function of X,X holds
( b3 = mlt (r,X) iff for x being Point of X holds b3 . x = r * x );

theorem Th46: :: RLTOPSP1:46
for X being non empty RLTopStruct
for V being Subset of X
for r being non zero Real holds (mlt (r,X)) .: V = r * V
proofend;

theorem Th47: :: RLTOPSP1:47
for X being LinearTopSpace
for r being non zero Real holds rng (mlt (r,X)) = [#] X
proofend;

Lm13:  for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is one-to-one
proofend;

theorem Th48: :: RLTOPSP1:48
for X being LinearTopSpace
for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
proofend;

Lm14:  for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is continuous
proofend;

registration
let X be LinearTopSpace;
let r be non zero Real;
cluster mlt (r,X) ->  being_homeomorphism ;
coherence
 mlt (r,X) is being_homeomorphism
proofend;
end;

theorem Th49: :: RLTOPSP1:49
for X being LinearTopSpace
for V being open Subset of X
for r being non zero Real holds r * V is open
proofend;

theorem Th50: :: RLTOPSP1:50
for X being LinearTopSpace
for V being closed Subset of X
for r being non zero Real holds r * V is closed
proofend;

theorem Th51: :: RLTOPSP1:51
for X being LinearTopSpace
for V being Subset of X
for r being non zero Real holds r * (Int V) = Int (r * V)
proofend;

theorem Th52: :: RLTOPSP1:52
for X being LinearTopSpace
for A being Subset of X
for r being non zero Real holds r * (Cl A) = Cl (r * A)
proofend;

theorem :: RLTOPSP1:53
for X being LinearTopSpace
for A being Subset of X st X is T_1 holds
0 * (Cl A) = Cl (0 * A)
proofend;

theorem Th54: :: RLTOPSP1:54
for X being LinearTopSpace
for x being Point of X
for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
proofend;

theorem Th55: :: RLTOPSP1:55
for X being LinearTopSpace
for V being a_neighborhood of 0. X
for r being non zero Real holds r * V is a_neighborhood of 0. X
proofend;

Lm15:  for X being LinearTopSpace
for V being bounded Subset of X
for r being Real holds r * V is bounded
proofend;

registration
let X be LinearTopSpace;
let V be bounded Subset of X;
let r be Real;
clusterr * V ->  bounded ;
coherence
 r * V is bounded by Lm15;
end;

theorem Th56: :: RLTOPSP1:56
for X being LinearTopSpace
for W being a_neighborhood of 0. X ex U being open a_neighborhood of 0. X st
( U is symmetric &amp; U + U c= W )
proofend;

theorem Th57: :: RLTOPSP1:57
for X being 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
proofend;

theorem Th58: :: RLTOPSP1:58
for X being LinearTopSpace
for B being local_base of X
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B &amp; Cl W c= V )
proofend;

theorem Th59: :: RLTOPSP1:59
for X being LinearTopSpace
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V
proofend;

registration
cluster non empty TopSpace-like T_1 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous  ->  Hausdorff for RLTopStruct ;
coherence
 for b1 being LinearTopSpace st b1 is T_1 holds
b1 is Hausdorff
proofend;
end;

theorem :: RLTOPSP1:60
for X being LinearTopSpace
for A being Subset of X holds Cl A = meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }
proofend;

theorem Th61: :: RLTOPSP1:61
for X being LinearTopSpace
for A, B being Subset of X holds (Int A) + (Int B) c= Int (A + B)
proofend;

theorem Th62: :: RLTOPSP1:62
for X being LinearTopSpace
for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
proofend;

Lm16:  for X being LinearTopSpace
for C being convex Subset of X holds Cl C is convex
proofend;

registration
let X be LinearTopSpace;
let C be convex Subset of X;
cluster Cl C ->  convex ;
coherence
 Cl C is convex by Lm16;
end;

Lm17:  for X being LinearTopSpace
for C being convex Subset of X holds Int C is convex
proofend;

registration
let X be LinearTopSpace;
let C be convex Subset of X;
cluster Int C ->  convex ;
coherence
 Int C is convex by Lm17;
end;

Lm18:  for X being LinearTopSpace
for B being circled Subset of X holds Cl B is circled
proofend;

registration
let X be LinearTopSpace;
let B be circled Subset of X;
cluster Cl B ->  circled ;
coherence
 Cl B is circled by Lm18;
end;

theorem :: RLTOPSP1:63
for X being LinearTopSpace
for B being circled Subset of X st 0. X in Int B holds
Int B is circled
proofend;

Lm19:  for X being LinearTopSpace
for E being bounded Subset of X holds Cl E is bounded
proofend;

registration
let X be LinearTopSpace;
let E be bounded Subset of X;
cluster Cl E ->  bounded ;
coherence
 Cl E is bounded by Lm19;
end;

Lm20:  for X being LinearTopSpace
for U, V being a_neighborhood of 0. X
for F being Subset-Family of X
for r being positive Real st ( for s being Real st abs s < r holds
s * V c= U ) &amp; F =  {  (a * V) where a is Real : abs a < r  }  holds
( union F is a_neighborhood of 0. X &amp; union F is circled &amp; union F c= U )
proofend;

theorem Th64: :: RLTOPSP1:64
for X being LinearTopSpace
for U being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W is circled &amp; W c= U )
proofend;

theorem Th65: :: RLTOPSP1:65
for X being LinearTopSpace
for U being a_neighborhood of 0. X st U is convex holds
ex W being a_neighborhood of 0. X st
( W is circled &amp; W is convex &amp; W c= U )
proofend;

theorem :: RLTOPSP1:66
for X being LinearTopSpace ex P being local_base of X st P is circled-membered
proofend;

theorem :: RLTOPSP1:67
for X being LinearTopSpace st X is locally-convex holds
ex P being local_base of X st P is convex-membered
proofend;

begin

theorem Th68: :: RLTOPSP1:68
for V being RealLinearSpace
for v, w being Point of V holds v in LSeg (v,w)
proofend;

theorem :: RLTOPSP1:69
for V being RealLinearSpace
for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)
proofend;

theorem :: RLTOPSP1:70
for V being RealLinearSpace
for v being Point of V holds LSeg (v,v) = {v}
proofend;

theorem :: RLTOPSP1:71
for V being RealLinearSpace
for v, w being Point of V st 0. V in LSeg (v,w) holds
ex r being Real st
( v = r * w or w = r * v )
proofend;