:: Introduction to Real Linear Topological Spaces
:: by Czes{\l}aw Byli\'nski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2011 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 Element of REAL ;
existence
not for b1 being Real holds b1 is empty
proof end;
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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

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)
proof end;

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
proof end;

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 & r <= 1 & u in M & 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 & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M )
proof end;
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 & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M );

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

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

theorem :: RLTOPSP1:17
canceled;

theorem :: RLTOPSP1:18
for X being RealLinearSpace
for M being convex Subset of X holds conv M = M
proof end;

theorem Th19: :: RLTOPSP1:19
for X being RealLinearSpace
for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
proof end;

theorem Th20: :: RLTOPSP1:20
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
Convex-Family M2 c= Convex-Family M1
proof end;

theorem Th21: :: RLTOPSP1:21
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
conv M1 c= conv M2
proof end;

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

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 & r <= 1 ) } ;
coherence
{ (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } is Subset of X
proof end;
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 & r <= 1 ) } holds
b1 = { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) }
proof end;
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 & 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 & LSeg (v,w) is convex )
proof end;
end;

theorem :: RLTOPSP1:23
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 & w in M holds
LSeg (u,w) c= M )
proof end;

definition
let V be non empty RLSStruct ;
let P be Subset-Family of V;
attr P 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 Element of bool (bool the carrier of V);
existence
ex b1 being Subset-Family of V st
( not b1 is empty & b1 is convex-membered )
proof end;
end;

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

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 Th25: :: RLTOPSP1:25
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) )
proof end;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attr A 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 Element of bool the carrier of X;
existence
ex b1 being Subset of X st
( not b1 is empty & b1 is symmetric )
proof end;
end;

theorem Th26: :: RLTOPSP1:26
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
proof end;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attr A 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 Element of bool the carrier of X;
coherence
for b1 being Subset of X st b1 is empty holds
b1 is circled
proof end;
end;

theorem Th27: :: RLTOPSP1:27
for X being RealLinearSpace holds {(0. X)} is circled
proof end;

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

theorem Th28: :: RLTOPSP1:28
for X being RealLinearSpace
for B being non empty circled Subset of X holds 0. X in B
proof end;

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

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

theorem Th29: :: RLTOPSP1:29
for X being RealLinearSpace
for A being circled Subset of X
for r being Real st abs r = 1 holds
r * A = A
proof end;

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

registration
let X be RealLinearSpace;
cluster circled -> symmetric 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
proof end;

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;
attr F 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 Element of bool (bool the carrier of V);
existence
ex b1 being Subset-Family of V st
( not b1 is empty & b1 is circled-membered )
proof end;
end;

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

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

begin

definition
attr c1 is strict ;
struct RLTopStruct -> RLSStruct , TopStruct ;
aggr RLTopStruct(# 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 RLTopStruct ;
existence
ex b1 being RLTopStruct st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let X be non empty RLTopStruct ;
attr X 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 & x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V );
attr X 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 & a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open & x in W & ( 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 & x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & 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 & a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open & x in W & ( 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 RLTopStruct ;
existence
ex b1 being non empty RLTopStruct st
( b1 is strict & b1 is add-continuous & b1 is Mult-continuous & b1 is TopSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital )
proof end;
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 Th32: :: RLTOPSP1:32
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
proof end;

theorem Th33: :: RLTOPSP1:33
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
proof end;

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
proof end;
uniqueness
for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = a + x ) & ( for x being Point of X holds b2 . x = a + x ) holds
b1 = b2
proof end;
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 Th34: :: RLTOPSP1:34
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
proof end;

theorem Th35: :: RLTOPSP1:35
for X being LinearTopSpace
for a being Point of X holds rng (transl (a,X)) = [#] X
proof end;

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

theorem Th36: :: RLTOPSP1:36
for X being LinearTopSpace
for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
proof end;

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

registration
let X be LinearTopSpace;
let a be Point of X;
cluster transl (a,X) -> being_homeomorphism ;
coherence
transl (a,X) is being_homeomorphism
proof end;
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
proof end;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let x be Point of X;
cluster x + 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
proof end;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let K be Subset of X;
cluster K + 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
proof end;

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

theorem Th37: :: RLTOPSP1:37
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
proof end;

theorem Th38: :: RLTOPSP1:38
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Int V) = Int (x + V)
proof end;

theorem :: RLTOPSP1:39
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
proof end;

theorem :: RLTOPSP1:40
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
proof end;

theorem :: RLTOPSP1:41
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
proof end;

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 ;
attr X 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;
attr E is bounded means :Def12: :: RLTOPSP1:def 12
 for V being a_neighborhood of 0. X ex s being Real st
( s > 0 & ( 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 & ( for t being Real st t > s holds
E c= t * V ) ) );

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

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

theorem Th42: :: RLTOPSP1:42
for X being LinearTopSpace
for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded
proof end;

theorem :: RLTOPSP1:43
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
proof end;

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

theorem Th45: :: RLTOPSP1:45
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
proof end;

theorem :: RLTOPSP1:46
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
proof end;

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
proof end;
uniqueness
for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = r * x ) & ( for x being Point of X holds b2 . x = r * x ) holds
b1 = b2
proof end;
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 Th47: :: RLTOPSP1:47
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
proof end;

theorem Th48: :: RLTOPSP1:48
for X being LinearTopSpace
for r being non zero Real holds rng (mlt (r,X)) = [#] X
proof end;

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

theorem Th49: :: RLTOPSP1:49
for X being LinearTopSpace
for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
proof end;

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

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

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

theorem Th51: :: RLTOPSP1:51
for X being LinearTopSpace
for V being closed Subset of X
for r being non zero Real holds r * V is closed
proof end;

theorem Th52: :: RLTOPSP1:52
for X being LinearTopSpace
for V being Subset of X
for r being non zero Real holds r * (Int V) = Int (r * V)
proof end;

theorem Th53: :: RLTOPSP1:53
for X being LinearTopSpace
for A being Subset of X
for r being non zero Real holds r * (Cl A) = Cl (r * A)
proof end;

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

theorem Th55: :: RLTOPSP1:55
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
proof end;

theorem Th56: :: RLTOPSP1:56
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
proof end;

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

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

theorem Th57: :: RLTOPSP1:57
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 & U + U c= W )
proof end;

theorem Th58: :: RLTOPSP1:58
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
proof end;

theorem Th59: :: RLTOPSP1:59
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 & Cl W c= V )
proof end;

theorem Th60: :: RLTOPSP1:60
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
proof end;

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 RLTopStruct ;
coherence
for b1 being LinearTopSpace st b1 is T_1 holds
b1 is T_2
proof end;
end;

theorem :: RLTOPSP1:61
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 }
proof end;

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

theorem Th63: :: RLTOPSP1:63
for X being LinearTopSpace
for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
proof end;

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

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
proof end;

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
proof end;

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:64
for X being LinearTopSpace
for B being circled Subset of X st 0. X in Int B holds
Int B is circled
proof end;

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

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 ) & F = { (a * V) where a is Real : abs a < r } holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
proof end;

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

theorem Th66: :: RLTOPSP1:66
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 & W is convex & W c= U )
proof end;

theorem :: RLTOPSP1:67
for X being LinearTopSpace ex P being local_base of X st P is circled-membered
proof end;

theorem :: RLTOPSP1:68
for X being LinearTopSpace st X is locally-convex holds
ex P being local_base of X st P is convex-membered
proof end;

begin

theorem Th69: :: RLTOPSP1:69
for V being RealLinearSpace
for v, w being Point of V holds v in LSeg (v,w)
proof end;

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

theorem :: RLTOPSP1:71
for V being RealLinearSpace
for v being Point of V holds LSeg (v,v) = {v}
proof end;

theorem :: RLTOPSP1:72
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 )
proof end;