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

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 ;

reconsider jj = 1 as positive Real ;

registration

cluster ext-real non zero complex V41() for object ;

existence
not for b₁ being Real holds b₁ is zero

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

for X being RealLinearSpace
for M being convex Subset of X holds conv M = M by CONVEX1:30, CONVEX1:41;

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)

proof end;

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

proof end;

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

proof end;

theorem :: RLTOPSP1:21

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 b₁ being Subset of X
for v, w being Point of X st b₁ = { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } holds
b₁ = { (((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: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 & 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 for Element of bool (bool the carrier of V);

existence
ex b₁ being Subset-Family of V st
( not b₁ is empty & b₁ is convex-membered )

proof end;

end;

theorem :: RLTOPSP1:23

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 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) )

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 for Element of bool the carrier of X;

existence
ex b₁ being Subset of X st
( not b₁ is empty & b₁ is symmetric )

proof end;

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

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 |.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 |.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 b₁ being Subset of X st b₁ is empty holds
b₁ is circled by CONVEX1:33;

end;

theorem Th26: :: RLTOPSP1:26

for X being RealLinearSpace holds {(0. X)} is circled by Th13;

registration

let X be RealLinearSpace;

cluster non empty circled for Element of bool the carrier of X;

existence
ex b₁ being Subset of X st
( not b₁ is empty & b₁ is circled )

proof end;

end;

theorem Th27: :: RLTOPSP1:27

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 Th28: :: RLTOPSP1:28

for X being RealLinearSpace
for A being circled Subset of X
for r being Real st |.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 for Element of bool the carrier of X;

coherence
for b₁ being Subset of X st b₁ is circled holds
b₁ 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 for Element of bool (bool the carrier of V);

existence
ex b₁ being Subset-Family of V st
( not b₁ is empty & b₁ is circled-membered )

proof end;

end;

theorem :: RLTOPSP1:29

for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds union F is circled

proof end;

theorem :: RLTOPSP1:30

for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds meet F is circled

proof end;

definition

attr c₁ 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 for RLTopStruct ;

existence
ex b₁ being RLTopStruct st
( b₁ is strict & not b₁ 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 |.(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 |.(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 b₁ being non empty RLTopStruct st
( b₁ is strict & b₁ is add-continuous & b₁ is Mult-continuous & b₁ is TopSpace-like & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ 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 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

proof end;

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 |.(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 b₁ being Function of X,X st
for x being Point of X holds b₁ . x = a + x

proof end;

uniqueness
for b₁, b₂ being Function of X,X st ( for x being Point of X holds b₁ . x = a + x ) & ( for x being Point of X holds b₂ . x = a + x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines transl RLTOPSP1:def 10 :
for X being non empty RLTopStruct
for a being Point of X
for b₃ being Function of X,X holds
( b₃ = transl (a,X) iff for x being Point of X holds b₃ . 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

proof end;

theorem Th34: :: RLTOPSP1:34

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 Th35: :: RLTOPSP1:35

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 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

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

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 :: RLTOPSP1:def 11
ex P being local_base of X st P is convex-membered ;

end;

:: deftheorem 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 for Element of bool the carrier of X;

coherence
for b₁ being Subset of X st b₁ is empty holds
b₁ is bounded

proof end;

end;

registration

let X be LinearTopSpace;

cluster bounded for Element of bool the carrier of X;

existence
ex b₁ being Subset of X st b₁ is bounded

proof end;

end;

theorem Th41: :: RLTOPSP1:41

for X being LinearTopSpace
for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded

proof end;

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

proof end;

theorem :: RLTOPSP1:43

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 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

proof end;

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

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 b₁ being Function of X,X st
for x being Point of X holds b₁ . x = r * x

proof end;

uniqueness
for b₁, b₂ being Function of X,X st ( for x being Point of X holds b₁ . x = r * x ) & ( for x being Point of X holds b₂ . x = r * x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines mlt RLTOPSP1:def 13 :
for X being non empty RLTopStruct
for r being Real
for b₃ being Function of X,X holds
( b₃ = mlt (r,X) iff for x being Point of X holds b₃ . 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

proof end;

theorem Th47: :: RLTOPSP1:47

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 Th48: :: RLTOPSP1:48

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 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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

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 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 & U + U c= W )

proof end;

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

proof end;

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 & Cl W c= V )

proof end;

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

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 for RLTopStruct ;

coherence
for b₁ being LinearTopSpace st b₁ is T_1 holds
b₁ is Hausdorff

proof end;

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 }

proof end;

theorem Th61: :: RLTOPSP1:61

for X being LinearTopSpace
for A, B being Subset of X holds (Int A) + (Int B) c= Int (A + B)

proof end;

theorem Th62: :: RLTOPSP1:62

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:63

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

proof end;

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 & W c= U )

proof end;

theorem :: 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 & W is convex & W c= U )

proof end;

theorem :: RLTOPSP1:66

for X being LinearTopSpace ex P being local_base of X st P is circled-membered

proof end;

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 ;

theorem Th68: :: RLTOPSP1:68

for V being RealLinearSpace
for v, w being Point of V holds v in LSeg (v,w)

proof end;

theorem :: RLTOPSP1:69

for V being RealLinearSpace
for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)

proof end;

theorem :: RLTOPSP1:70

for V being RealLinearSpace
for v being Point of V holds LSeg (v,v) = {v}

proof end;

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 )

proof end;

:: from EUCLID_4 (generalized), A.T.

definition

let V be RealLinearSpace;
let v, w be Point of V;

func Line (v,w) -> Subset of V equals :: RLTOPSP1:def 14
{ (((1 - r) * v) + (r * w)) where r is Real : verum } ;

coherence
{ (((1 - r) * v) + (r * w)) where r is Real : verum } is Subset of V

proof end;

commutativity
for b₁ being Subset of V
for v, w being Point of V st b₁ = { (((1 - r) * v) + (r * w)) where r is Real : verum } holds
b₁ = { (((1 - r) * w) + (r * v)) where r is Real : verum }

proof end;

end;

:: deftheorem defines Line RLTOPSP1:def 14 :
for V being RealLinearSpace
for v, w being Point of V holds Line (v,w) = { (((1 - r) * v) + (r * w)) where r is Real : verum } ;

theorem Th72: :: RLTOPSP1:72

for V being RealLinearSpace
for v, w being Point of V holds v in Line (v,w)

proof end;

registration

let V be RealLinearSpace;
let v, w be Point of V;

cluster Line (v,w) -> non empty ;

coherence
not Line (v,w) is empty by Th72;

end;

theorem :: RLTOPSP1:73

for V being RealLinearSpace
for v, w being Point of V holds LSeg (v,w) c= Line (v,w)

proof end;

theorem Th74: :: RLTOPSP1:74

for V being RealLinearSpace
for x1, x2, y1, y2 being Element of V st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
Line (y1,y2) c= Line (x1,x2)

proof end;

theorem Th75: :: RLTOPSP1:75

for V being RealLinearSpace
for x1, x2, y1, y2 being Element of V st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (y1,y2) = Line (x1,x2)

proof end;

:: 12.11.28, A.T.

definition

let V be RealLinearSpace;
let A be Subset of V;

attr A is being_line means :Def15: :: RLTOPSP1:def 15
ex x1, x2 being Element of V st A = Line (x1,x2);

end;

:: deftheorem Def15 defines being_line RLTOPSP1:def 15 :
for V being RealLinearSpace
for A being Subset of V holds
( A is being_line iff ex x1, x2 being Element of V st A = Line (x1,x2) );

registration

let V be RealLinearSpace;

cluster being_line for Element of bool the carrier of V;

existence
ex b₁ being Subset of V st b₁ is being_line

proof end;

end;

registration

let V be non trivial RealLinearSpace;

cluster non trivial being_line for Element of bool the carrier of V;

existence
ex b₁ being Subset of V st
( not b₁ is trivial & b₁ is being_line )

proof end;

end;

definition

let V be RealLinearSpace;
mode line of V is being_line Subset of V;

end;

definition

let V be RealLinearSpace;
let x1, x2, x3 be Point of V;

pred x1,x2,x3 are_collinear means :: RLTOPSP1:def 16
ex L being line of V st
( x1 in L & x2 in L & x3 in L );

end;

:: deftheorem defines are_collinear RLTOPSP1:def 16 :
for V being RealLinearSpace
for x1, x2, x3 being Point of V holds
( x1,x2,x3 are_collinear iff ex L being line of V st
( x1 in L & x2 in L & x3 in L ) );

definition

let V be RealLinearSpace;
let x1, x2, x3, x4 be Point of V;

pred x1,x2,x3,x4 are_collinear means :: RLTOPSP1:def 17
ex L being line of V st
( x1 in L & x2 in L & x3 in L & x4 in L );

end;

:: deftheorem defines are_collinear RLTOPSP1:def 17 :
for V being RealLinearSpace
for x1, x2, x3, x4 being Point of V holds
( x1,x2,x3,x4 are_collinear iff ex L being line of V st
( x1 in L & x2 in L & x3 in L & x4 in L ) );

theorem :: RLTOPSP1:76

for V being RealLinearSpace
for v, w being Point of V
for x being object st x in LSeg (v,w) holds
ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) )

proof end;

theorem Th77: :: RLTOPSP1:77

for V being RealLinearSpace
for v being Point of V holds Line (v,v) = {v}

proof end;

registration

let V be RealLinearSpace;
let v be Point of V;

cluster {v} -> being_line for Subset of V;

coherence
for b₁ being Subset of V st b₁ = {v} holds
b₁ is being_line

proof end;

let w be Point of V;

cluster Line (v,w) -> being_line ;

coherence
Line (v,w) is being_line ;

end;

theorem :: RLTOPSP1:78

for V being non trivial RealLinearSpace
for L being non trivial line of V ex p, q being Point of V st
( p <> q & L = Line (p,q) )

proof end;

theorem :: RLTOPSP1:79

for V being RealLinearSpace
for x1, x2, x3, x4 being Point of V st x1,x2,x3,x4 are_collinear holds
( x1,x2,x3 are_collinear & x1,x2,x4 are_collinear ) ;

theorem Th80: :: RLTOPSP1:80

for V being RealLinearSpace
for L being line of V
for x1, x2 being Element of V st x1 <> x2 & x1 in L & x2 in L holds
L = Line (x1,x2)

proof end;

theorem :: RLTOPSP1:81

for V being RealLinearSpace
for x1, x2, x3, x4 being Point of V st x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear holds
x1,x2,x3,x4 are_collinear

proof end;