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

::

:: Received October 6, 2004

:: Copyright (c) 2004 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 ;

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 b_{1} being Real holds b_{1} is empty

end;
existence

not for b

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

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;

theorem Th10: :: RLTOPSP1:10

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 Th13: :: RLTOPSP1:13

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;

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 )

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

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

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

end;
let M be empty Subset of X;

cluster conv M -> empty ;

coherence

conv M is empty

proof end;

theorem :: RLTOPSP1:17

canceled;

theorem :: RLTOPSP1:18

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)

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

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

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

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

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

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 )

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

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 )

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

:: 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 b_{1} being Subset-Family of V st

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

end;
cluster non empty convex-membered Element of bool (bool the carrier of V);

existence

ex b

( not b

proof end;

theorem :: RLTOPSP1:24

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

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;
let A be Subset of X;

func - A -> Subset of X equals :: RLTOPSP1:def 4

(- 1) * A;

coherence

(- 1) * A is Subset of X ;

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

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;
let A be Subset of X;

attr A is symmetric means :Def5: :: RLTOPSP1:def 5

A = - A;

:: 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 b_{1} being Subset of X st

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

end;
cluster non empty symmetric Element of bool the carrier of X;

existence

ex b

( not b

proof 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

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

:: 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 b_{1} being Subset of X st b_{1} is empty holds

b_{1} is circled

end;
cluster empty -> circled Element of bool the carrier of X;

coherence

for b

b

proof end;

theorem Th27: :: RLTOPSP1:27

proof end;

registration

let X be RealLinearSpace;

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

existence

ex b_{1} being Subset of X st

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

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

existence

ex b

( not b

proof end;

theorem Th28: :: RLTOPSP1:28

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;
let A, B be circled Subset of X;

cluster A + B -> circled ;

coherence

A + B is circled by Lm5;

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

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 b_{1} being Subset of X st b_{1} is circled holds

b_{1} is symmetric
by Lm6;

end;
cluster circled -> symmetric Element of bool the carrier of X;

coherence

for b

b

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;
let M be circled Subset of X;

cluster conv M -> circled ;

coherence

conv M is circled by Lm7;

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

:: 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 b_{1} being Subset-Family of V st

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

end;
cluster non empty circled-membered Element of bool (bool the carrier of V);

existence

ex b

( not b

proof end;

theorem :: RLTOPSP1:30

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

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;

begin

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;

cluster RLTopStruct(# X,O,F,G,T #) -> non empty ;

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;

cluster RLTopStruct(# X,O,F,G,T #) -> non empty ;

coherence

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

registration

cluster non empty strict RLTopStruct ;

existence

ex b_{1} being RLTopStruct st

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

end;
existence

ex b

( b

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

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

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

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

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

( b

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

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

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

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

end;
let a be Point of X;

cluster transl (a,X) -> being_homeomorphism ;

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;

cluster x + E -> open ;

coherence

x + E is open by Lm10;

end;
let E be open Subset of X;

let x be Point of X;

cluster x + E -> open ;

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;

cluster K + E -> open ;

coherence

K + E is open by Lm11;

end;
let E be open Subset of X;

let K be Subset of X;

cluster K + E -> open ;

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;

cluster x + D -> closed ;

coherence

x + D is closed by Lm12;

end;
let D be closed Subset of X;

let x be Point of X;

cluster x + D -> closed ;

coherence

x + D is closed by Lm12;

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

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)

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)

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

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

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 ;

attr X is locally-convex means :Def11: :: RLTOPSP1:def 11

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

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

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

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

:: 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 b_{1} being Subset of X st b_{1} is empty holds

b_{1} is bounded

end;
cluster empty -> bounded Element of bool the carrier of X;

coherence

for b

b

proof end;

registration

let X be LinearTopSpace;

cluster bounded Element of bool the carrier of X;

existence

ex b_{1} being Subset of X st b_{1} is bounded

end;
cluster bounded Element of bool the carrier of X;

existence

ex b

proof end;

theorem Th42: :: RLTOPSP1:42

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

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

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

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

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

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

( b

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

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

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

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

end;
let r be non zero Real;

cluster mlt (r,X) -> being_homeomorphism ;

coherence

mlt (r,X) is being_homeomorphism

proof 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

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

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)

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)

for A being Subset of X

for r being non zero Real holds r * (Cl A) = Cl (r * A)

proof end;

theorem :: RLTOPSP1:54

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

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

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;
let V be bounded Subset of X;

let r be Real;

cluster r * V -> bounded ;

coherence

r * V is bounded by Lm15;

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 )

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

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 )

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

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 b_{1} being LinearTopSpace st b_{1} is T_1 holds

b_{1} is T_2

end;
coherence

for b

b

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

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

proof end;

theorem Th63: :: RLTOPSP1:63

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;
let C be convex Subset of X;

cluster Cl C -> convex ;

coherence

Cl C is convex by Lm16;

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;
let C be convex Subset of X;

cluster Int C -> convex ;

coherence

Int C is convex by Lm17;

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;
let B be circled Subset of X;

cluster Cl B -> circled ;

coherence

Cl B is circled by Lm18;

theorem :: RLTOPSP1:64

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;
let E be bounded Subset of X;

cluster Cl E -> bounded ;

coherence

Cl E is bounded by Lm19;

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 )

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 )

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

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

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

proof end;

begin

theorem Th69: :: RLTOPSP1:69

proof end;

theorem :: RLTOPSP1:70

proof end;

theorem :: RLTOPSP1:71

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 )

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;