:: by Czes{\l}aw Byli\'nski

::

:: Received October 6, 2004

:: Copyright (c) 2004-2017 Association of Mizar Users

theorem :: RLTOPSP1:1

reconsider jj = 1 as positive Real ;

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 )

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

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

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

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)

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)

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

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

for M being Subset of X

for x being Point of X st x in M holds

0. X in (- x) + M

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

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

for V1, V2 being Subset of X st 0. X in V2 holds

V1 c= V1 + V2

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

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)

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

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;

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

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

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

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

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

theorem :: RLTOPSP1:17

for X being RealLinearSpace

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

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)

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

for M1, M2 being Subset of X st M1 c= M2 holds

Convex-Family M2 c= Convex-Family M1

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

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;

{ (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } is Subset of X

for b_{1} being Subset of X

for v, w being Point of X st b_{1} = { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } holds

b_{1} = { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) }

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

{ (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } is Subset of X

proof end;

commutativity for b

for v, w being Point of X st b

b

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

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;

coherence

( not LSeg (v,w) is empty & LSeg (v,w) is convex )

end;
let v, w be Point of X;

coherence

( not LSeg (v,w) is empty & LSeg (v,w) is convex )

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

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;

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

for M being Subset of V st M in P holds

M is convex ;

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

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 ;

existence

ex b_{1} being Subset-Family of V st

( not b_{1} is empty & b_{1} is convex-membered )

end;
existence

ex b

( not b

proof end;

theorem :: RLTOPSP1:23

for V being non empty RLSStruct

for F being convex-membered Subset-Family of V holds meet F is convex

for F being convex-membered Subset-Family of V holds meet F is convex

proof end;

definition
end;

:: deftheorem defines - RLTOPSP1:def 4 :

for X being non empty RLSStruct

for A being Subset of X holds - A = (- 1) * A;

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

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;

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

for X being non empty RLSStruct

for A being Subset of X holds

( A is symmetric iff A = - A );

registration

let X be RealLinearSpace;

existence

ex b_{1} being Subset of X st

( not b_{1} is empty & b_{1} is symmetric )

end;
existence

ex b

( not b

proof 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

for A being symmetric Subset of X

for x being Point of X st x in A holds

- x in A

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

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 ;

coherence

for b_{1} being Subset of X st b_{1} is empty holds

b_{1} is circled
by CONVEX1:33;

end;
coherence

for b

b

registration

let X be RealLinearSpace;

existence

ex b_{1} being Subset of X st

( not b_{1} is empty & b_{1} is circled )

end;
existence

ex b

( not b

proof end;

Lm5: for X being RealLinearSpace

for A, B being circled Subset of X holds A + B is circled

proof end;

registration
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

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;

coherence

for b_{1} being Subset of X st b_{1} is circled holds

b_{1} is symmetric
by Lm6;

end;
coherence

for b

b

Lm7: for X being RealLinearSpace

for M being circled Subset of X holds conv M is circled

proof end;

registration
end;

definition

let X be non empty RLSStruct ;

let F be Subset-Family of X;

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

for V being Subset of X st V in F holds

V is circled ;

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

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 ;

existence

ex b_{1} being Subset-Family of V st

( not b_{1} is empty & b_{1} is circled-membered )

end;
existence

ex b

( not b

proof end;

theorem :: RLTOPSP1:29

for X being non empty RLSStruct

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

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

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

proof end;

definition

attr c_{1} is strict ;

struct RLTopStruct -> RLSStruct , TopStruct ;

aggr RLTopStruct(# carrier, ZeroF, addF, Mult, topology #) -> RLTopStruct ;

end;
struct RLTopStruct -> RLSStruct , TopStruct ;

aggr RLTopStruct(# carrier, ZeroF, addF, Mult, topology #) -> RLTopStruct ;

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;

coherence

not RLTopStruct(# X,O,F,G,T #) is empty ;

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

coherence

not RLTopStruct(# X,O,F,G,T #) is empty ;

registration
end;

definition

let X be non empty RLTopStruct ;

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

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

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

ex b_{1} being non empty RLTopStruct st

( b_{1} is strict & b_{1} is add-continuous & b_{1} is Mult-continuous & b_{1} is TopSpace-like & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital )
end;

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

( b

proof 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

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

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;

ex b_{1} being Function of X,X st

for x being Point of X holds b_{1} . x = a + x

for b_{1}, b_{2} being Function of X,X st ( for x being Point of X holds b_{1} . x = a + x ) & ( for x being Point of X holds b_{2} . x = a + x ) holds

b_{1} = b_{2}

end;
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 for x being Point of X holds it . x = a + x;

ex b

for x being Point of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines transl RLTOPSP1:def 10 :

for X being non empty RLTopStruct

for a being Point of X

for b_{3} being Function of X,X holds

( b_{3} = transl (a,X) iff for x being Point of X holds b_{3} . x = a + x );

for X being non empty RLTopStruct

for a being Point of X

for b

( b

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

for a being Point of X

for V being Subset of X holds (transl (a,X)) .: V = a + V

proof end;

Lm8: for X being LinearTopSpace

for a being Point of X holds transl (a,X) is one-to-one

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;

coherence

transl (a,X) is being_homeomorphism

end;
let a be Point of X;

coherence

transl (a,X) is being_homeomorphism

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

coherence

x + E is open by Lm10;

end;
let E be open Subset of X;

let x be Point of X;

coherence

x + E is open by Lm10;

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;

coherence

K + E is open by Lm11;

end;
let E be open Subset of X;

let K be Subset of X;

coherence

K + E is open by Lm11;

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;

coherence

x + D is closed by Lm12;

end;
let D be closed Subset of X;

let x be Point of X;

coherence

x + D is closed by Lm12;

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

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)

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)

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

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

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 ;

end;
attr X is locally-convex means :: RLTOPSP1:def 11

ex P being local_base of X st P is convex-membered ;

ex P being local_base of X st P is convex-membered ;

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

for X being non empty RLTopStruct holds

( X is locally-convex iff ex P being local_base of X st P is convex-membered );

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

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;

coherence

for b_{1} being Subset of X st b_{1} is empty holds

b_{1} is bounded

end;
coherence

for b

b

proof end;

registration
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

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

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

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

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;

ex b_{1} being Function of X,X st

for x being Point of X holds b_{1} . x = r * x

for b_{1}, b_{2} being Function of X,X st ( for x being Point of X holds b_{1} . x = r * x ) & ( for x being Point of X holds b_{2} . x = r * x ) holds

b_{1} = b_{2}

end;
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 for x being Point of X holds it . x = r * x;

ex b

for x being Point of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines mlt RLTOPSP1:def 13 :

for X being non empty RLTopStruct

for r being Real

for b_{3} being Function of X,X holds

( b_{3} = mlt (r,X) iff for x being Point of X holds b_{3} . x = r * x );

for X being non empty RLTopStruct

for r being Real

for b

( b

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

for V being Subset of X

for r being non zero Real holds (mlt (r,X)) .: V = r * V

proof end;

Lm13: for X being LinearTopSpace

for r being non zero Real holds mlt (r,X) is one-to-one

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;

coherence

mlt (r,X) is being_homeomorphism

end;
let r be non zero Real;

coherence

mlt (r,X) is being_homeomorphism

proof 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

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

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)

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)

for A being Subset of X

for r being non zero Real holds r * (Cl A) = Cl (r * 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

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

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;

coherence

r * V is bounded by Lm15;

end;
let V be bounded Subset of X;

let r be Real;

coherence

r * V is bounded by Lm15;

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 )

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

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 )

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

for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V

proof end;

registration

for b_{1} being LinearTopSpace st b_{1} is T_1 holds

b_{1} is Hausdorff
end;

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

b

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

for A being Subset of X holds Cl A = meet { (A + V) where V is a_neighborhood of 0. X : verum }

proof end;

Lm16: for X being LinearTopSpace

for C being convex Subset of X holds Cl C is convex

proof end;

registration
end;

Lm17: for X being LinearTopSpace

for C being convex Subset of X holds Int C is convex

proof end;

registration
end;

Lm18: for X being LinearTopSpace

for B being circled Subset of X holds Cl B is circled

proof end;

registration
end;

Lm19: for X being LinearTopSpace

for E being bounded Subset of X holds Cl E is bounded

proof end;

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

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 )

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 st X is locally-convex holds

ex P being local_base of X st P is convex-membered ;

ex P being local_base of X st P is convex-membered ;

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 )

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;

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

for b_{1} being Subset of V

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

b_{1} = { (((1 - r) * w) + (r * v)) where r is Real : verum }

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

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

proof end;

commutativity for b

for v, w being Point of V st b

b

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

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

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

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)

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;

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

ex x1, x2 being Element of V st A = Line (x1,x2);

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

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

registration

let V be non trivial RealLinearSpace;

existence

ex b_{1} being Subset of V st

( not b_{1} is trivial & b_{1} is being_line )

end;
existence

ex b

( not b

proof end;

definition

let V be RealLinearSpace;

let x1, x2, x3 be Point of V;

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

ex L being line of V st

( x1 in L & x2 in L & x3 in L );

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

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;

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

ex L being line of V st

( x1 in L & x2 in L & x3 in L & x4 in L );

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

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

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;

registration

let V be RealLinearSpace;

let v be Point of V;

coherence

for b_{1} being Subset of V st b_{1} = {v} holds

b_{1} is being_line

coherence

Line (v,w) is being_line ;

end;
let v be Point of V;

coherence

for b

b

proof end;

let w be Point of V;coherence

Line (v,w) is being_line ;

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

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

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)

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

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;