begin
theorem
theorem Th2:
theorem Th3:
Lm1:
for X being non empty addLoopStr
for M being Subset of
for x, y being Point of st y in M holds
x + y in x + M
Lm2:
for X being non empty addLoopStr
for M, N being Subset of holds { (x + N) where x is Point of : x in M } is Subset-Family of
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm3:
for X being non empty addLoopStr
for M, N, V being Subset of st M c= N holds
V + M c= V + N
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
:: deftheorem Def1 defines convex RLTOPSP1:def 1 :
Lm4:
for X being RealLinearSpace holds conv ({} X) = {}
theorem
canceled;
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
:: deftheorem defines LSeg RLTOPSP1:def 2 :
theorem
:: deftheorem Def3 defines convex-membered RLTOPSP1:def 3 :
theorem
:: deftheorem defines - RLTOPSP1:def 4 :
theorem Th25:
:: deftheorem Def5 defines symmetric RLTOPSP1:def 5 :
theorem Th26:
:: deftheorem Def6 defines circled RLTOPSP1:def 6 :
Lm5:
for X being non empty RLSStruct holds {} X is circled
theorem Th27:
theorem Th28:
Lm6:
for X being RealLinearSpace
for A, B being circled Subset of holds A + B is circled
theorem Th29:
Lm7:
for X being RealLinearSpace
for A being circled Subset of holds A is symmetric
Lm8:
for X being RealLinearSpace
for M being circled Subset of holds conv M is circled
:: deftheorem Def7 defines circled-membered RLTOPSP1:def 7 :
theorem
theorem
begin
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 ;
cluster RLTopStruct(#
X,
O,
F,
G,
T #)
-> non
empty ;
coherence
not RLTopStruct(# X,O,F,G,T #) is empty
;
end;
:: deftheorem Def8 defines add-continuous RLTOPSP1:def 8 :
:: deftheorem Def9 defines Mult-continuous RLTOPSP1:def 9 :
theorem Th32:
theorem Th33:
:: deftheorem Def10 defines transl RLTOPSP1:def 10 :
theorem Th34:
theorem Th35:
Lm9:
for X being LinearTopSpace
for a being Point of holds transl a,X is one-to-one
theorem Th36:
Lm10:
for X being LinearTopSpace
for a being Point of holds transl a,X is continuous
Lm11:
for X being LinearTopSpace
for E being Subset of
for x being Point of st E is open holds
x + E is open
Lm12:
for X being LinearTopSpace
for E being open Subset of
for K being Subset of holds K + E is open
Lm13:
for X being LinearTopSpace
for D being closed Subset of
for x being Point of holds x + D is closed
theorem Th37:
theorem Th38:
theorem
theorem
theorem
:: deftheorem Def11 defines locally-convex RLTOPSP1:def 11 :
:: deftheorem Def12 defines bounded RLTOPSP1:def 12 :
theorem Th42:
theorem
theorem
theorem Th45:
theorem
:: deftheorem Def13 defines mlt RLTOPSP1:def 13 :
theorem Th47:
theorem Th48:
Lm14:
for X being LinearTopSpace
for r being non zero Real holds mlt r,X is one-to-one
theorem Th49:
Lm15:
for X being LinearTopSpace
for r being non zero Real holds mlt r,X is continuous
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem Th56:
Lm16:
for X being LinearTopSpace
for V being bounded Subset of
for r being Real holds r * V is bounded
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
Lm17:
for X being LinearTopSpace
for C being convex Subset of holds Cl C is convex
Lm18:
for X being LinearTopSpace
for C being convex Subset of holds Int C is convex
Lm19:
for X being LinearTopSpace
for B being circled Subset of holds Cl B is circled
theorem
Lm20:
for X being LinearTopSpace
for E being bounded Subset of holds Cl E is bounded
Lm21:
for X being LinearTopSpace
for U, V being a_neighborhood of 0. X
for F being Subset-Family of
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 )
theorem Th65:
theorem Th66:
theorem
theorem
begin
theorem Th69:
theorem
theorem
theorem