:: Introduction to Real Linear Topological Spaces
:: by Czes{\l}aw Byli\'nski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, XBOOLE_0, RLVECT_1, SUBSET_1, PRE_TOPC, RELAT_1,
XCMPLX_0, SETFAM_1, TARSKI, ALGSTR_0, ARYTM_3, ZFMISC_1, STRUCT_0,
SUPINF_2, ARYTM_1, CONNSP_2, TOPS_1, CONVEX1, CARD_1, XXREAL_0, RELAT_2,
COMPLEX1, BINOP_1, FUNCT_1, RCOMP_1, ORDINAL2, TOPS_2, YELLOW13,
XXREAL_2, FINSET_1, RVSUM_1, EQREL_1, COMPTS_1, RLTOPSP1, FUNCT_2,
INCSP_1, AFF_1, PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, SETFAM_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, BINOP_1, REAL_1, EQREL_1, DOMAIN_1, STRUCT_0,
ALGSTR_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, YELLOW13,
RLVECT_1, RUSUB_4, CONVEX1;
constructors SETFAM_1, BINOP_1, DOMAIN_1, XXREAL_0, REAL_1, COMPLEX1, EQREL_1,
TOPS_1, TOPS_2, CONNSP_2, RUSUB_4, CONVEX1, URYSOHN1, YELLOW13, COMPTS_1,
RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, STRUCT_0, TOPS_1, RLVECT_1, CONVEX1, TOPGRP_1,
ORDINAL1, BORSUK_1, COMPTS_1, PRE_TOPC, FUNCT_2, ANPROJ_1;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, STRUCT_0, RLVECT_1, PRE_TOPC, CONNSP_2, TOPS_2,
YELLOW13, CONVEX1, ALGSTR_0, SETFAM_1, ZFMISC_1;
equalities STRUCT_0, RLVECT_1, CONVEX1, SUBSET_1, ALGSTR_0, XCMPLX_0;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, CONVEX1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, SUBSET_1, SETFAM_1, XCMPLX_1,
XREAL_0, XCMPLX_0, FUNCT_2, FUNCT_1, ABSVALUE, FINSET_1, EQREL_1,
PRE_TOPC, COMPTS_1, CONNSP_2, TOPS_1, URYSOHN1, YELLOW13, RLVECT_1,
RUSUB_4, CONVEX1, TOPGRP_1, TOPS_2, YELLOW_8, XREAL_1, TSEP_1, COMPLEX1,
XXREAL_0, XTUPLE_0, STRUCT_0;
schemes BINOP_1, FUNCT_2, SUBSET_1, EQREL_1, FINSET_1;
begin :: Preliminaries
reserve r,s,t,u for Real;
theorem
for X being non empty RLSStruct, M being Subset of X, x being Point of
X, r being Real st x in M holds r*x in r*M;
reconsider jj=1 as positive Real;
registration
cluster non zero for Real;
existence
proof
take jj;
thus thesis;
end;
end;
theorem Th2:
for T being non empty TopSpace, X being non empty Subset of T, FX
being Subset-Family of T st FX is Cover of X for x being Point of T st x in X
ex W being Subset of T st x in W & W in FX
proof
let T be non empty TopSpace, X be non empty Subset of T, FX be Subset-Family
of T;
assume FX is Cover of X;
then
A1: X c= union FX by SETFAM_1:def 11;
let x be Point of T;
assume x in X;
then consider W being set such that
A2: x in W and
A3: W in FX by A1,TARSKI:def 4;
reconsider W as Subset of T by A3;
take W;
thus thesis by A2,A3;
end;
theorem Th3:
for X being non empty addLoopStr, M,N being Subset of X, x,y
being Point of X st x in M & y in N holds x+y in M+N
proof
let X be non empty addLoopStr, M,N be Subset of X, x,y be Point of X;
M+N = {u + v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9;
hence thesis;
end;
Lm1: for X being non empty addLoopStr, M being Subset of X, x,y being Point of
X st y in M holds x+y in x+M
proof
let X be non empty addLoopStr, M be Subset of X, x,y be Point of X;
x+M = {x + u where u is Point of X: u in M} by RUSUB_4:def 8;
hence thesis;
end;
Lm2: for X being non empty addLoopStr, M,N being Subset of X holds {x+N where
x is Point of X: x in M} is Subset-Family of X
proof
let X be non empty addLoopStr, M,N be Subset of X;
set F = {u+N where u is Point of X: u in M};
F c= bool the carrier of X
proof
let x be object;
assume x in F;
then ex u being Point of X st x=u+N & u in M;
hence thesis;
end;
hence thesis;
end;
theorem Th4:
for X being non empty addLoopStr, M,N being Subset of X, 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
let X be non empty addLoopStr, M,N be Subset of X, F be Subset-Family of X;
assume
A1: F = {x+N where x is Point of X: x in M};
thus M+N c= union F
proof
let x be object;
assume x in M+N;
then x in {u+v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9;
then consider u,v being Point of X such that
A2: x = u+v and
A3: u in M and
A4: v in N;
u+N = {u + v9 where v9 is Point of X: v9 in N} by RUSUB_4:def 8;
then
A5: x in u+N by A2,A4;
u+N in F by A1,A3;
hence thesis by A5,TARSKI:def 4;
end;
let x be object;
assume x in union F;
then consider Y being set such that
A6: x in Y and
A7: Y in F by TARSKI:def 4;
consider u being Point of X such that
A8: Y = u+N and
A9: u in M by A1,A7;
u+N = {u + v where v is Point of X: v in N} by RUSUB_4:def 8;
then ex v being Point of X st x = u+v & v in N by A6,A8;
then x in {u9+v9 where u9,v9 is Point of X: u9 in M & v9 in N} by A9;
hence thesis by RUSUB_4:def 9;
end;
theorem Th5:
for X being add-associative right_zeroed right_complementable
non empty addLoopStr, M being Subset of X holds 0.X+M = M
proof
let X be add-associative right_zeroed right_complementable non empty
addLoopStr, M be Subset of X;
A1: 0.X+M = {0.X + u where u is Point of X: u in M} by RUSUB_4:def 8;
thus 0.X+M c= M
proof
let x be object;
assume x in 0.X+M;
then ex u being Point of X st x = 0.X+u & u in M by A1;
hence thesis;
end;
let x be object;
assume
A2: x in M;
then reconsider x as Point of X;
0.X+x = x;
hence thesis by A1,A2;
end;
theorem Th6:
for X being add-associative non empty addLoopStr,x,y being
Point of X, M being Subset of X holds x+y+M = x+(y+M)
proof
let X be add-associative non empty addLoopStr,x,y be Point of X, M be
Subset of X;
A1: x+(y+M) = {x+u where u is Point of X: u in y+M} by RUSUB_4:def 8;
A2: y+M = {y+u where u is Point of X: u in M} by RUSUB_4:def 8;
A3: x+y+M = {x+y+u where u is Point of X: u in M} by RUSUB_4:def 8;
thus x+y+M c= x+(y+M)
proof
let z be object;
assume z in x+y+M;
then consider u being Point of X such that
A4: x+y+u = z & u in M by A3;
x+(y+u) = z & y+u in y+M by A2,A4,RLVECT_1:def 3;
hence thesis by A1;
end;
let z be object;
assume z in x+(y+M);
then consider u being Point of X such that
A5: x+u = z and
A6: u in y+M by A1;
consider v being Point of X such that
A7: y+v = u and
A8: v in M by A2,A6;
x+y+v = z by A5,A7,RLVECT_1:def 3;
hence thesis by A3,A8;
end;
theorem Th7:
for X being add-associative non empty addLoopStr, x being Point
of X, M,N being Subset of X holds x+M+N = x+(M+N)
proof
let X be add-associative non empty addLoopStr, x be Point of X, M,N be
Subset of X;
A1: x+(M+N) = {x+u where u is Point of X: u in M+N} by RUSUB_4:def 8;
A2: x+M = {x+u where u is Point of X: u in M} by RUSUB_4:def 8;
A3: M+N = {u+v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9;
A4: x+M+N = {u+v where u,v is Point of X: u in x+M & v in N} by RUSUB_4:def 9;
thus x+M+N c= x+(M+N)
proof
let z be object;
assume z in x+M+N;
then consider u,v being Point of X such that
A5: u+v = z and
A6: u in x+M and
A7: v in N by A4;
consider u9 being Point of X such that
A8: x+u9 = u & u9 in M by A2,A6;
x+(u9+v) = z & u9+v in M+N by A3,A5,A7,A8,RLVECT_1:def 3;
hence thesis by A1;
end;
let z be object;
assume z in x+(M+N);
then consider u being Point of X such that
A9: x+u = z and
A10: u in M+N by A1;
consider w,v being Point of X such that
A11: w+v = u and
A12: w in M and
A13: v in N by A3,A10;
A14: x+w in x+M by A2,A12;
x+w+v = z by A9,A11,RLVECT_1:def 3;
hence thesis by A4,A13,A14;
end;
theorem Th8:
for X being non empty addLoopStr, M,N being Subset of X, x being
Point of X st M c= N holds x+M c= x+N
proof
let X be non empty addLoopStr, M,N be Subset of X, x be Point of X such that
A1: M c= N;
let z be object;
assume
A2: z in x+M;
then reconsider z as Point of X;
x+M = {x + u where u is Element of X: u in M} by RUSUB_4:def 8;
then ex u being Point of X st x+u = z & u in M by A2;
hence thesis by A1,Lm1;
end;
theorem Th9:
for X being add-associative right_zeroed right_complementable
non empty addLoopStr, M being Subset of X, x being Point of X st x in M holds
0.X in -x+M
proof
let X be add-associative right_zeroed right_complementable non empty
addLoopStr, M be Subset of X, x be Point of X;
assume x in M;
then -x+x in -x+M by Lm1;
hence thesis by RLVECT_1:5;
end;
theorem Th10:
for X being non empty addLoopStr, M,N,V being Subset of X st M
c= N holds M+V c= N+V
proof
let X be non empty addLoopStr, M,N,V be Subset of X such that
A1: M c= N;
let x be object;
assume x in M+V;
then x in {u + v where u,v is Point of X: u in M & v in V} by RUSUB_4:def 9;
then ex u,v being Point of X st u+v = x & u in M & v in V;
then x in {u9 + v9 where u9,v9 is Point of X: u9 in N & v9 in V} by A1;
hence thesis by RUSUB_4:def 9;
end;
Lm3: for X being non empty addLoopStr, M,N,V being Subset of X st M c= N holds
V+M c= V+N
proof
let X be non empty addLoopStr, M,N,V be Subset of X such that
A1: M c= N;
let x be object;
assume x in V+M;
then x in {u + v where u,v is Point of X: u in V & v in M} by RUSUB_4:def 9;
then ex u,v being Point of X st u+v = x & u in V & v in M;
then x in {u9 + v9 where u9,v9 is Point of X: u9 in V & v9 in N} by A1;
hence thesis by RUSUB_4:def 9;
end;
theorem Th11:
for X being non empty addLoopStr, V1,V2,W1,W2 being Subset of X
st V1 c= W1 & V2 c= W2 holds V1+V2 c= W1+W2
proof
let X be non empty addLoopStr, V1,V2,W1,W2 be Subset of X such that
A1: V1 c= W1 & V2 c= W2;
let x be object;
assume x in V1+V2;
then x in {u + v where u,v is Point of X: u in V1 & v in V2} by RUSUB_4:def 9
;
then ex u,v being Point of X st u+v = x & u in V1 & v in V2;
then x in {u9 + v9 where u9,v9 is Point of X: u9 in W1 & v9 in W2} by A1;
hence thesis by RUSUB_4:def 9;
end;
theorem Th12:
for X being right_zeroed non empty addLoopStr, V1,V2 being
Subset of X st 0.X in V2 holds V1 c= V1+V2
proof
let X be right_zeroed non empty addLoopStr, V1,V2 be Subset of X such that
A1: 0.X in V2;
let x be object;
assume
A2: x in V1;
then reconsider x as Point of X;
x+0.X = x by RLVECT_1:def 4;
then x in {u + v where u,v is Point of X: u in V1 & v in V2} by A1,A2;
hence thesis by RUSUB_4:def 9;
end;
theorem Th13:
for X being RealLinearSpace, r being Real holds r*{0.X} = {0.X}
proof
let X be RealLinearSpace, r be Real;
thus r*{0.X} c= {0.X}
proof
let x be object;
assume
A1: x in r*{0.X};
then reconsider x as Point of X;
consider v being Point of X such that
A2: x = r*v and
A3: v in {0.X} by A1;
v = 0.X by A3,TARSKI:def 1;
then r*v = 0.X;
hence thesis by A2,TARSKI:def 1;
end;
0.X in {0.X} by TARSKI:def 1;
then r*0.X in r*{0.X};
then 0.X in r*{0.X};
hence thesis by ZFMISC_1:31;
end;
theorem
for X being RealLinearSpace, M being Subset of X, r being non zero
Real st 0.X in r*M holds 0.X in M
proof
let X be RealLinearSpace, M be Subset of X, r be non zero Real;
assume 0.X in r*M;
then
A1: ex v being Point of X st r*v = 0.X & v in M;
r * 0.X = 0.X;
hence thesis by A1,RLVECT_1:36;
end;
theorem Th15:
for X being RealLinearSpace, M,N being Subset of X, r being non
zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
proof
let X be RealLinearSpace, M,N be Subset of X, r be non zero Real;
thus for x being object st x in (r * M) /\ (r * N)
holds x in r * (M /\ N)
proof
let x be object;
assume
A1: x in (r * M) /\ (r * N);
then x in r * M by XBOOLE_0:def 4;
then consider v1 being Point of X such that
A2: r*v1 = x and
A3: v1 in M;
x in (r * N) by A1,XBOOLE_0:def 4;
then consider v2 being Point of X such that
A4: r*v2 = x and
A5: v2 in N;
v1 = v2 by A2,A4,RLVECT_1:36;
then v1 in M /\ N by A3,A5,XBOOLE_0:def 4;
hence thesis by A2;
end;
let x be object;
assume x in r * (M /\ N);
then consider v being Point of X such that
A6: r*v = x and
A7: v in M /\ N;
v in N by A7,XBOOLE_0:def 4;
then
A8: x in r*N by A6;
v in M by A7,XBOOLE_0:def 4;
then x in r*M by A6;
hence thesis by A8,XBOOLE_0:def 4;
end;
theorem
for X being non empty TopSpace, x being Point of X, A being
a_neighborhood of x, B being Subset of X st A c= B holds B is a_neighborhood of
x
proof
let X be non empty TopSpace, x be Point of X, A be a_neighborhood of x, B be
Subset of X;
assume A c= B;
then x in Int A & Int A c= Int B by CONNSP_2:def 1,TOPS_1:19;
hence thesis by CONNSP_2:def 1;
end;
definition
let V be RealLinearSpace, M be Subset of V;
redefine attr M is convex means :: redefines convex (CONVEX1, definition)
:Def1:
for u,v being Point of V, r being Real
st 0 <= r & r <= 1 & u in M & v in M holds r*u + (1-r)*v in M;
compatibility
proof
hereby
assume
A1: M is convex;
let u,v be Point of V, r be Real such that
A2: 0 <= r & r <= 1 and
A3: u in M and
A4: v in M;
per cases by A2,XXREAL_0:1;
suppose
0 < r & r < 1;
hence r*u + (1-r)*v in M by A1,A3,A4;
end;
suppose
0 = r;
then r*u = 0.V & (1-r)*v = v by RLVECT_1:10,def 8;
hence r*u + (1-r)*v in M by A4;
end;
suppose
r = 1;
then (1-r)*v = 0.V & r*u = u by RLVECT_1:10,def 8;
hence r*u + (1-r)*v in M by A3;
end;
end;
assume
A5: for u,v being Point of V, r being Real st 0 <= r & r <= 1 & u in
M & v in M holds r*u + (1-r)*v in M;
let u,v be Point of V, r be Real;
thus thesis by A5;
end;
end;
Lm4: for X being RealLinearSpace holds conv({}X) = {}
proof
let X be RealLinearSpace;
{}X is convex;
then {}X in Convex-Family {}X by CONVEX1:def 4;
hence thesis by SETFAM_1:4;
end;
registration
let X be RealLinearSpace, M be empty Subset of X;
cluster conv(M) -> empty;
coherence
proof
M = {}X;
hence thesis by Lm4;
end;
end;
theorem
for X being RealLinearSpace, M being convex Subset of X holds conv(M) = M
by CONVEX1:30,CONVEX1:41;
theorem Th18:
for X being RealLinearSpace, M being Subset of X, r being Real
holds r*conv(M) = conv(r*M)
proof
let X be RealLinearSpace, M be Subset of X, r be Real;
thus r*conv(M) c= conv(r*M)
proof
let x be object;
per cases;
suppose
A1: r = 0;
per cases;
suppose
M = {};
hence thesis by CONVEX1:33;
end;
suppose
A2: M <> {};
then r*M = {0.X} by A1,CONVEX1:34;
then
A3: {0.X} c= conv(r*M) by CONVEX1:41;
conv(M) <> {} by A2,CONVEX1:41,XBOOLE_1:3;
then r*conv(M) = {0.X} by A1,CONVEX1:34;
hence thesis by A3;
end;
end;
suppose
A4: r <> 0;
assume x in r*conv(M);
then consider v being Point of X such that
A5: x = r*v and
A6: v in conv(M);
for V being set st V in Convex-Family(r*M) holds r*v in V
proof
let V be set;
assume
A7: V in Convex-Family(r*M);
then reconsider V as Subset of X;
r*M c= V by A7,CONVEX1:def 4;
then r"*(r*M) c= r"*V by CONVEX1:39;
then (r"*r)*M c= r"*V by CONVEX1:37;
then 1*M c= r"*V by A4,XCMPLX_0:def 7;
then
A8: M c= r"*V by CONVEX1:32;
V is convex by A7,CONVEX1:def 4;
then r"*V is convex by CONVEX1:1;
then r"*V in Convex-Family M by A8,CONVEX1:def 4;
then v in r"*V by A6,SETFAM_1:def 1;
then consider w being Point of X such that
A9: v = r"*w and
A10: w in V;
r*v = (r*r")*w by A9,RLVECT_1:def 7
.= 1*w by A4,XCMPLX_0:def 7
.= w by RLVECT_1:def 8;
hence thesis by A10;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
end;
r*M c= r*conv(M) & r*conv(M) is convex by CONVEX1:1,39,41;
hence thesis by CONVEX1:30;
end;
theorem Th19:
for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2
holds Convex-Family M2 c= Convex-Family M1
proof
let X be RealLinearSpace, M1,M2 be Subset of X such that
A1: M1 c= M2;
let M be object;
assume
A2: M in Convex-Family M2;
then reconsider M as Subset of X;
M2 c= M by A2,CONVEX1:def 4;
then
A3: M1 c= M by A1;
M is convex by A2,CONVEX1:def 4;
hence thesis by A3,CONVEX1:def 4;
end;
theorem Th20:
for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2
holds conv(M1) c= conv(M2)
proof
let X be RealLinearSpace, M1,M2 be Subset of X;
assume M1 c= M2;
then Convex-Family M2 c= Convex-Family M1 by Th19;
then
A1: meet (Convex-Family M1) c= meet (Convex-Family M2) by SETFAM_1:6;
let x be object;
assume x in conv(M1);
hence thesis by A1;
end;
theorem
for X being RealLinearSpace, M being convex Subset of X, r being Real
st 0 <= r & r <= 1 & 0.X in M holds r*M c= M
proof
let X be RealLinearSpace, M be convex Subset of X, r be Real such that
A1: 0 <= r & r <= 1 & 0.X in M;
let x be object;
assume x in r*M;
then consider v being Point of X such that
A2: r*v = x and
A3: v in M;
r*v + (1-r)*0.X in M by A1,A3,Def1;
then r*v + 0.X in M;
hence thesis by A2;
end;
definition
let X be RealLinearSpace, v,w be Point of X;
func LSeg(v,w) -> Subset of X equals
{(1-r)*v + r*w : 0 <= r & r <= 1 };
coherence
proof
{(1-r)*v + r*w: 0 <= r & r <= 1 } c= the carrier of X
proof
let x be object;
assume x in {(1-r)*v + r*w: 0 <= r & r <= 1 };
then ex r st x = (1-r)*v + r*w & 0 <= r & r <= 1;
hence thesis;
end;
hence thesis;
end;
commutativity
proof
let A be Subset of X, v,w be Point of X;
assume
A1: A = {(1-r)*v + r*w : 0 <= r & r <= 1 };
thus A c= {(1-r)*w + r*v : 0 <= r & r <= 1 }
proof
let x be object;
assume x in A;
then consider r such that
A2: x = (1-r)*v + r*w and
A3: 0 <= r & r <= 1 by A1;
A4: 1-(1-r)=r;
0 <= 1-r & 1-r <= 1-0 by A3,XREAL_1:10,48;
hence thesis by A2,A4;
end;
let x be object;
assume x in {(1-r)*w + r*v : 0 <= r & r <= 1 };
then consider r such that
A5: x = (1-r)*w + r*v and
A6: 0 <= r & r <= 1;
A7: 1-(1-r)=r;
0 <= 1-r & 1-r <= 1-0 by A6,XREAL_1:10,48;
hence thesis by A1,A5,A7;
end;
end;
registration
let X be RealLinearSpace, v,w be Point of X;
cluster LSeg(v,w) -> non empty convex;
coherence
proof
A1: 0 * w = 0.X & v + 0.X = v by RLVECT_1:10;
1 - 0 = 1 & 1 * v = v by RLVECT_1:def 8;
then v in LSeg(v,w) by A1;
hence LSeg(v,w) is non empty;
let u,u9 be Point of X, r be Real;
assume that
A2: 0 <= r and
A3: r <= 1;
A4: 0 <= 1-r by A3,XREAL_1:48;
assume u in LSeg(v,w);
then consider s being Real such that
A5: u = (1-s)*v + s*w and
A6: 0 <= s and
A7: s <= 1;
A8: r*u = r*((1-s)*v) + r*(s*w) by A5,RLVECT_1:def 5
.= r*(1-s)*v + r*(s*w) by RLVECT_1:def 7
.= r*(1-s)*v + r*s*w by RLVECT_1:def 7;
assume u9 in LSeg(v,w);
then consider t being Real such that
A9: u9 = (1-t)*v + t*w and
A10: 0 <= t and
A11: t <= 1;
(1-r)*u9 = (1-r)*((1-t)*v) + (1-r)*(t*w) by A9,RLVECT_1:def 5
.= (1-r)*(1-t)*v + (1-r)*(t*w) by RLVECT_1:def 7
.= (1-r)*(1-t)*v + (1-r)*t*w by RLVECT_1:def 7;
then
A12: r*u + (1-r)*u9 = r*(1-s)*v + (r*s*w + ((1-r)*(1-t)*v + (1-r)*t*w)) by A8,
RLVECT_1:def 3
.= r*(1-s)*v + ((1-r)*(1-t)*v + (r*s*w + (1-r)*t*w)) by RLVECT_1:def 3
.= r*(1-s)*v + (1-r)*(1-t)*v + (r*s*w + (1-r)*t*w) by RLVECT_1:def 3
.= (r*(1-s) + (1-r)*(1-t))*v + (r*s*w + (1-r)*t*w) by RLVECT_1:def 6
.= (1 - ((r*s + (1-r)*t)))*v + (r*s + (1-r)*t)*w by RLVECT_1:def 6;
(1-r)*t + r*s <= 1 by A2,A3,A7,A11,XREAL_1:174;
hence thesis by A2,A6,A10,A12,A4;
end;
end;
theorem
for X being RealLinearSpace, 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
let X be RealLinearSpace, M be Subset of X;
hereby
assume
A1: M is convex;
let u,w be Point of X such that
A2: u in M & w in M;
thus LSeg(u,w) c= M
proof
let x be object;
assume x in LSeg(u,w);
then ex r st x = (1-r)*u + r*w & 0 <= r & r <= 1;
hence x in M by A1,A2;
end;
end;
assume
A3: for w,u being Point of X st w in M & u in M holds LSeg(w,u) c= M;
let u,w be Point of X, r be Real such that
A4: 0 <= r & r <= 1 and
A5: u in M & w in M;
A6: r*u + (1-r)*w in LSeg(w,u) by A4;
LSeg(w,u) c= M by A3,A5;
hence thesis by A6;
end;
definition
let V be non empty RLSStruct, P be Subset-Family of V;
attr P is convex-membered means
:Def3:
for M being Subset of V st M in P holds M is convex;
end;
registration
let V be non empty RLSStruct;
cluster non empty convex-membered for Subset-Family of V;
existence
proof
reconsider F = {{}V} as Subset-Family of V;
take F;
thus F is non empty;
let M be Subset of V;
assume M in F;
then M = {}V by TARSKI:def 1;
hence thesis;
end;
end;
theorem
for V being non empty RLSStruct, F being convex-membered Subset-Family
of V holds meet F is convex
proof
let V be non empty RLSStruct, F be convex-membered Subset-Family of V;
for M being Subset of V st M in F holds M is convex by Def3;
hence thesis by CONVEX1:15;
end;
definition
let X be non empty RLSStruct, A be Subset of X;
func -A -> Subset of X equals
(-1)*A;
coherence;
end;
theorem Th24:
for X being RealLinearSpace, M,N being Subset of X, v being
Point of X holds v+M meets N iff v in N+(-M)
proof
let X be RealLinearSpace, M,N be Subset of X, v being Point of X;
A1: N+(-1)*M = {u + w where u,w is Point of X: u in N & w in (-1)*M} by
RUSUB_4:def 9;
hereby
A2: v+M = {v + u where u is Point of X: u in M} by RUSUB_4:def 8;
assume v+M meets N;
then consider z being object such that
A3: z in v+M and
A4: z in N by XBOOLE_0:3;
consider u being Point of X such that
A5: v+u = z and
A6: u in M by A3,A2;
reconsider z as Point of X by A3;
A7: (-1)*u in (-1)*M by A6;
z + (-1)*u = v + (u + (-1)*u) by A5,RLVECT_1:def 3
.= v + (u + -u) by RLVECT_1:16
.= v+ 0.X by RLVECT_1:5
.= v;
hence v in N+-M by A4,A7,Th3;
end;
assume v in N+(-M);
then consider u,w being Point of X such that
A8: v = u+w and
A9: u in N and
A10: w in (-1)*M by A1;
consider w9 being Point of X such that
A11: w = (-1)*w9 and
A12: w9 in M by A10;
A13: (-1)*w = (-1)*(-1)*w9 by A11,RLVECT_1:def 7
.= w9 by RLVECT_1:def 8;
v+w9 = u + (w+w9) by A8,RLVECT_1:def 3
.= u + (w+-w) by A13,RLVECT_1:16
.= u + 0.X by RLVECT_1:5
.= u;
then u in v+M by A12,Lm1;
hence thesis by A9,XBOOLE_0:3;
end;
definition
let X be non empty RLSStruct, A be Subset of X;
attr A is symmetric means
:Def5:
A = -A;
end;
registration
let X be RealLinearSpace;
cluster non empty symmetric for Subset of X;
existence
proof
take V = {0.X};
thus V is non empty;
thus V = -V by Th13;
end;
end;
theorem Th25:
for X being RealLinearSpace, A being symmetric Subset of X, x
being Point of X st x in A holds -x in A
proof
let X be RealLinearSpace, A be symmetric Subset of X, x be Point of X such
that
A1: x in A;
A = -A by Def5
.= (-1)*A;
then consider v being Point of X such that
A2: x = (-1)*v and
A3: v in A by A1;
(-1)*x = (-1)*(-1)*v by A2,RLVECT_1:def 7
.= v by RLVECT_1:def 8;
hence thesis by A3,RLVECT_1:16;
end;
definition
let X be non empty RLSStruct, A be Subset of X;
attr A is circled means
:Def6:
for r being Real st |.r.| <= 1 holds r*A c= A;
end;
registration
let X be non empty RLSStruct;
cluster empty -> circled for Subset of X;
coherence
by CONVEX1:33;
end;
theorem Th26:
for X being RealLinearSpace holds {0.X} is circled
by Th13;
registration
let X be RealLinearSpace;
cluster non empty circled for Subset of X;
existence
proof
take {0.X};
thus thesis by Th26;
end;
end;
theorem Th27:
for X being RealLinearSpace, B being non empty circled Subset of
X holds 0.X in B
proof
let X be RealLinearSpace;
let B be non empty circled Subset of X;
|. 0 .| = 0 by ABSVALUE:2;
then 0*B c= B by Def6;
then
A1: {0.X} c= B by CONVEX1:34;
0.X in {0.X} by TARSKI:def 1;
hence thesis by A1;
end;
Lm5: for X being RealLinearSpace,A,B being circled Subset of X holds A+B is
circled
proof
let X be non empty RealLinearSpace,A,B be circled Subset of X;
A1: A+B = {u + v where u,v is Point of X: u in A & v in B} by RUSUB_4:def 9;
let r be Real;
assume |.r.| <= 1;
then
A2: r*A c= A & r*B c= B by Def6;
let x be object;
assume x in r*(A+B);
then consider x9 being Point of X such that
A3: x = r*x9 and
A4: x9 in A+B;
consider u,v being Point of X such that
A5: x9 = u+v and
A6: u in A & v in B by A1,A4;
A7: r*u in r*A & r*v in r*B by A6;
x = r*u+r*v by A3,A5,RLVECT_1:def 5;
hence thesis by A2,A7,Th3;
end;
registration
let X be RealLinearSpace, A,B be circled Subset of X;
cluster A+B -> circled;
coherence by Lm5;
end;
theorem Th28:
for X being RealLinearSpace, A being circled Subset of X for r
being Real st |.r.| = 1 holds r*A = A
proof
let X be RealLinearSpace, A be circled Subset of X;
let r be Real;
assume
A1: |.r.| = 1;
hence
A2: r*A c= A by Def6;
let x be object;
assume
A3: x in A;
then reconsider x as Point of X;
A4: r*x in r*A by A3;
per cases;
suppose
0 <= r;
then r = 1 by A1,ABSVALUE:def 1;
hence thesis by A3,CONVEX1:32;
end;
suppose
r < 0;
then |.r.| = -r by ABSVALUE:def 1;
then (-1)*((-1)*x) in r*A by A1,A2,A4;
then (-1)*(-1)*x in r*A by RLVECT_1:def 7;
hence thesis by RLVECT_1:def 8;
end;
end;
Lm6: for X being RealLinearSpace, A being circled Subset of X holds A is
symmetric
proof
let X be RealLinearSpace, A be circled Subset of X;
|.-1.| = --1 by ABSVALUE:def 1
.= 1;
hence A = -A by Th28;
end;
registration
let X be RealLinearSpace;
cluster circled -> symmetric for Subset of X;
coherence by Lm6;
end;
Lm7: for X being RealLinearSpace, M being circled Subset of X holds conv(M) is
circled
proof
let X be RealLinearSpace, M be circled Subset of X;
let r be Real;
assume |.r.| <= 1;
then
A1: r*M c= M by Def6;
r*conv(M) = conv(r*M) by Th18;
hence thesis by A1,Th20;
end;
registration
let X be RealLinearSpace, M be circled Subset of X;
cluster conv(M) -> circled;
coherence by Lm7;
end;
definition
let X be non empty RLSStruct, F be Subset-Family of X;
attr F is circled-membered means
:Def7:
for V being Subset of X st V in F holds V is circled;
end;
registration
let V be non empty RLSStruct;
cluster non empty circled-membered for Subset-Family of V;
existence
proof
reconsider F = {{}V} as Subset-Family of V;
take F;
thus F is non empty;
let M be Subset of V;
assume M in F;
hence thesis by TARSKI:def 1;
end;
end;
theorem
for X being non empty RLSStruct, F being circled-membered
Subset-Family of X holds union F is circled
proof
let X be non empty RLSStruct, F be circled-membered Subset-Family of X;
let r be Real such that
A1: |.r.| <= 1;
let x be object;
assume x in r*(union F);
then consider x9 being Point of X such that
A2: x = r*x9 and
A3: x9 in union F;
consider Y being set such that
A4: x9 in Y and
A5: Y in F by A3,TARSKI:def 4;
reconsider Y as Subset of X by A5;
Y is circled by A5,Def7;
then
A6: r*Y c= Y by A1;
r*x9 in r*Y by A4;
hence thesis by A2,A5,A6,TARSKI:def 4;
end;
theorem
for X being non empty RLSStruct, F being circled-membered
Subset-Family of X holds meet F is circled
proof
let X be non empty RLSStruct, F be circled-membered Subset-Family of X;
let r be Real such that
A1: |.r.| <= 1;
let x be object;
assume x in r*(meet F);
then consider x9 being Point of X such that
A2: x = r*x9 and
A3: x9 in meet F;
A4: now
let Y be set;
assume
A5: Y in F;
then reconsider Y9 = Y as Subset of X;
x9 in Y by A3,A5,SETFAM_1:def 1;
then
A6: r*x9 in r*Y9;
Y9 is circled by A5,Def7;
then r*Y9 c= Y9 by A1;
hence x in Y by A2,A6;
end;
F <> {} by A3,SETFAM_1:def 1;
hence thesis by A4,SETFAM_1:def 1;
end;
begin
definition
struct(RLSStruct,TopStruct) RLTopStruct (# carrier -> set, ZeroF -> Element
of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:REAL, the
carrier:],the carrier, topology -> Subset-Family of the carrier #);
end;
registration
let X be non empty set, O be Element of X, F be BinOp of X, G be Function of
[:REAL,X:],X, T be Subset-Family of X;
cluster RLTopStruct (# X,O,F,G,T #) -> non empty;
coherence;
end;
registration
cluster strict non empty for RLTopStruct;
existence
proof
set X = {0};
reconsider O = 0 as Element of X by TARSKI:def 1;
set F = the BinOp of X;
set G = the Function of [:REAL,X:],X;
take RT = RLTopStruct (# X,O,F,G,{}bool X#);
thus RT is strict;
thus the carrier of RT is non empty;
end;
end;
definition
let X be non empty RLTopStruct;
attr X is add-continuous means
:Def8:
for x1,x2 being Point of X, V being
Subset of X st V is open & x1+x2 in V 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:
for a being Real, x being Point of X,
V being Subset of X st V is open & a*x in V
ex r being positive Real, 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;
registration
cluster strict add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital for non
empty RLTopStruct;
existence
proof
set ZS = {0};
set T = {{},ZS};
T c= bool ZS
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in T;
then x = {} or x = ZS by TARSKI:def 2;
then xx c= ZS;
hence thesis;
end;
then reconsider T as Subset-Family of ZS;
reconsider O = 0 as Element of ZS by TARSKI:def 1;
deffunc A((Element of ZS), Element of ZS) = O;
consider F being BinOp of ZS such that
A1: for x,y being Element of ZS holds F.(x,y) = A(x,y) from BINOP_1:
sch 4;
deffunc M(Real, Element of ZS) = O;
consider G being Function of [:REAL,ZS:],ZS such that
A2: for a being Element of REAL for x being Element of ZS holds G.(a,x
) = M(a,x) from BINOP_1:sch 4;
take W = RLTopStruct (# ZS,O,F,G,T #);
thus W is strict;
thus W is add-continuous
proof
reconsider V1 = {O}, V2 = {O} as Subset of W;
let x1,x2 be Point of W, V be Subset of W such that
A3: V is open and
A4: x1+x2 in V;
take V1,V2;
V1 in T by TARSKI:def 2;
hence V1 is open & V2 is open;
thus x1 in V1 & x2 in V2;
V in T by A3;
then V = the carrier of W by A4,TARSKI:def 2;
hence thesis;
end;
thus W is Mult-continuous
proof
reconsider V9 = {O} as Subset of W;
let a be Real, x be Point of W, V be Subset of W such that
A5: V is open and
A6: a*x in V;
take jj,V9;
V9 in T by TARSKI:def 2;
hence V9 is open;
thus x in V9;
let s be Real such that
|.s-a.| < jj;
V in T by A5;
then V = {} or V = ZS by TARSKI:def 2;
hence thesis by A6;
end;
thus W is TopSpace-like
proof
thus the carrier of W in the topology of W by TARSKI:def 2;
hereby
let a be Subset-Family of W;
assume a c= the topology of W;
then a={} or a={{}} or a={ZS} or a={{},ZS} by ZFMISC_1:36;
then union a={} or union a=ZS or union a = {} \/ ZS by ZFMISC_1:2,25,75
;
hence union a in the topology of W by TARSKI:def 2;
end;
let a,b be Subset of W such that
A7: a in the topology of W and
A8: b in the topology of W;
A9: b={} or b=ZS by A8,TARSKI:def 2;
a={} or a=ZS by A7,TARSKI:def 2;
hence thesis by A9,TARSKI:def 2;
end;
thus for x,y being Point of W holds x + y = y + x
proof
let x,y be Point of W;
reconsider X = x, Y = y as Element of ZS;
x + y = A(X,Y) by A1;
hence thesis by A1;
end;
thus for x,y,z being Point of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be Point of W;
reconsider X = x, Y = y, Z = z as Element of ZS;
(x + y) + z = A(A(X,Y),Z) by A1;
hence thesis by A1;
end;
thus for x being Point of W holds x + 0.W = x
proof
let x be Point of W;
reconsider X = x as Element of ZS;
x + 0.W = A(X,O) by A1;
hence thesis by TARSKI:def 1;
end;
thus for x being Point of W holds x is right_complementable
proof
reconsider y = O as Point of W;
let x be Point of W;
take y;
thus thesis by A1;
end;
thus for a being Real, x,y being Point of W holds a * (x + y) = a *
x + a * y
proof
let a be Real;
reconsider a as Element of REAL by XREAL_0:def 1;
let x,y be Point of W;
reconsider X = x, Y = y as Element of ZS;
a * x + a * y = M(a,A(X,Y)) by A1
.= G.(a,A(X,Y)) by A2
.= G.(a,F.(x,y)) by A1;
hence thesis;
end;
thus for a,b being Real for x being Point of W holds (a + b) * x =
a * x + b * x
proof
let a,b be Real, x be Point of W;
reconsider a,b as Element of REAL by XREAL_0:def 1;
set c = a + b;
reconsider X = x as Element of ZS;
c * x = M(c,X) by A2;
hence thesis by A1;
end;
thus for a,b being Real, x being Point of W holds (a * b) * x = a *
(b * x)
proof
let a,b be Real, x be Point of W;
reconsider a,b as Element of REAL by XREAL_0:def 1;
set c = a * b;
reconsider X = x as Element of ZS;
c * x = M(c,X) by A2;
hence thesis by A2;
end;
thus for x being Point of W holds 1 * x = x
proof
reconsider A9 = 1 as Element of REAL by XREAL_0:def 1 ;
let x be Point of W;
reconsider X = x as Element of ZS;
A9 * x = M(A9,X) by A2;
hence thesis by TARSKI:def 1;
end;
end;
end;
definition
mode LinearTopSpace is add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty RLTopStruct;
end;
theorem Th31:
for X being LinearTopSpace, x1,x2 being Point of X, V being
a_neighborhood of x1+x2 ex V1 being a_neighborhood of x1, V2 being
a_neighborhood of x2 st V1+V2 c= V
proof
let X be LinearTopSpace;
let x1,x2 be Point of X, V be a_neighborhood of x1+x2;
x1+x2 in Int V by CONNSP_2:def 1;
then consider V1,V2 being Subset of X such that
A1: V1 is open and
A2: V2 is open and
A3: x1 in V1 and
A4: x2 in V2 and
A5: V1+V2 c= Int V by Def8;
Int V2 = V2 by A2,TOPS_1:23;
then reconsider V2 as a_neighborhood of x2 by A4,CONNSP_2:def 1;
Int V1 = V1 by A1,TOPS_1:23;
then reconsider V1 as a_neighborhood of x1 by A3,CONNSP_2:def 1;
take V1,V2;
Int V c= V by TOPS_1:16;
hence thesis by A5;
end;
theorem Th32:
for X being LinearTopSpace, a being Real, x being Point of X, V
being a_neighborhood of a*x
ex r being positive Real, W being a_neighborhood of
x st for s being Real st |.s-a.| < r holds s*W c= V
proof
let X be LinearTopSpace, a be Real, x be Point of X, V be a_neighborhood of
a*x;
a*x in Int(V) by CONNSP_2:def 1;
then consider r being positive Real, W being Subset of X such that
A1: W is open and
A2: x in W and
A3: for s being Real st |.s-a.| < r holds s*W c= Int(V) by Def9;
Int(W) = W by A1,TOPS_1:23;
then reconsider W as a_neighborhood of x by A2,CONNSP_2:def 1;
take r;
take W;
let s be Real;
assume |.s-a.| < r;
then
A4: s*W c= Int(V) by A3;
Int(V) c= V by TOPS_1:16;
hence thesis by A4;
end;
definition
let X be non empty RLTopStruct, a be Point of X;
func transl(a,X) -> Function of X,X means
:Def10:
for x being Point of X holds it.x = a+x;
existence
proof
deffunc F(Point of X) = a+$1;
consider F be Function of the carrier of X, the carrier of X such that
A1: for x being Point of X holds F.x = F(x) from FUNCT_2:sch 4;
reconsider F as Function of X,X;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function of X,X such that
A2: for x being Point of X holds F.x = a+x and
A3: for x being Point of X holds G.x = a+x;
now
let x be Point of X;
thus F.x = a+x by A2
.= G.x by A3;
end;
hence F = G by FUNCT_2:63;
end;
end;
theorem Th33:
for X being non empty RLTopStruct, a being Point of X, V being
Subset of X holds transl(a,X).:V = a+V
proof
let X be non empty RLTopStruct, a be Point of X, V be Subset of X;
thus transl(a,X).:V c= a+V
proof
let y be object;
assume y in transl(a,X).:V;
then consider c being Point of X such that
A1: c in V and
A2: y = transl(a,X).c by FUNCT_2:65;
y = a+c by A2,Def10;
hence thesis by A1,Lm1;
end;
let x be object;
assume x in a+V;
then x in {a + u where u is Point of X: u in V} by RUSUB_4:def 8;
then consider u being Point of X such that
A3: x = a+u and
A4: u in V;
x = transl(a,X).u by A3,Def10;
hence thesis by A4,FUNCT_2:35;
end;
theorem Th34:
for X being LinearTopSpace, a being Point of X holds rng transl( a,X) = [#]X
proof
let X be LinearTopSpace, a be Point of X;
thus rng transl(a,X) c= [#]X;
let y be object;
assume y in [#]X;
then reconsider y as Point of X;
transl(a,X).(-a+y) = a+(-a+y) by Def10
.= a+-a+y by RLVECT_1:def 3
.= 0.X+y by RLVECT_1:5
.= y;
hence thesis by FUNCT_2:4;
end;
Lm8: for X being LinearTopSpace, a being Point of X holds transl(a,X) is
one-to-one
proof
let X be LinearTopSpace, a be Point of X;
now
let x1,x2 be object such that
A1: x1 in the carrier of X & x2 in the carrier of X and
A2: transl(a,X).x1 = transl(a,X).x2;
reconsider x19 = x1, x29 = x2 as Point of X by A1;
transl(a,X).x1 = a+x19 & transl(a,X).x2 = a+x29 by Def10;
hence x1 = x2 by A2,RLVECT_1:8;
end;
hence thesis by FUNCT_2:19;
end;
theorem Th35:
for X being LinearTopSpace, a being Point of X holds transl(a,X)
" = transl(-a,X)
proof
let X be LinearTopSpace, a be Point of X;
A1: rng transl(a,X) = [#]X by Th34;
now
let x be Point of X;
consider u being object such that
A2: u in dom transl(a,X) and
A3: x = transl(a,X).u by A1,FUNCT_1:def 3;
reconsider u as Point of X by A2;
A4: x = a+u by A3,Def10;
transl(a,X) is onto one-to-one by A1,Lm8,FUNCT_2:def 3;
hence transl(a,X)".x = (transl(a,X) qua Function)".x by TOPS_2:def 4
.= u by A3,Lm8,FUNCT_2:26
.= 0.X+u
.= (-a+a)+u by RLVECT_1:5
.= -a+x by A4,RLVECT_1:def 3
.= transl(-a,X).x by Def10;
end;
hence thesis by FUNCT_2:63;
end;
Lm9: for X being LinearTopSpace, a being Point of X holds transl(a,X) is
continuous
proof
let X be LinearTopSpace, a be Point of X;
A1: now
reconsider X9 = X as TopStruct;
let P be Subset of X;
defpred P[Subset of X9] means ex D being Subset of X st D = $1 & D is open
& a+D c= P;
consider F being Subset-Family of X9 such that
A2: for A being Subset of X9 holds A in F iff P[A] from SUBSET_1:sch 3;
reconsider F as Subset-Family of X;
assume
A3: P is open;
A4: union F = transl(a,X)"P
proof
thus union F c= transl(a,X)"P
proof
let x be object;
assume x in union F;
then consider A being set such that
A5: x in A and
A6: A in F by TARSKI:def 4;
reconsider x as Point of X by A5,A6;
A7: transl(a,X).x = a+x by Def10;
consider D being Subset of X such that
A8: D = A and
D is open and
A9: a+D c= P by A2,A6;
a+D = {a + u where u is Point of X: u in D} by RUSUB_4:def 8;
then a+x in a+D by A5,A8;
hence thesis by A9,A7,FUNCT_2:38;
end;
let x be object;
assume
A10: x in transl(a,X)"P;
then reconsider x as Point of X;
transl(a,X).x in P by A10,FUNCT_2:38;
then a+x in P by Def10;
then consider V,D being Subset of X such that
V is open and
A11: D is open and
A12: a in V and
A13: x in D and
A14: V+D c= P by A3,Def8;
{a}+D = a+D & {a} c= V by A12,RUSUB_4:33,ZFMISC_1:31;
then a+D c= V+D by Th10;
then a+D c= P by A14;
then D in F by A2,A11;
hence thesis by A13,TARSKI:def 4;
end;
F is open
proof
let A be Subset of X;
assume A in F;
then ex D being Subset of X st D=A & D is open & a+D c= P by A2;
hence thesis;
end;
hence transl(a,X)"P is open by A4,TOPS_2:19;
end;
[#]X <> {};
hence thesis by A1,TOPS_2:43;
end;
registration
let X be LinearTopSpace, a be Point of X;
cluster transl(a,X) -> being_homeomorphism;
coherence
proof
thus dom transl(a,X) = [#]X by FUNCT_2:def 1;
thus rng transl(a,X) = [#]X by Th34;
thus transl(a,X) is one-to-one by Lm8;
thus transl(a,X) is continuous by Lm9;
transl(a,X)" = transl(-a,X) by Th35;
hence thesis by Lm9;
end;
end;
Lm10: for X being LinearTopSpace, E being Subset of X, x being Point of X st E
is open holds x+E is open
proof
let X be LinearTopSpace, E be Subset of X, x be Point of X;
assume
A1: E is open;
transl(x,X).:E = x+E by Th33;
hence thesis by A1,TOPGRP_1:25;
end;
registration
let X be LinearTopSpace, E be open Subset of X, x be Point of X;
cluster x+E -> open;
coherence by Lm10;
end;
Lm11: for X being LinearTopSpace, E being open Subset of X, K being Subset of
X holds K+E is open
proof
let X be LinearTopSpace, E be open Subset of X, K be Subset of X;
reconsider F = { a+E where a is Point of X: a in K} as Subset-Family of X by
Lm2;
A1: F is open
proof
let P be Subset of X;
assume P in F;
then ex a being Point of X st P=a+E & a in K;
hence thesis;
end;
K+E = union F by Th4;
hence thesis by A1,TOPS_2:19;
end;
registration
let X be LinearTopSpace, E be open Subset of X, K be Subset of X;
cluster K+E -> open;
coherence by Lm11;
end;
Lm12: for X being LinearTopSpace, D being closed Subset of X, x being Point of
X holds x+D is closed
proof
let X be LinearTopSpace, D be closed Subset of X, x be Point of X;
transl(x,X).:D = x+D by Th33;
hence thesis by TOPS_2:58;
end;
registration
let X be LinearTopSpace, D be closed Subset of X, x be Point of X;
cluster x+D -> closed;
coherence by Lm12;
end;
theorem Th36:
for X being LinearTopSpace, V1,V2,V being Subset of X st V1+V2
c= V holds Int V1 + Int V2 c= Int V
proof
let X be LinearTopSpace, V1,V2,V be Subset of X such that
A1: V1+V2 c= V;
Int V1 c= V1 & Int V2 c= V2 by TOPS_1:16;
then Int V1 + Int V2 c= V1+V2 by Th11;
then Int V1 + Int V2 c= V by A1;
hence thesis by TOPS_1:24;
end;
theorem Th37:
for X being LinearTopSpace, x being Point of X, V being Subset
of X holds x+Int(V) = Int(x+V)
proof
let X be LinearTopSpace, x be Point of X, V be Subset of X;
x+Int(V) c= x+V by Th8,TOPS_1:16;
hence x+Int(V) c= Int(x+V) by TOPS_1:24;
let v be object;
assume
A1: v in Int(x+V);
then reconsider v as Point of X;
consider Q being Subset of X such that
A2: Q is open and
A3: Q c= x+V and
A4: v in Q by A1,TOPS_1:22;
-x+Q c= -x+(x+V) by A3,Th8;
then -x+Q c= -x+x+V by Th6;
then -x+Q c= 0.X+V by RLVECT_1:5;
then -x+Q c= V by Th5;
then
A5: x+Int(V) = {x + u where u is Point of X: u in Int V} & -x+Q c=Int(V) by A2,
RUSUB_4:def 8,TOPS_1:24;
-x+v in -x+Q by A4,Lm1;
then x+(-x+v) in x+Int(V) by A5;
then x+-x+v in x+Int(V) by RLVECT_1:def 3;
then 0.X+v in x+Int(V) by RLVECT_1:5;
hence thesis;
end;
theorem
for X being LinearTopSpace, x being Point of X, V being Subset of X
holds x+Cl(V) = Cl(x+V)
proof
let X be LinearTopSpace, x be Point of X, V be Subset of X;
thus x+Cl(V) c= Cl(x+V)
proof
let v be object;
assume
A1: v in x+Cl(V);
then reconsider v as Point of X;
now
A2: x+Cl(V) = {x + u where u is Point of X: u in Cl V} by RUSUB_4:def 8;
A3: x+V = {x + u where u is Point of X: u in V} by RUSUB_4:def 8;
let G be Subset of X such that
A4: G is open and
A5: v in G;
A6: -x+G = {-x+u where u is Point of X: u in G} by RUSUB_4:def 8;
then
A7: -x+v in -x+G by A5;
consider u being Point of X such that
A8: v = x+u and
A9: u in Cl V by A1,A2;
-x+v = -x+x+u by A8,RLVECT_1:def 3
.= 0.X+u by RLVECT_1:5
.= u;
then V meets -x+G by A4,A9,A7,PRE_TOPC:24;
then consider z being object such that
A10: z in V and
A11: z in -x+G by XBOOLE_0:3;
reconsider z as Point of X by A10;
consider w being Point of X such that
A12: z = -x+w and
A13: w in G by A6,A11;
A14: x+z in x+V by A3,A10;
x+z = x+-x+w by A12,RLVECT_1:def 3
.= 0.X+w by RLVECT_1:5
.= w;
hence x+V meets G by A13,A14,XBOOLE_0:3;
end;
hence thesis by PRE_TOPC:24;
end;
x+V c= x+Cl(V) by Th8,PRE_TOPC:18;
hence thesis by TOPS_1:5;
end;
theorem
for X being LinearTopSpace, x,v being Point of X, V being
a_neighborhood of x holds v+V is a_neighborhood of v+x
proof
let X be LinearTopSpace, x,v be Point of X, V be a_neighborhood of x;
v+Int(V) = {v + u where u is Point of X: u in Int V} & x in Int V by
CONNSP_2:def 1,RUSUB_4:def 8;
then
A1: v+x in v+Int(V);
v+Int(V) = Int(v+V) by Th37;
hence thesis by A1,CONNSP_2:def 1;
end;
theorem
for X being LinearTopSpace, x being Point of X, V being a_neighborhood
of x holds -x+V is a_neighborhood of 0.X
proof
let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x;
-x+Int(V) = {-x + v where v is Point of X: v in Int V} & x in Int V by
CONNSP_2:def 1,RUSUB_4:def 8;
then -x+x in -x+Int(V);
then
A1: 0.X in -x+Int(V) by RLVECT_1:5;
-x+Int(V) c= Int(-x+V) by Th37;
hence thesis by A1,CONNSP_2:def 1;
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
ex P being local_base of X st P is convex-membered;
end;
definition
let X be LinearTopSpace, E be Subset of X;
attr E is bounded means
:Def12:
for V being a_neighborhood of 0.X ex s st s
> 0 & for t st t > s holds E c= t*V;
end;
registration
let X be LinearTopSpace;
cluster empty -> bounded for Subset of X;
coherence
proof let S be Subset of X;
assume S is empty;
then
A1: S = {}X;
let V be a_neighborhood of 0.X;
take 1;
thus thesis by A1;
end;
end;
registration
let X be LinearTopSpace;
cluster bounded for Subset of X;
existence
proof
take {}X;
thus thesis;
end;
end;
theorem Th41:
for X being LinearTopSpace, V1,V2 being bounded Subset of X
holds V1 \/ V2 is bounded
proof
let X be non empty LinearTopSpace, V1,V2 be bounded Subset of X;
thus thesis
proof
let V be a_neighborhood of 0.X;
consider s such that
A1: s > 0 and
A2: for t st t > s holds V1 c= t*V by Def12;
consider r such that
A3: r > 0 and
A4: for t st t > r holds V2 c= t*V by Def12;
per cases;
suppose
A5: r <= s;
take s;
thus s > 0 by A1;
let t such that
A6: t > s;
t > r by A5,A6,XXREAL_0:2;
then
A7: V2 c= t*V by A4;
V1 c= t*V by A2,A6;
hence thesis by A7,XBOOLE_1:8;
end;
suppose
A8: r > s;
take r;
thus r > 0 by A3;
let t such that
A9: t > r;
t > s by A8,A9,XXREAL_0:2;
then
A10: V1 c= t*V by A2;
V2 c= t*V by A4,A9;
hence thesis by A10,XBOOLE_1:8;
end;
end;
end;
theorem
for X being LinearTopSpace, P being bounded Subset of X, Q being
Subset of X st Q c= P holds Q is bounded
proof
let X be LinearTopSpace, P be bounded Subset of X, Q being Subset of X such
that
A1: Q c= P;
let V be a_neighborhood of 0.X;
consider s such that
A2: s > 0 and
A3: for t st t > s holds P c= t*V by Def12;
take s;
thus s > 0 by A2;
let t;
assume t > s;
then P c= t*V by A3;
hence thesis by A1;
end;
theorem
for X being LinearTopSpace, F being Subset-Family of X st F is finite
& F = the set of all P where P is bounded Subset of X holds union F is
bounded
proof
let X be LinearTopSpace, F be Subset-Family of X such that
A1: F is finite and
A2: F = the set of all P where P is bounded Subset of X;
defpred P[set] means ex A being Subset of X st A = union $1 & A is bounded;
A3: now
let P be Subset of X;
assume P in F;
then ex A being bounded Subset of X st P=A by A2;
hence P is bounded;
end;
A4: for x,B being set st x in F & B c= F & P[B] holds P[B \/ {x}]
proof
let x,B be set such that
A5: x in F and
B c= F and
A6: P[B];
consider A being Subset of X such that
A7: A = union B & A is bounded by A6;
reconsider x as Subset of X by A5;
A8: union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78
.= union B \/ x by ZFMISC_1:25;
A9: x is bounded by A3,A5;
ex Y being Subset of X st Y = union (B \/ {x}) & Y is bounded
proof
take A \/ x;
thus thesis by A7,A8,A9,Th41;
end;
hence thesis;
end;
{}X = union {} by ZFMISC_1:2;
then
A10: P[{}];
P[F] from FINSET_1:sch 2(A1,A10,A4);
hence thesis;
end;
theorem Th44:
for X being LinearTopSpace, P being Subset-Family of X st P = the set of all
U
where U is a_neighborhood of 0.X holds P is local_base of X
proof
let X be LinearTopSpace, P be Subset-Family of X such that
A1: P = the set of all U where U is a_neighborhood of 0.X;
let A be a_neighborhood of 0.X;
take A;
thus thesis by A1;
end;
theorem
for X being LinearTopSpace, O being local_base of X, 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
let X be LinearTopSpace, O be basis of 0.X, P be Subset-Family of X such
that
A1: P = {a+U where a is Point of X, U is Subset of X: U in O};
let p be Point of X;
let A be a_neighborhood of p;
p in Int(A) by CONNSP_2:def 1;
then -p+Int(A) is a_neighborhood of 0.X by Th9,CONNSP_2:3;
then consider V being a_neighborhood of 0.X such that
A2: V in O and
A3: V c= -p+Int(A) by YELLOW13:def 2;
take U = p+V;
0.X in Int(V) by CONNSP_2:def 1;
then p+0.X in p+Int(V) by Lm1;
then
A4: p in p+Int(V);
p+Int(V) c= Int(U) by Th37;
hence U is a_neighborhood of p by A4,CONNSP_2:def 1;
thus U in P by A1,A2;
U c= p+(-p+Int(A)) by A3,Th8;
then U c= p+-p+Int(A) by Th6;
then U c= 0.X+Int(A) by RLVECT_1:5;
then Int(A) c= A & U c= Int(A) by Th5,TOPS_1:16;
hence thesis;
end;
definition
let X be non empty RLTopStruct, r be Real;
func mlt(r,X) -> Function of X,X means
:Def13:
for x being Point of X holds it.x = r*x;
existence
proof
deffunc F(Point of X) = r*$1;
consider F be Function of the carrier of X, the carrier of X such that
A1: for x being Point of X holds F.x = F(x) from FUNCT_2:sch 4;
reconsider F as Function of X,X;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function of X,X such that
A2: for x being Point of X holds F.x = r*x and
A3: for x being Point of X holds G.x = r*x;
now
let x be Point of X;
thus F.x = r*x by A2
.= G.x by A3;
end;
hence F = G by FUNCT_2:63;
end;
end;
theorem Th46:
for X being non empty RLTopStruct, V being Subset of X, r being
non zero Real holds mlt(r,X).:V = r*V
proof
let X be non empty RLTopStruct, V be Subset of X, r be non zero Real;
thus mlt(r,X).:V c= r*V
proof
let y be object;
assume y in mlt(r,X).:V;
then consider c being Point of X such that
A1: c in V and
A2: y = mlt(r,X).c by FUNCT_2:65;
y = r*c by A2,Def13;
hence thesis by A1;
end;
let x be object;
assume x in r*V;
then consider u being Point of X such that
A3: x = r*u and
A4: u in V;
x = mlt(r,X).u by A3,Def13;
hence thesis by A4,FUNCT_2:35;
end;
theorem Th47:
for X being LinearTopSpace, r being non zero Real holds rng mlt( r,X) = [#]X
proof
let X be LinearTopSpace, r be non zero Real;
thus rng mlt(r,X) c= [#]X;
let y be object;
assume y in [#]X;
then reconsider y as Point of X;
mlt(r,X).(r"*y) = r*(r"*y) by Def13
.= r*r"*y by RLVECT_1:def 7
.= 1*y by XCMPLX_0:def 7
.= y by RLVECT_1:def 8;
hence thesis by FUNCT_2:4;
end;
Lm13: for X being LinearTopSpace, r being non zero Real holds mlt(r,X) is
one-to-one
proof
let X be LinearTopSpace, r be non zero Real;
now
let x1,x2 be object such that
A1: x1 in the carrier of X & x2 in the carrier of X and
A2: mlt(r,X).x1 = mlt(r,X).x2;
reconsider x19 = x1, x29 = x2 as Point of X by A1;
mlt(r,X).x1 = r*x19 & mlt(r,X).x2 = r*x29 by Def13;
hence x1 = x2 by A2,RLVECT_1:36;
end;
hence thesis by FUNCT_2:19;
end;
theorem Th48:
for X being LinearTopSpace, r being non zero Real holds mlt(r,X)
" = mlt(r",X)
proof
let X be LinearTopSpace, r be non zero Real;
A1: rng mlt(r,X) = [#]X by Th47;
now
let x be Point of X;
consider u being object such that
A2: u in dom mlt(r,X) and
A3: x = mlt(r,X).u by A1,FUNCT_1:def 3;
reconsider u as Point of X by A2;
A4: x = r*u by A3,Def13;
mlt(r,X) is onto one-to-one by A1,Lm13,FUNCT_2:def 3;
hence mlt(r,X)".x = (mlt(r,X) qua Function)".x by TOPS_2:def 4
.= u by A3,Lm13,FUNCT_2:26
.= 1*u by RLVECT_1:def 8
.= (r*r")*u by XCMPLX_0:def 7
.= r"*x by A4,RLVECT_1:def 7
.= mlt(r",X).x by Def13;
end;
hence thesis by FUNCT_2:63;
end;
Lm14: for X being LinearTopSpace, r being non zero Real holds mlt(r,X) is
continuous
proof
let X be LinearTopSpace, r be non zero Real;
A1: now
let P be Subset of X;
defpred P[Subset of X] means $1 is open & r*$1 c= P;
consider F being Subset-Family of X such that
A2: for A being Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;
reconsider F as Subset-Family of X;
assume
A3: P is open;
A4: union F = mlt(r,X)"P
proof
thus union F c= mlt(r,X)"P
proof
let x be object;
assume x in union F;
then consider A being set such that
A5: x in A and
A6: A in F by TARSKI:def 4;
reconsider A as Subset of X by A6;
A is Subset of X;
then reconsider x as Point of X by A5;
A7: mlt(r,X).x = r*x by Def13;
r*A c= P & r*x in r*A by A2,A5,A6;
hence thesis by A7,FUNCT_2:38;
end;
let x be object;
assume
A8: x in mlt(r,X)"P;
then reconsider x as Point of X;
mlt(r,X).x in P by A8,FUNCT_2:38;
then r*x in P by Def13;
then consider e being positive Real, W being Subset of X such that
A9: W is open and
A10: x in W and
A11: for s being Real st |.s - r.| < e holds s*W c= P by A3,Def9;
|.r - r.| < e by ABSVALUE:2;
then r*W c= P by A11;
then W in F by A2,A9;
hence thesis by A10,TARSKI:def 4;
end;
F is open
by A2;
hence mlt(r,X)"P is open by A4,TOPS_2:19;
end;
[#]X <> {};
hence thesis by A1,TOPS_2:43;
end;
registration
let X be LinearTopSpace, r be non zero Real;
cluster mlt(r,X) -> being_homeomorphism;
coherence
proof
thus dom mlt(r,X) = [#]X by FUNCT_2:def 1;
thus rng mlt(r,X) = [#]X by Th47;
thus mlt(r,X) is one-to-one by Lm13;
thus mlt(r,X) is continuous by Lm14;
mlt(r,X)" = mlt(r",X) by Th48;
hence thesis by Lm14;
end;
end;
theorem Th49:
for X being LinearTopSpace, V being open Subset of X, r being
non zero Real holds r*V is open
proof
let X be LinearTopSpace, V be open Subset of X, r be non zero Real;
reconsider r as non zero Real;
mlt(r,X).:V = r*V by Th46;
hence thesis by TOPGRP_1:25;
end;
theorem Th50:
for X being LinearTopSpace, V being closed Subset of X, r being
non zero Real holds r*V is closed
proof
let X be LinearTopSpace, V be closed Subset of X,
r be non zero Real;
reconsider r as non zero Real;
mlt(r,X).:V = r*V by Th46;
hence thesis by TOPS_2:58;
end;
theorem Th51:
for X being LinearTopSpace, V being Subset of X, r be non zero
Real holds r*Int(V) = Int(r*V)
proof
let X be LinearTopSpace, V be Subset of X, r be non zero Real;
r*Int(V) c= r*V by CONVEX1:39,TOPS_1:16;
hence r*Int(V) c= Int(r*V) by Th49,TOPS_1:24;
let x be object;
assume
A1: x in Int(r*V);
then reconsider x as Point of X;
consider Q being Subset of X such that
A2: Q is open and
A3: Q c= r*V and
A4: x in Q by A1,TOPS_1:22;
r"*Q c= r"*(r*V) by A3,CONVEX1:39;
then r"*Q c= r"*r*V by CONVEX1:37;
then r"*Q c= 1*V by XCMPLX_0:def 7;
then
A5: r"*Q c= V by CONVEX1:32;
r"*x in r"*Q & r"*Q is open by A2,A4,Th49;
then r"*x in Int(V) by A5,TOPS_1:22;
then r*(r"*x) in r*Int(V);
then r*r"*x in r*Int(V) by RLVECT_1:def 7;
then 1*x in r*Int(V) by XCMPLX_0:def 7;
hence thesis by RLVECT_1:def 8;
end;
theorem Th52:
for X being LinearTopSpace, A being Subset of X, r being non
zero Real holds r*Cl(A) = Cl(r*A)
proof
let X be LinearTopSpace, A be Subset of X, r be non zero Real;
thus r*Cl(A) c= Cl(r*A)
proof
let z be object;
assume
A1: z in r*Cl(A);
then reconsider z as Point of X;
now
let G be Subset of X;
assume G is open & z in G;
then
A2: r"*z in r"*G & r"*G is open by Th49;
consider v being Point of X such that
A3: z = r*v and
A4: v in Cl A by A1;
r"*z = r"*r*v by A3,RLVECT_1:def 7
.= 1*v by XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
then A meets r"*G by A4,A2,PRE_TOPC:24;
then consider x being object such that
A5: x in A and
A6: x in r"*G by XBOOLE_0:3;
reconsider x as Point of X by A5;
consider u being Point of X such that
A7: x = r"*u and
A8: u in G by A6;
A9: r*x in r*A by A5;
r*x = r*r"*u by A7,RLVECT_1:def 7
.= 1*u by XCMPLX_0:def 7
.= u by RLVECT_1:def 8;
hence r*A meets G by A8,A9,XBOOLE_0:3;
end;
hence thesis by PRE_TOPC:24;
end;
r*A c= r*Cl(A) by CONVEX1:39,PRE_TOPC:18;
hence thesis by Th50,TOPS_1:5;
end;
theorem
for X being LinearTopSpace,A being Subset of X st X is T_1 holds 0*Cl(
A) = Cl(0*A)
proof
let X be LinearTopSpace, A be Subset of X such that
A1: X is T_1;
per cases;
suppose
A2: A is empty;
then
A3: Cl A = {}X by PRE_TOPC:22;
hence 0*Cl(A) = {}X by CONVEX1:33
.= Cl(0*A) by A2,A3,CONVEX1:33;
end;
suppose
A4: A is non empty;
then Cl A is non empty by PRE_TOPC:18,XBOOLE_1:3;
hence 0*Cl(A) = {0.X} by CONVEX1:34
.= Cl {0.X} by A1,YELLOW_8:26
.= Cl(0*A) by A4,CONVEX1:34;
end;
end;
theorem Th54:
for X being LinearTopSpace, x being Point of X, V being
a_neighborhood of x, r be non zero Real
holds r*V is a_neighborhood of r*x
proof
let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x, r be non
zero Real;
x in Int(V) by CONNSP_2:def 1;
then r*x in r*Int(V);
hence r*x in Int(r*V) by Th51;
end;
theorem Th55:
for X being LinearTopSpace, V being a_neighborhood of 0.X, r be
non zero Real holds r*V is a_neighborhood of 0.X
proof
let X be LinearTopSpace, V be a_neighborhood of 0.X,
r be non zero Real;
r*V is a_neighborhood of r*0.X by Th54;
hence thesis;
end;
Lm15: for X being LinearTopSpace, V being bounded Subset of X,
r being Real
holds r*V is bounded
proof
let X be LinearTopSpace, V be bounded Subset of X;
let r be Real;
per cases;
suppose
A1: r = 0;
per cases;
suppose
V is empty;
hence thesis by CONVEX1:33;
end;
suppose
A2: V is non empty;
let U be a_neighborhood of 0.X;
take s = 1;
thus s > 0;
let t;
assume t > s;
then t*U is a_neighborhood of 0.X by Th55;
then
A3: 0.X in t*U by CONNSP_2:4;
r*V = {0.X} by A1,A2,CONVEX1:34;
hence thesis by A3,ZFMISC_1:31;
end;
end;
suppose
A4: r <> 0;
let U be a_neighborhood of 0.X;
(1/r)*U is a_neighborhood of 0.X by A4,Th55;
then consider s such that
A5: s > 0 and
A6: for t st t > s holds V c= t*((1/r)*U) by Def12;
take s;
thus s > 0 by A5;
let t;
assume t > s;
then r*V c= r*(t*((1/r)*U)) by A6,CONVEX1:39;
then r*V c= r*(t*(1/r)*U) by CONVEX1:37;
then r*V c= r*((1/r)*(t*U)) by CONVEX1:37;
then r*V c= r*(1/r)*(t*U) by CONVEX1:37;
then r*V c= 1*(t*U) by A4,XCMPLX_1:87;
then
A7: r*V c= t*U by CONVEX1:32;
let x be object;
assume x in r*V;
hence thesis by A7;
end;
end;
registration
let X be LinearTopSpace, V be bounded Subset of X, r be Real;
cluster r*V -> bounded;
coherence by Lm15;
end;
theorem Th56:
for X being LinearTopSpace, 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
let X be LinearTopSpace, W be a_neighborhood of 0.X;
0.X+0.X = 0.X;
then consider
V1 being a_neighborhood of 0.X, V2 being a_neighborhood of 0.X such
that
A1: V1+V2 c= W by Th31;
set U = Int(V1) /\ Int(V2) /\ ((-1)*Int(V1)) /\ ((-1)*Int(V2));
A2: (-1)*Int(V1) is open & (-1)*Int(V2) is open by Th49;
(-1)*V2 is a_neighborhood of 0.X by Th55;
then 0.X in Int((-1)*V2) by CONNSP_2:def 1;
then
A3: 0.X in (-1)*Int(V2) by Th51;
(-1)*V1 is a_neighborhood of 0.X by Th55;
then 0.X in Int((-1)*V1) by CONNSP_2:def 1;
then
A4: 0.X in (-1)*Int(V1) by Th51;
0.X in Int V1 & 0.X in Int V2 by CONNSP_2:def 1;
then 0.X in Int(V1) /\ Int(V2) by XBOOLE_0:def 4;
then 0.X in Int(V1) /\ Int(V2) /\ ((-1)*Int(V1)) by A4,XBOOLE_0:def 4;
then 0.X in U by A3,XBOOLE_0:def 4;
then 0.X in Int(U) by A2,TOPS_1:23;
then reconsider U as open a_neighborhood of 0.X by A2,CONNSP_2:def 1;
take U;
(-1)*(-1)*Int(V1) = Int(V1) by CONVEX1:32;
then
A5: (-1)*((-1)*Int(V1)) = Int(V1) by CONVEX1:37;
(-1)*(-1)*Int(V2) = Int(V2) by CONVEX1:32;
then
A6: (-1)*((-1)*Int(V2)) = Int(V2) by CONVEX1:37;
thus U = Int(V1) /\ Int(V2) /\ (((-1)*Int(V1)) /\ ((-1)*Int(V2))) by
XBOOLE_1:16
.= (-1)*(Int(V1) /\ Int(V2)) /\ (Int(V1) /\ Int(V2)) by Th15
.= (-1)*(Int(V1) /\ Int(V2)) /\ ((-1)*((-1)*Int(V1) /\ ((-1)*Int(V2))))
by A5,A6,Th15
.= (-1)*(Int(V1) /\ Int(V2) /\ ((-1)*Int(V1) /\ ((-1)*Int(V2)))) by Th15
.= -U by XBOOLE_1:16;
let x be object;
assume x in U + U;
then x in {u + v where u,v is Point of X: u in U & v in U} by RUSUB_4:def 9;
then consider u,v being Point of X such that
A7: u+v = x and
A8: u in U and
A9: v in U;
A10: U = Int(V1) /\ Int(V2) /\ (((-1)*Int(V1)) /\ ((-1)*Int(V2))) by
XBOOLE_1:16;
then v in Int(V1) /\ Int(V2) by A9,XBOOLE_0:def 4;
then
A11: v in Int(V2) by XBOOLE_0:def 4;
Int(V1) c= V1 & Int(V2) c= V2 by TOPS_1:16;
then
A12: Int(V1)+Int(V2) c= V1+V2 by Th11;
u in Int(V1) /\ Int(V2) by A8,A10,XBOOLE_0:def 4;
then u in Int(V1) by XBOOLE_0:def 4;
then
u+v in {u9+v9 where u9,v9 is Point of X: u9 in Int(V1) & v9 in Int(V2)}
by A11;
then u+v in Int(V1)+Int(V2) by RUSUB_4:def 9;
then u+v in V1+V2 by A12;
hence thesis by A1,A7;
end;
theorem Th57:
for X being LinearTopSpace, K being compact Subset of X, C being
closed Subset of X st K misses C ex V being a_neighborhood of 0.X st K+V misses
C+V
proof
let X be LinearTopSpace, K be compact Subset of X, C be closed Subset of X
such that
A1: K misses C;
per cases;
suppose
A2: K = {};
take V = [#]X;
thus V is a_neighborhood of 0.X by TOPGRP_1:21;
K+V = {} by A2,CONVEX1:40;
hence thesis;
end;
suppose
A3: K <> {};
set xV = { [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0.X:
x in K & Vx is symmetric & x+Vx+Vx+Vx misses C};
A4: now
let x be Point of X such that
A5: x in K;
-x+C` = {-x + u where u is Point of X: u in C`} & K c= C` by A1,
RUSUB_4:def 8,SUBSET_1:23;
then -x+x in -x+C` by A5;
then 0.X in -x+C` by RLVECT_1:5;
then -x+C` is a_neighborhood of 0.X by CONNSP_2:3;
then consider V9 being open a_neighborhood of 0.X such that
V9 is symmetric and
A6: V9+V9 c= -x+C` by Th56;
consider Vx being open a_neighborhood of 0.X such that
A7: Vx is symmetric and
A8: Vx+Vx c= V9 by Th56;
take Vx;
thus Vx is symmetric by A7;
Vx c= V9
proof
let z be object;
assume
A9: z in Vx;
then reconsider z as Point of X;
0.X in Vx by CONNSP_2:4;
then z+0.X in Vx+Vx by A9,Th3;
then z in Vx+Vx;
hence thesis by A8;
end;
then Vx+(Vx+Vx) c= V9 + V9 by A8,Th11;
then Vx+Vx+Vx c=-x+C` by A6;
then x+(Vx+Vx+Vx) c= x+(-x+C`) by Th8;
then x+Vx+(Vx+Vx) c= x+(-x+C`) by Th7;
then x+Vx+Vx+Vx c= x+(-x+C`) by CONVEX1:36;
then x+Vx+Vx+Vx c= x+-x+C` by Th6;
then x+Vx+Vx+Vx c= 0.X+C` by RLVECT_1:def 10;
then x+Vx+Vx+Vx c= C` by Th5;
hence x+Vx+Vx+Vx misses C by SUBSET_1:23;
end;
A10: now
consider x be object such that
A11: x in K by A3,XBOOLE_0:def 1;
reconsider x as Point of X by A11;
consider Vx being open a_neighborhood of 0.X such that
A12: Vx is symmetric & x+Vx+Vx+Vx misses C by A4,A11;
take z = [x,Vx];
thus z in xV by A11,A12;
end;
defpred P[object,object] means
ex v1,v2 being Point of X, V1,V2 being open
a_neighborhood of 0.X st $1 = [v1,V1] & $2 = [v2,V2] & v1+V1 = v2+V2;
A13: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z]
proof
let x,y,z be object;
given v1,v2 being Point of X, V1,V2 being open a_neighborhood of 0.X
such that
A14: x = [v1,V1] and
A15: y = [v2,V2] and
A16: v1+V1 = v2+V2;
given w1,w2 being Point of X, W1,W2 being open a_neighborhood of 0.X
such that
A17: y = [w1,W1] and
A18: z = [w2,W2] & w1+W1 = w2+W2;
take v1,w2,V1,W2;
v2 = w1 by A15,A17,XTUPLE_0:1;
hence thesis by A14,A15,A16,A17,A18,XTUPLE_0:1;
end;
reconsider xV as non empty set by A10;
A19: for x being object st x in xV holds P[x,x]
proof
let x be object;
assume x in xV;
then
ex v being Point of X, V being open a_neighborhood of 0.X st x = [v
,V] & v in K & V is symmetric & v+V+V+V misses C;
hence thesis;
end;
A20: for x,y being object st P[x,y] holds P[y,x];
consider eqR being Equivalence_Relation of xV such that
A21: for x,y being object holds [x,y] in eqR iff x in xV & y in xV & P[x,
y] from EQREL_1:sch 1(A19,A20,A13);
now
let X be set;
assume X in Class eqR;
then ex x being object st x in xV & X = Class(eqR,x) by EQREL_1:def 3;
hence X <> {} by EQREL_1:20;
end;
then consider g being Function such that
A22: dom g = Class eqR and
A23: for X being set st X in Class eqR holds g.X in X by FUNCT_1:111;
set xVV = rng g;
set F = { x+Vx where x is Point of X, Vx is open a_neighborhood of 0.X: [x
,Vx] in xVV};
F c= bool the carrier of X
proof
let A be object;
assume A in F;
then
ex x being Point of X, Vx being open a_neighborhood of 0.X st A = x
+Vx & [x,Vx] in xVV;
hence thesis;
end;
then reconsider F as Subset-Family of X;
A24: F is Cover of K
proof
let x be object;
assume
A25: x in K;
then reconsider x as Point of X;
consider Vx being open a_neighborhood of 0.X such that
A26: Vx is symmetric & x+Vx+Vx+Vx misses C by A4,A25;
[x,Vx] in xV by A25,A26;
then
A27: Class(eqR,[x,Vx]) in Class eqR by EQREL_1:def 3;
then
A28: g.Class(eqR,[x,Vx]) in xVV by A22,FUNCT_1:def 3;
x+0.X in x+Vx by Lm1,CONNSP_2:4;
then
A29: x in x+Vx;
g.Class(eqR,[x,Vx]) in Class(eqR,[x,Vx]) by A23,A27;
then [g.Class(eqR,[x,Vx]),[x,Vx]] in eqR by EQREL_1:19;
then consider
v1,v2 being Point of X, V1,V2 being open a_neighborhood of 0.X
such that
A30: g.Class(eqR,[x,Vx]) = [v1,V1] and
A31: [x,Vx] = [v2,V2] and
A32: v1+V1 = v2+V2 by A21;
x = v2 & Vx = V2 by A31,XTUPLE_0:1;
then x+Vx in F by A30,A32,A28;
hence thesis by A29,TARSKI:def 4;
end;
F is open
proof
let P be Subset of X;
assume P in F;
then
ex x being Point of X, Vx being open a_neighborhood of 0.X st P = x
+Vx & [x,Vx] in xVV;
hence thesis;
end;
then consider G being Subset-Family of X such that
A33: G c= F and
A34: G is Cover of K and
A35: G is finite by A24,COMPTS_1:def 4;
set FVx = {Vx where Vx is open a_neighborhood of 0.X: ex x being Point of
X st x+Vx in G & [x,Vx] in xVV};
FVx c= bool the carrier of X
proof
let A be object;
assume A in FVx;
then ex Vx being open a_neighborhood of 0.X st A = Vx & ex x being
Point of X st x+Vx in G & [x,Vx] in xVV;
hence thesis;
end;
then reconsider FVx as Subset-Family of X;
defpred P[object,object] means ex x being Point of X, Vx being open
a_neighborhood of 0.X st $1 = x+Vx & x+Vx in G & [x,Vx] in xVV & $2 = Vx;
A36: for x being object st x in G ex y being object st y in FVx & P[x,y]
proof
let x be object;
assume
A37: x in G;
then x in F by A33;
then consider
z being Point of X, Vz being open a_neighborhood of 0.X such
that
A38: x = z+Vz & [z,Vz] in xVV;
take Vz;
thus thesis by A37,A38;
end;
consider f being Function of G,FVx such that
A39: for x being object st x in G holds P[x,f.x] from FUNCT_2:sch 1(A36
);
set FxVxVx = {x+Vx+Vx where x is Point of X, Vx is open a_neighborhood of
0.X : x+Vx in G & [x,Vx] in xVV};
take V = meet FVx;
A40: rng g c= xV
proof
let x be object;
assume x in rng g;
then consider y being object such that
A41: y in dom g and
A42: x = g.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
x in y by A22,A23,A41,A42;
hence thesis by A22,A41;
end;
A43: for A being Subset of X st A in G ex x being Point of X, Vx being
open a_neighborhood of 0.X st A = x+Vx & [x,Vx] in xVV
proof
let A be Subset of X;
assume A in G;
then A in F by A33;
hence thesis;
end;
A44: now
consider y be Point of X such that
A45: y in K by A3,SUBSET_1:4;
consider W being Subset of X such that
y in W and
A46: W in G by A34,A45,Th2;
consider x being Point of X, Vx being open a_neighborhood of 0.X such
that
A47: W = x+Vx & [x,Vx] in xVV by A43,A46;
Vx in FVx by A46,A47;
hence ex z being set st z in FVx;
end;
then
A48: dom f = G by FUNCT_2:def 1;
A49: FVx c= rng f
proof
let z be object;
assume z in FVx;
then consider Vx being open a_neighborhood of 0.X such that
A50: z = Vx and
A51: ex x being Point of X st x+Vx in G & [x,Vx] in xVV;
consider x being Point of X such that
A52: x+Vx in G and
A53: [x,Vx] in xVV by A51;
consider v being Point of X, Vv being open a_neighborhood of 0.X such
that
A54: x+Vx = v+Vv and
v+Vv in G and
A55: [v,Vv] in xVV and
A56: f.(x+Vx) = Vv by A39,A52;
[[x,Vx],[v,Vv]] in eqR by A21,A40,A53,A54,A55;
then [x,Vx] in Class(eqR,[v,Vv]) by EQREL_1:19;
then
A57: Class(eqR,[v,Vv]) = Class(eqR,[x,Vx]) by A40,A55,EQREL_1:23;
consider A being object such that
A58: A in dom g and
A59: [x,Vx] = g.A by A53,FUNCT_1:def 3;
consider a being object such that
A60: a in xV and
A61: A = Class(eqR,a) by A22,A58,EQREL_1:def 3;
[x,Vx] in Class(eqR,a) by A22,A23,A58,A59,A61;
then
A62: Class(eqR,a) = Class(eqR,[x,Vx]) by A60,EQREL_1:23;
consider B being object such that
A63: B in dom g and
A64: [v,Vv] = g.B by A55,FUNCT_1:def 3;
consider b being object such that
A65: b in xV and
A66: B = Class(eqR,b) by A22,A63,EQREL_1:def 3;
[v,Vv] in Class(eqR,b) by A22,A23,A63,A64,A66;
then [x,Vx] = [v,Vv] by A57,A59,A64,A61,A65,A66,A62,EQREL_1:23;
then Vx = Vv by XTUPLE_0:1;
hence thesis by A48,A50,A52,A56,FUNCT_1:3;
end;
A67: for x being Point of X, Vx being open a_neighborhood of 0.X st x+Vx
in G & [x,Vx] in xVV holds x in K & Vx is symmetric & x+Vx+Vx+Vx misses C
proof
let x be Point of X, Vx be open a_neighborhood of 0.X such that
A68: x+Vx in G and
A69: [x,Vx] in xVV;
consider A being object such that
A70: A in dom g and
A71: [x,Vx] = g.A by A69,FUNCT_1:def 3;
consider a being object such that
A72: a in xV and
A73: A = Class(eqR,a) by A22,A70,EQREL_1:def 3;
[x,Vx] in Class(eqR,a) by A22,A23,A70,A71,A73;
then
A74: Class(eqR,a) = Class(eqR,[x,Vx]) by A72,EQREL_1:23;
x+Vx in F by A33,A68;
then consider
v being Point of X, Vv being open a_neighborhood of 0.X such
that
A75: x+Vx = v+Vv and
A76: [v,Vv] in xVV;
[[x,Vx],[v,Vv]] in eqR by A21,A40,A69,A75,A76;
then [x,Vx] in Class(eqR,[v,Vv]) by EQREL_1:19;
then
A77: Class(eqR,[v,Vv]) = Class(eqR,[x,Vx]) by A40,A76,EQREL_1:23;
consider B being object such that
A78: B in dom g and
A79: [v,Vv] = g.B by A76,FUNCT_1:def 3;
consider b being object such that
A80: b in xV and
A81: B = Class(eqR,b) by A22,A78,EQREL_1:def 3;
[v,Vv] in Class(eqR,b) by A22,A23,A78,A79,A81;
then
A82: [x,Vx] = [v,Vv] by A77,A71,A79,A73,A80,A81,A74,EQREL_1:23;
then
A83: Vx = Vv by XTUPLE_0:1;
[v,Vv] in xV by A40,A76;
then consider
u being Point of X, Vu being open a_neighborhood of 0.X such
that
A84: [u,Vu] = [v,Vv] and
A85: u in K & Vu is symmetric & u+Vu+Vu+Vu misses C;
Vv = Vu by A84,XTUPLE_0:1;
hence thesis by A84,A85,A82,A83,XTUPLE_0:1;
end;
now
let Z be set;
hereby
reconsider A = C+V as set;
assume Z in {{}};
then
A86: Z = {} by TARSKI:def 1;
consider y be Point of X such that
A87: y in K by A3,SUBSET_1:4;
consider W being Subset of X such that
y in W and
A88: W in G by A34,A87,Th2;
consider x being Point of X, Vx being open a_neighborhood of 0.X such
that
A89: W = x+Vx & [x,Vx] in xVV by A43,A88;
A90: x+Vx+Vx+Vx misses C by A67,A88,A89;
reconsider B = x+Vx+Vx as set;
take A,B;
thus A in {C+V} by TARSKI:def 1;
thus B in FxVxVx by A88,A89;
A91: Vx is symmetric by A67,A88,A89;
now
A92: C+V = {u + v where u,v is Point of X: u in C & v in V} by
RUSUB_4:def 9;
assume A meets B;
then consider z being object such that
A93: z in A and
A94: z in B by XBOOLE_0:3;
reconsider z as Point of X by A93;
consider u,v being Point of X such that
A95: z = u+v and
A96: u in C and
A97: v in V by A93,A92;
Vx in FVx by A88,A89;
then v in Vx by A97,SETFAM_1:def 1;
then -v in Vx by A91,Th25;
then
A98: z+-v in x+Vx+Vx+Vx by A94,Th3;
z+-v = u+(v+-v) by A95,RLVECT_1:def 3
.= u+0.X by RLVECT_1:5
.= u;
hence contradiction by A90,A96,A98,XBOOLE_0:3;
end;
hence Z = A /\ B by A86;
end;
given A,B being set such that
A99: A in {C+V} and
A100: B in FxVxVx and
A101: Z = A /\ B;
A102: A = C+V by A99,TARSKI:def 1;
consider x being Point of X, Vx being open a_neighborhood of 0.X such
that
A103: B = x+Vx+Vx and
A104: x+Vx in G & [x,Vx] in xVV by A100;
A105: x+Vx+Vx+Vx misses C by A67,A104;
A106: Vx is symmetric by A67,A104;
now
A107: C+V = {u + v where u,v is Point of X: u in C & v in V} by RUSUB_4:def 9
;
assume A meets B;
then consider z being object such that
A108: z in A and
A109: z in B by XBOOLE_0:3;
reconsider z as Point of X by A99,A108;
consider u,v being Point of X such that
A110: z = u+v and
A111: u in C and
A112: v in V by A102,A108,A107;
Vx in FVx by A104;
then v in Vx by A112,SETFAM_1:def 1;
then -v in Vx by A106,Th25;
then
A113: z+-v in x+Vx+Vx+Vx by A103,A109,Th3;
z+-v = u+(v+-v) by A110,RLVECT_1:def 3
.= u+0.X by RLVECT_1:5
.= u;
hence contradiction by A105,A111,A113,XBOOLE_0:3;
end;
then A /\ B = {};
hence Z in {{}} by A101,TARSKI:def 1;
end;
then INTERSECTION ({C+V}, FxVxVx) = {{}} by SETFAM_1:def 5;
then union INTERSECTION ({C+V}, FxVxVx) = {} by ZFMISC_1:25;
then (C+V) /\ union FxVxVx = {} by SETFAM_1:25;
then
A114: C+V misses union FxVxVx;
A115: FVx is open
proof
let P be Subset of X;
assume P in FVx;
then ex Vx being open a_neighborhood of 0.X st P = Vx & ex x being
Point of X st x+Vx in G& [x,Vx] in xVV;
hence thesis;
end;
f"FVx is finite by A35,FINSET_1:1;
then FVx is finite by A49,FINSET_1:9;
then V is open by A115,TOPS_2:20;
then
A116: Int V = V by TOPS_1:23;
now
let A be set;
assume
A117: A in FVx;
then reconsider A9=A as Subset of X;
ex Vx being open a_neighborhood of 0.X st A = Vx & ex x being
Point of X st x+Vx in G & [x,Vx] in xVV by A117;
then Int A9 c= A9 & 0.X in Int A9 by CONNSP_2:def 1,TOPS_1:16;
hence 0.X in A;
end;
then 0.X in V by A44,SETFAM_1:def 1;
hence V is a_neighborhood of 0.X by A116,CONNSP_2:def 1;
set FxVxV = {x+Vx+V where x is Point of X, Vx is open a_neighborhood of 0.
X: x+Vx in G & [x,Vx] in xVV};
A118: union FxVxV c= union FxVxVx
proof
let z be object;
assume z in union FxVxV;
then consider Y being set such that
A119: z in Y and
A120: Y in FxVxV by TARSKI:def 4;
consider x being Point of X, Vx being open a_neighborhood of 0.X such
that
A121: Y = x+Vx+V and
A122: x+Vx in G & [x,Vx] in xVV by A120;
A123: x+Vx+Vx in FxVxVx by A122;
x+Vx+V = {u + v where u,v is Point of X: u in x+Vx & v in V} by
RUSUB_4:def 9;
then consider u,v being Point of X such that
A124: z = u+v and
A125: u in x+Vx and
A126: v in V by A119,A121;
Vx in FVx by A122;
then v in Vx by A126,SETFAM_1:def 1;
then u+v in x+Vx+Vx by A125,Th3;
hence thesis by A124,A123,TARSKI:def 4;
end;
K+V c= union FxVxV
proof
let z be object;
A127: K+V = {u + v where u,v is Point of X: u in K & v in V} by RUSUB_4:def 9;
assume z in K+V;
then consider u,v being Point of X such that
A128: z = u+v and
A129: u in K and
A130: v in V by A127;
consider Vu being Subset of X such that
A131: u in Vu and
A132: Vu in G by A34,A129,Th2;
consider x being Point of X, Vx being open a_neighborhood of 0.X such
that
A133: Vu = x+Vx and
A134: [x,Vx] in xVV by A43,A132;
A135: x+Vx+V in FxVxV by A132,A133,A134;
z in x+Vx+V by A128,A130,A131,A133,Th3;
hence thesis by A135,TARSKI:def 4;
end;
hence thesis by A118,A114,XBOOLE_1:1,63;
end;
end;
theorem Th58:
for X being LinearTopSpace, B being local_base of X, V being
a_neighborhood of 0.X ex W being a_neighborhood of 0.X st W in B & Cl W c= V
proof
let X be LinearTopSpace, B be local_base of X;
let V be a_neighborhood of 0.X;
set C = (Int V)`;
set K = {0.X};
0.X in Int V by CONNSP_2:def 1;
then not 0.X in (Int V)` by XBOOLE_0:def 5;
then consider P being a_neighborhood of 0.X such that
A1: K+P misses C+P by Th57,ZFMISC_1:50;
A2: 0.X in Int P by CONNSP_2:def 1;
then reconsider P9 = Int P as open a_neighborhood of 0.X by CONNSP_2:3;
K+P9 c= K+P & C+P9 c= C+P by Lm3,TOPS_1:16;
then K+P9 misses C+P9 by A1,XBOOLE_1:64;
then Cl(K+P9) misses C+P9 by TSEP_1:36;
then Cl(K+P9) misses C by A2,Th12,XBOOLE_1:63;
then Cl P9 misses C by CONVEX1:35;
then
A3: Cl P9 c= Int V by SUBSET_1:24;
consider W being a_neighborhood of 0.X such that
A4: W in B and
A5: W c= P9 by YELLOW13:def 2;
take W;
thus W in B by A4;
A6: Cl W c= Cl P9 by A5,PRE_TOPC:19;
Int V c= V by TOPS_1:16;
then Cl P9 c= V by A3;
hence thesis by A6;
end;
theorem Th59:
for X being LinearTopSpace, V being a_neighborhood of 0.X ex W
being a_neighborhood of 0.X st Cl W c= V
proof
let X be LinearTopSpace, V be a_neighborhood of 0.X;
set B = the set of all U where U is a_neighborhood of 0.X;
B c= bool the carrier of X
proof
let A be object;
assume A in B;
then ex U being a_neighborhood of 0.X st A = U;
hence thesis;
end;
then B is local_base of X by Th44;
then consider W being a_neighborhood of 0.X such that
W in B and
A1: Cl W c= V by Th58;
take W;
thus thesis by A1;
end;
registration
cluster T_1 -> Hausdorff for LinearTopSpace;
coherence
proof
let X be LinearTopSpace;
assume
A1: X is T_1;
let p, q be Point of X;
assume
A2: p <> q;
{q} is closed by A1,URYSOHN1:19;
then consider V being a_neighborhood of 0.X such that
A3: {p}+V misses {q}+V by A2,Th57,ZFMISC_1:11;
take p+Int(V),q+Int(V);
A4: {p}+V = p+V & {q}+V = q+V by RUSUB_4:33;
thus p+Int(V) is open & q+Int(V) is open;
0.X in Int(V) by CONNSP_2:def 1;
then p+0.X in p+Int(V) & q+0.X in q+Int(V) by Lm1;
hence p in p+Int(V) & q in q+Int(V);
p+Int(V) c= p+V & q+Int(V) c= q+V by Th8,TOPS_1:16;
hence thesis by A3,A4,XBOOLE_1:64;
end;
end;
theorem
for X being LinearTopSpace, A being Subset of X holds Cl A = meet the set of
all A+V
where V is a_neighborhood of 0.X
proof
let X be LinearTopSpace, A be Subset of X;
set AV = the set of all A+V where V is a_neighborhood of 0.X;
set V = the a_neighborhood of 0.X;
A1: for x being Point of X, V being a_neighborhood of 0.X holds A meets x+
Int(V) iff x in A+(-1)*Int(V)
proof
let x be Point of X, V be a_neighborhood of 0.X;
A2: A+(-1)*Int(V) = {a+v where a,v is Point of X: a in A & v in (-1)*Int(
V)} by RUSUB_4:def 9;
hereby
assume A meets x+Int(V);
then x in A+-Int(V) by Th24;
hence x in A+(-1)*Int(V);
end;
assume x in A+(-1)*Int(V);
then consider a,v being Point of X such that
A3: x = a+v and
A4: a in A and
A5: v in (-1)*Int(V) by A2;
consider v9 being Point of X such that
A6: v = (-1)*v9 and
A7: v9 in Int(V) by A5;
-v = (-1)*v by RLVECT_1:16
.= (-1)*(-1)*v9 by A6,RLVECT_1:def 7
.= v9 by RLVECT_1:def 8;
then
A8: x+v9 = a + (v + (-v)) by A3,RLVECT_1:def 3
.= a+0.X by RLVECT_1:5
.= a;
x+Int(V) = {x+w where w is Point of X: w in Int(V)} by RUSUB_4:def 8;
then x+v9 in x+Int(V) by A7;
hence thesis by A4,A8,XBOOLE_0:3;
end;
AV c= bool the carrier of X
proof
let x be object;
assume x in AV;
then ex V being a_neighborhood of 0.X st x = A+V;
hence thesis;
end;
then reconsider AV9 = AV as Subset-Family of X;
A9: for x being Point of X holds x in Cl A iff for V being a_neighborhood of
0.X holds A meets x+Int(V)
proof
let x be Point of X;
hereby
assume
A10: x in Cl A;
let V be a_neighborhood of 0.X;
0.X in Int(V) by CONNSP_2:def 1;
then x+0.X in x+Int(V) by Lm1;
then x in x+Int(V);
hence A meets x+Int(V) by A10,TOPS_1:12;
end;
assume
A11: for V being a_neighborhood of 0.X holds A meets x+Int(V);
now
let V be Subset of X such that
A12: V is open and
A13: x in V;
A14: Int(-x+V) = -x+V by A12,TOPS_1:23;
-x+x in -x+V by A13,Lm1;
then 0.X in -x+V by RLVECT_1:5;
then -x+V is a_neighborhood of 0.X by A14,CONNSP_2:def 1;
then A meets x+(-x+V) by A11,A14;
then A meets x+-x+V by Th6;
then A meets 0.X+V by RLVECT_1:5;
hence A meets V by Th5;
end;
hence thesis by TOPS_1:12;
end;
A15: A+V in AV;
thus Cl A c= meet AV
proof
let x be object;
assume
A16: x in Cl A;
then reconsider x as Point of X;
now
let Y be set;
assume Y in AV;
then consider V being a_neighborhood of 0.X such that
A17: Y = A+V;
A18: A+V = {a+v where a,v is Point of X: a in A & v in V} by RUSUB_4:def 9;
A19: (-1)*V is a_neighborhood of 0.X by Th55;
then A meets x+Int((-1)*V) by A9,A16;
then
A+(-1)*Int((-1)*V) = {a+v where a,v is Point of X: a in A & v in (-
1)*Int((-1 )*V)} & x in A+(-1)*Int(((-1)*V)) by A1,A19,RUSUB_4:def 9;
then consider a,v being Point of X such that
A20: x = a+v & a in A and
A21: v in (-1)*Int((-1)*V);
consider v9 being Point of X such that
A22: v=(-1)*v9 and
A23: v9 in Int((-1)*V) by A21;
Int((-1)*V) c= (-1)*V by TOPS_1:16;
then v9 in (-1)*V by A23;
then consider v99 being Point of X such that
A24: v9 = (-1)*v99 and
A25: v99 in V;
v = (-1)*(-1)*v99 by A22,A24,RLVECT_1:def 7
.= v99 by RLVECT_1:def 8;
hence x in Y by A17,A18,A20,A25;
end;
hence thesis by A15,SETFAM_1:def 1;
end;
let x be object;
assume
A26: x in meet AV;
meet AV9 c= the carrier of X;
then reconsider x as Point of X by A26;
now
let V be a_neighborhood of 0.X;
0.X in Int(V) by CONNSP_2:def 1;
then Int(V) is a_neighborhood of 0.X by CONNSP_2:3;
then (-1)*Int(V) is a_neighborhood of 0.X by Th55;
then A+(-1)*Int(V) in AV;
then x in A+(-1)*Int(V) by A26,SETFAM_1:def 1;
hence A meets x+Int(V) by A1;
end;
hence thesis by A9;
end;
theorem Th61:
for X being LinearTopSpace, A,B being Subset of X holds Int A +
Int B c= Int(A+B)
proof
let X be LinearTopSpace, A,B be Subset of X;
Int A c= A & Int B c= B by TOPS_1:16;
then Int A + Int B c= A+B by Th11;
hence thesis by TOPS_1:24;
end;
theorem Th62:
for X being LinearTopSpace, A,B being Subset of X holds Cl A +
Cl B c= Cl(A+B)
proof
let X be LinearTopSpace, A,B be Subset of X;
let z be object;
assume
A1: z in Cl A + Cl B;
then reconsider z as Point of X;
{u + v where u,v is Point of X: u in Cl A & v in Cl B} = Cl A + Cl B by
RUSUB_4:def 9;
then consider a,b being Point of X such that
A2: z = a+b and
A3: a in Cl A and
A4: b in Cl B by A1;
now
let W be Subset of X such that
A5: W is open and
A6: z in W;
W is a_neighborhood of z by A5,A6,CONNSP_2:3;
then consider
W1 being a_neighborhood of a, W2 being a_neighborhood of b such
that
A7: W1+W2 c= W by A2,Th31;
a in Int W1 by CONNSP_2:def 1;
then A meets Int W1 by A3,TOPS_1:12;
then consider x being object such that
A8: x in A and
A9: x in Int W1 by XBOOLE_0:3;
reconsider x as Point of X by A8;
A10: Int W1 + Int W2 c= Int W by A7,Th36;
b in Int W2 by CONNSP_2:def 1;
then B meets Int W2 by A4,TOPS_1:12;
then consider y being object such that
A11: y in B and
A12: y in Int W2 by XBOOLE_0:3;
reconsider y as Point of X by A11;
x+y in A+B & x+y in Int W1 + Int W2 by A8,A9,A11,A12,Th3;
then A+B meets Int W by A10,XBOOLE_0:3;
hence A+B meets W by A5,TOPS_1:23;
end;
hence thesis by TOPS_1:12;
end;
Lm16: for X being LinearTopSpace, C being convex Subset of X holds Cl C is
convex
proof
let X be LinearTopSpace, C be convex Subset of X;
now
let r be Real such that
A1: 0 < r and
A2: r < 1;
r*C + (1-r)*C c= C by A1,A2,CONVEX1:4;
then
A3: Cl(r*C + (1-r)*C) c= Cl(C) by PRE_TOPC:19;
0+r < 1 by A2;
then 0 < 1-r by XREAL_1:20;
then
A4: (1-r)*Cl(C) = Cl((1-r)*C) by Th52;
A5: Cl(r*C) + Cl((1-r)*C) c= Cl(r*C + (1-r)*C) by Th62;
Cl(r*C) = r*Cl(C) by A1,Th52;
hence r*Cl(C) + (1-r)*Cl(C) c= Cl(C) by A3,A5,A4;
end;
hence thesis by CONVEX1:4;
end;
registration
let X be LinearTopSpace, C be convex Subset of X;
cluster Cl C -> convex;
coherence by Lm16;
end;
Lm17: for X being LinearTopSpace, C being convex Subset of X holds Int C is
convex
proof
let X be LinearTopSpace, C be convex Subset of X;
now
let r be Real such that
A1: 0 < r and
A2: r < 1;
r*C + (1-r)*C c= C by A1,A2,CONVEX1:4;
then
A3: Int(r*C + (1-r)*C) c= Int(C) by TOPS_1:19;
0+r < 1 by A2;
then 0 < 1-r by XREAL_1:20;
then
A4: (1-r)*Int(C) = Int((1-r)*C) by Th51;
A5: Int(r*C) + Int((1-r)*C) c= Int(r*C + (1-r)*C) by Th61;
Int(r*C) = r*Int(C) by A1,Th51;
hence r*Int(C) + (1-r)*Int(C) c= Int(C) by A3,A5,A4;
end;
hence thesis by CONVEX1:4;
end;
registration
let X be LinearTopSpace, C be convex Subset of X;
cluster Int C -> convex;
coherence by Lm17;
end;
Lm18: for X being LinearTopSpace, B being circled Subset of X holds Cl B is
circled
proof
let X be LinearTopSpace, B be circled Subset of X;
let r be Real such that
A1: |.r.| <= 1;
per cases;
suppose
A2: r = 0;
now
per cases;
suppose
B = {}X;
then Cl B = {}X by PRE_TOPC:22;
hence thesis by CONVEX1:33;
end;
suppose
A3: B <> {}X;
A4: B c= Cl B by PRE_TOPC:18;
A5: 0.X in B by A3,Th27;
then r*Cl(B) = {0.X} by A2,A4,CONVEX1:34;
hence thesis by A5,A4,ZFMISC_1:31;
end;
end;
hence thesis;
end;
suppose
A6: r <> 0;
r*B c= B by A1,Def6;
then Cl(r*B) c= Cl(B) by PRE_TOPC:19;
hence thesis by A6,Th52;
end;
end;
registration
let X be LinearTopSpace, B be circled Subset of X;
cluster Cl B -> circled;
coherence by Lm18;
end;
theorem
for X being LinearTopSpace, B being circled Subset of X st 0.X in Int
B holds Int B is circled
proof
let X be LinearTopSpace, B be circled Subset of X such that
A1: 0.X in Int B;
let r be Real;
assume |.r.| <= 1;
then r*B c= B by Def6;
then
A2: Int(r*B) c= Int(B) by TOPS_1:19;
per cases;
suppose
r = 0;
then r*Int(B) = {0.X} by A1,CONVEX1:34;
hence thesis by A1,ZFMISC_1:31;
end;
suppose
r <> 0;
hence thesis by A2,Th51;
end;
end;
Lm19: for X being LinearTopSpace, E being bounded Subset of X holds Cl E is
bounded
proof
let X be LinearTopSpace, E be bounded Subset of X;
let V be a_neighborhood of 0.X;
consider W be a_neighborhood of 0.X such that
A1: Cl W c= V by Th59;
consider s such that
A2: s > 0 and
A3: for t st t > s holds E c= t*W by Def12;
take s;
thus s > 0 by A2;
let t;
assume t > s;
then
A4: Cl E c= Cl(t*W) & Cl(t*W) = t*Cl(W) by A2,A3,Th52,PRE_TOPC:19;
t*Cl(W) c= t*V by A1,CONVEX1:39;
hence thesis by A4;
end;
registration
let X be LinearTopSpace, E be bounded Subset of X;
cluster Cl E -> bounded;
coherence by Lm19;
end;
Lm20: for X being LinearTopSpace, U,V being a_neighborhood of 0.X, F being
Subset-Family of X, 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
let X be LinearTopSpace, U,V be a_neighborhood of 0.X, F be Subset-Family of
X, r be positive Real such that
A1: for s being Real st |.s.| < r holds s*V c= U and
A2: F = {a*V where a is Real: |.a.| < r};
set W = union F;
thus W is a_neighborhood of 0.X
proof
set F9 = {a*Int(V) where a is non zero Real: |.a.| < r};
consider a being Real such that
A3: 0 < a and
A4: a < r by XREAL_1:5;
reconsider a as Real;
0.X in Int(V) by CONNSP_2:def 1;
then a*0.X in a*Int(V);
then
A5: 0.X in a*Int(V);
A6: F9 c= bool the carrier of X
proof
let A be object;
assume A in F9;
then ex a being non zero Real st A = a*Int(V) & |.a.| < r;
hence thesis;
end;
|.a.| < r by A3,A4,ABSVALUE:def 1;
then a*Int(V) in F9 by A3;
then
A7: 0.X in union F9 by A5,TARSKI:def 4;
reconsider F9 as Subset-Family of X by A6;
union F9 c= W
proof
let x be object;
A8: Int V c= V by TOPS_1:16;
assume x in union F9;
then consider P being set such that
A9: x in P and
A10: P in F9 by TARSKI:def 4;
consider a being non zero Real such that
A11: P = a*Int(V) and
A12: |.a.| < r by A10;
ex v being Point of X st x = a*v & v in Int(V) by A9,A11;
then
A13: x in a*V by A8;
a*V in F by A2,A12;
hence thesis by A13,TARSKI:def 4;
end;
then
A14: Int union F9 c= Int W by TOPS_1:19;
F9 is open
proof
let P be Subset of X;
assume P in F9;
then ex a being non zero Real st P = a*Int(V) & |.a.| < r;
hence thesis by Th49;
end;
then union F9 is open by TOPS_2:19;
then 0.X in Int union F9 by A7,TOPS_1:23;
hence 0.X in Int W by A14;
end;
thus W is circled
proof
let s be Real;
assume |.s.| <= 1;
then
A15: |.s.|*r <= r by XREAL_1:153;
let z be object;
assume z in s*W;
then consider u being Point of X such that
A16: z = s*u and
A17: u in W;
consider Y being set such that
A18: u in Y and
A19: Y in F by A17,TARSKI:def 4;
consider a being Real such that
A20: Y = a*V and
A21: |.a.| < r by A2,A19;
consider v being Point of X such that
A22: u = a*v and
A23: v in V by A18,A20;
z = s*a*v by A16,A22,RLVECT_1:def 7;
then
A24: z in s*a*V by A23;
per cases;
suppose
0 <> |.s.|;
then s <> 0 by ABSVALUE:2;
then 0 < |.s.| by COMPLEX1:47;
then |.s.|*|.a.| < |.s.| * r by A21,XREAL_1:68;
then |.s.|*|.a.| < r by A15,XXREAL_0:2;
then |.s*a.| < r by COMPLEX1:65;
then s*a*V in F by A2;
hence thesis by A24,TARSKI:def 4;
end;
suppose
|.s.| = 0;
then s = 0 by ABSVALUE:2;
then |.s*a.| = 0 by ABSVALUE:def 1;
then s*a*V in F by A2;
hence thesis by A24,TARSKI:def 4;
end;
end;
let z be object;
assume
A25: z in W;
then reconsider z as Point of X;
consider Y being set such that
A26: z in Y and
A27: Y in F by A25,TARSKI:def 4;
consider a being Real such that
A28: Y = a*V and
A29: |.a.| < r by A2,A27;
a*V c= U by A1,A29;
hence thesis by A26,A28;
end;
theorem Th64:
for X being LinearTopSpace, U being a_neighborhood of 0.X ex W
being a_neighborhood of 0.X st W is circled & W c= U
proof
let X be LinearTopSpace, U be a_neighborhood of 0.X;
0.X = 0*0.X;
then consider r being positive Real,
V being a_neighborhood of 0.X such that
A1: for s being Real st |.s-0 .| < r holds s*V c= U by Th32;
set F = {a*V where a is Real: |.a.| < r};
F c= bool the carrier of X
proof
let A be object;
assume A in F;
then ex a being Real st A = a*V & |.a.| < r;
hence thesis;
end;
then reconsider F as Subset-Family of X;
take union F;
now
let s be Real;
assume |.s.| < r;
then |.s-0 .| < r;
hence s*V c= U by A1;
end;
hence thesis by Lm20;
end;
theorem
for X being LinearTopSpace, U being a_neighborhood of 0.X st U
is convex ex W being a_neighborhood of 0.X st W is circled convex & W c= U
proof
let X be LinearTopSpace, U be a_neighborhood of 0.X such that
A1: U is convex;
set V = U /\ -U;
-U is a_neighborhood of 0.X by Th55;
then reconsider V as a_neighborhood of 0.X by CONNSP_2:2;
take V;
A2: -U is convex by A1,CONVEX1:1;
thus V is circled
proof
0.X in V by CONNSP_2:4;
then
A3: 0.X in -U by XBOOLE_0:def 4;
A4: 0.X in U by CONNSP_2:4;
let r be Real such that
A5: |.r.| <= 1;
let u be object;
assume u in r*V;
then consider v being Point of X such that
A6: u = r*v and
A7: v in V;
A8: v in -U by A7,XBOOLE_0:def 4;
A9: v in U by A7,XBOOLE_0:def 4;
per cases;
suppose
A10: r < 0;
then
A11: -r <= 1 by A5,ABSVALUE:def 1;
then (-r)*v + (1--r)*0.X in -U by A2,A8,A3,A10;
then (-r)*v + 0.X in -U;
then (-r)*v in -U;
then consider u9 being Point of X such that
A12: (-r)*v = (-1)*u9 and
A13: u9 in U;
(-r)*v + (1--r)*0.X in U by A1,A9,A4,A10,A11;
then (-r)*v + 0.X in U;
then (-r)*v in U;
then (-1)*(((-1)*r)*v) in (-1)*U;
then
A14: ((-1)*((-1)*r))*v in (-1)*U by RLVECT_1:def 7;
u9 = ((-1)*(-1))*u9 by RLVECT_1:def 8
.= (-1)*((-1)*u9) by RLVECT_1:def 7
.= ((-r)*(-1))*v by A12,RLVECT_1:def 7
.= r*v;
hence thesis by A6,A13,A14,XBOOLE_0:def 4;
end;
suppose
A15: r >= 0;
A16: r <= 1 by A5,ABSVALUE:def 1;
then r*v + (1-r)*0.X in -U by A2,A8,A3,A15;
then r*v + 0.X in -U;
then
A17: r*v in -U;
r*v + (1-r)*0.X in U by A1,A9,A4,A15,A16;
then r*v + 0.X in U;
then r*v in U;
hence thesis by A6,A17,XBOOLE_0:def 4;
end;
end;
thus V is convex by A1,A2;
thus thesis by XBOOLE_1:17;
end;
theorem
for X being LinearTopSpace ex P being local_base of X st P is
circled-membered
proof
let X be LinearTopSpace;
defpred P[Subset of X] means $1 is circled;
consider P being Subset-Family of X such that
A1: for V being Subset of X holds V in P iff P[V] from SUBSET_1:sch 3;
reconsider P as Subset-Family of X;
take P;
thus P is local_base of X
proof
let V be a_neighborhood of 0.X;
consider W being a_neighborhood of 0.X such that
A2: W is circled and
A3: W c= V by Th64;
take W;
thus W in P by A1,A2;
thus thesis by A3;
end;
let V be Subset of X;
assume V in P;
hence thesis by A1;
end;
theorem
for X being LinearTopSpace st X is locally-convex ex P being
local_base of X st P is convex-membered;
begin :: Addenda
:: segments in a real vector space, 2009.04.01- A.T.
reserve V for RealLinearSpace,
v,w for Point of V;
theorem Th68: :: TOPREAL1:6
v in LSeg(v,w)
proof
v = (1-0)*v by RLVECT_1:def 8
.= (1-0)*v + 0.V
.= (1-0)*v + 0*w by RLVECT_1:10;
hence thesis;
end;
theorem :: GOBOARD7:7
1/2*(v+w) in LSeg(v,w)
proof
1/2*(v+w) = (1-1/2)*v+1/2*w by RLVECT_1:def 5;
hence thesis;
end;
theorem :: TOPREAL1:7
LSeg(v,v) = {v}
proof
thus LSeg(v,v) c= {v}
proof
let a be object;
assume a in LSeg(v,v);
then consider r such that
A1: a = (1-r)*v + r*v and
0 <= r and
r <= 1;
a = ((1-r)+r)*v by A1,RLVECT_1:def 6
.= v by RLVECT_1:def 8;
hence thesis by TARSKI:def 1;
end;
v in LSeg(v,v) by Th68;
hence thesis by ZFMISC_1:31;
end;
theorem :: JORDAN2C:47
0.V in LSeg(v,w) implies ex r st v = r*w or w = r*v
proof
assume 0.V in LSeg(v,w);
then consider s being Real such that
A1: 0.V= (1-s)*v + s*w and
0 <= s and
s <= 1;
-s*w=(1-s)*v by A1,RLVECT_1:6;
then
A2: (-s)*w =(1-s)*v by RLVECT_1:79;
per cases;
suppose
A3: -s<>0;
take r = (-s)"*(1-s);
w = 1*w by RLVECT_1:def 8
.= (-s)"*(-s)*w by A3,XCMPLX_0:def 7
.= (-s)"*((-s)*w) by RLVECT_1:def 7
.= r*v by A2,RLVECT_1:def 7;
hence thesis;
end;
suppose
A4: -s=0;
take -s;
thus thesis by A2,A4,RLVECT_1:def 8;
end;
end;
:: from EUCLID_4 (generalized), A.T.
definition
let V,v,w;
func Line(v,w) -> Subset of V equals
the set of all (1-r)*v + r*w ;
coherence
proof
set A = the set of all (1-r)*v + r*w ;
A c= the carrier of V
proof
let x be object;
assume x in A;
then ex r st x = (1-r)*v + r*w;
hence x in the carrier of V;
end;
hence thesis;
end;
commutativity
proof let S be Subset of V;
let v,w;
set A = the set of all (1-r)*w + r*v ;
assume
A1: S = the set of all (1-r)*v + r*w ;
thus S c= A
proof let e be object;
assume e in S;
then consider r such that
A2: e = (1-r)*v + r*w by A1;
e = (1-(1-r))*w + (1-r)*v by A2;
hence e in A;
end;
let e be object;
assume e in A;
then consider r such that
A3: e = (1-r)*w + r*v;
e = (1-(1-r))*v + (1-r)*w by A3;
hence e in S by A1;
end;
end;
theorem Th72:
v in Line(v,w)
proof
v = (1-0)*v + 0.V by RLVECT_1:def 8
.= (1-0)*v + 0*w by RLVECT_1:10;
hence thesis;
end;
registration
let V,v,w;
cluster Line(v,w) -> non empty;
coherence by Th72;
end;
theorem
LSeg(v,w) c= Line(v,w)
proof let e be object;
assume e in LSeg(v,w);
then ex r st e =(1-r)*v + r*w & 0 <= r & r <= 1;
hence e in Line(v,w);
end;
reserve x1,x2,x3,x4,y1,y2 for Element of V;
theorem Th74:
y1 in Line(x1,x2) & y2 in Line(x1,x2) implies Line(y1,y2) c= Line(x1,x2)
proof
assume y1 in Line(x1,x2);
then consider t such that
A1: y1 = (1-t)*x1 + t*x2;
assume y2 in Line(x1,x2);
then consider s such that
A2: y2 = (1-s)*x1 + s*x2;
let z be object;
assume z in Line(y1,y2);
then consider u such that
A3: z = (1-u)*y1 + u*y2;
z = ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+u*((1-s)*x1+s*x2)
by A1,A2,A3,RLVECT_1:def 5
.= ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2))
by RLVECT_1:def 5
.= (((1-u)*(1-t))*x1+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2))
by RLVECT_1:def 7
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+(u*((1-s)*x1)+u*(s*x2))
by RLVECT_1:def 7
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+u*(s*x2))
by RLVECT_1:def 7
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+(u*s)*x2)
by RLVECT_1:def 7
.= ((1-u)*(1-t))*x1+(((1-u)*t)*x2+((u*(1-s))*x1+(u*s)*x2))
by RLVECT_1:def 3
.= ((1-u)*(1-t))*x1+((u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2))
by RLVECT_1:def 3
.= (((1-u)*(1-t))*x1+(u*(1-s))*x1)+(((1-u)*t)*x2+(u*s)*x2)
by RLVECT_1:def 3
.= ((1-u)*(1-t)+u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2) by RLVECT_1:def 6
.= (1-(1*t-u*t+u*s))*x1+(1*t-u*t+u*s)*x2 by RLVECT_1:def 6;
hence z in Line(x1,x2);
end;
theorem Th75:
y1 in Line(x1,x2) & y2 in Line(x1,x2) & y1 <> y2 implies
Line(y1,y2) = Line(x1,x2)
proof
assume
A1: y1 in Line(x1,x2);
then consider t such that
A2: y1 = (1-t)*x1 + t*x2;
assume
A3: y2 in Line(x1,x2);
then consider s such that
A4: y2 = (1-s)*x1 + s*x2;
assume y1<>y2;
then
A5: t-s<>0 by A2,A4;
thus Line(y1,y2) c= Line(x1,x2) by A1,A3,Th74;
(1-((t-1)/(t-s)))*y1 + ((t-1)/(t-s))*y2 = ((1*(t-s)-(t-1))/(t-s))*y1 + (
(t-1)/(t-s))*y2 by A5,XCMPLX_1:127
.= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + ((t-1)/(t-s))*(
(1-s)*x1 + s*x2) by A2,A4,RLVECT_1:def 5
.= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 5
.= ((((-s+1)/(t-s))*(1-t))*x1 + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by RLVECT_1:def 7
.= (((-s+1)*(1-t))/(t-s))*x1 + ((((-s+1)*t)/(t-s))*x2 + ((((t-1)*(1-s))/
(t-s))*x1 + (((t-1)*s)/(t-s))*x2)) by RLVECT_1:def 3
.= (((-s+1)*(1-t))/(t-s))*x1 + ((((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/
(t-s))*x2 + (((t-1)*s)/(t-s))*x2)) by RLVECT_1:def 3
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((t-1)*(1-s))/(t-s))*x1) + ((((-s+1)*t)
/(t-s))*x2 + (((t-1)*s)/(t-s))*x2) by RLVECT_1:def 3
.= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/(t-s))
*x2 + (((t-1)*s)/(t-s))*x2) by RLVECT_1:def 6
.= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + (((-s+1)*t)/(t-s) +
((t-1)*s)/(t-s))*x2 by RLVECT_1:def 6
.= 0.V + (((-s+1)*t + (t-1)*s)/(t-s))*x2 by RLVECT_1:10
.= (1*(t-s)/(t-s))*x2
.= 1*x2 by A5,XCMPLX_1:89
.= x2 by RLVECT_1:def 8;
then
A6: x2 in Line(y1,y2);
(1-(t/(t-s)))*y1 + (t/(t-s))*y2 = ((1*(t-s)-t)/(t-s))*y1 + (t/(t-s))*y2
by A5,XCMPLX_1:127
.= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + (t/(t-s))*((1-s)*x1
+ s*x2) by A2,A4,RLVECT_1:def 5
.= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 5
.= ((((-s)/(t-s))*(1-t))*x1 + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))*
x1 + (t/(t-s))*(s*x2)) by RLVECT_1:def 7
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))*
x1 + ((t/(t-s))*s)*x2) by RLVECT_1:def 7
.= (((-s)*(1-t))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + (((t*(1-s))/(t-s))*
x1 + ((t*s)/(t-s))*x2)) by RLVECT_1:def 3
.= (((-s)*(1-t))/(t-s))*x1 + (((t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))*
x2 + ((t*s)/(t-s))*x2)) by RLVECT_1:def 3
.= ((((-s)*(1-t))/(t-s))*x1 + ((t*(1-s))/(t-s))*x1) + ((((-s)*t)/(t-s))*
x2 + ((t*s)/(t-s))*x2) by RLVECT_1:def 3
.= (((-s)*(1-t))/(t-s) + (t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + ((
t*s)/(t-s))*x2) by RLVECT_1:def 6
.= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + (((-s)*t)/(t-s) + (t*s)/(t-s))*x2
by RLVECT_1:def 6
.= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + 0.V by RLVECT_1:10
.= ((1*(t-s))/(t-s))*x1
.= 1*x1 by A5,XCMPLX_1:89
.= x1 by RLVECT_1:def 8;
then x1 in Line(y1,y2);
hence thesis by A6,Th74;
end;
:: 12.11.28, A.T.
definition
let V;
let A be Subset of V;
attr A is being_line means
:Def15: ex x1,x2 st A=Line(x1,x2);
end;
registration let V;
cluster being_line for Subset of V;
existence
proof
set v = the Point of V;
take Line(v,v),v,v;
thus thesis;
end;
end;
registration let V be non trivial RealLinearSpace;
cluster non trivial being_line for Subset of V;
existence
proof
consider v,w being Point of V such that
A1: v <> w by STRUCT_0:def 10;
take L=Line(v,w);
thus L is non trivial
proof
take v,w;
thus v in L & w in L by Th72;
thus v <> w by A1;
end;
take v,w;
thus thesis;
end;
end;
definition let V;
mode line of V is being_line Subset of V;
end;
definition let V;
let x1,x2,x3 be Point of V;
pred x1,x2,x3 are_collinear means
ex L being line of V st x1 in L & x2 in L & x3 in L;
end;
definition let V;
let x1,x2,x3,x4 be Point of V;
pred x1,x2,x3,x4 are_collinear means
ex L being line of V st x1 in L & x2 in L & x3 in L & x4 in L;
end;
theorem
for x being object st x in LSeg(v,w)
ex r st 0<=r & r<=1 & x=(1-r)*v+r*w
proof let x be object;
assume x in LSeg(v,w);
then ex r st x = (1-r)*v + r*w & 0 <= r & r <= 1;
hence ex r st 0<=r & r<=1 & x=(1-r)*v+r*w;
end;
theorem Th77:
Line(v,v) = {v}
proof
for x being object holds x in Line(v,v) iff x = v
proof let x be object;
thus x in Line(v,v) implies x = v
proof assume
A1: x in Line(v,v);
then reconsider w=x as Point of V;
consider r such that
A2: w = (1-r)*v + r*v by A1;
w = ((1-r)+r)*v by A2,RLVECT_1:def 6;
hence x = v by RLVECT_1:def 8;
end;
assume x = v;
hence thesis by Th72;
end;
hence thesis by TARSKI:def 1;
end;
registration let V,v;
cluster {v} -> being_line for Subset of V;
coherence
proof let A be Subset of V such that
A1: A = {v};
take v,v;
thus thesis by A1,Th77;
end;
let w;
cluster Line(v,w) -> being_line;
coherence;
end;
theorem
for V being non trivial RealLinearSpace, L being non trivial line of V
ex p,q being Point of V st p <> q & L = Line(p,q)
proof let V be non trivial RealLinearSpace, L be non trivial line of V;
consider p,q being object such that
A1: p in L & q in L and
A2: p <> q by ZFMISC_1:def 10;
reconsider p,q as Point of V by A1;
take p,q;
thus p <> q by A2;
ex x1,x2 being Element of V st L = Line(x1,x2) by Def15;
hence L = Line(p,q) by A2,Th75,A1;
end;
theorem
for x1,x2,x3,x4 be Point of V st x1,x2,x3,x4 are_collinear
holds x1,x2,x3 are_collinear & x1,x2,x4 are_collinear;
theorem Th80:
for L being line of V, x1,x2 st x1 <> x2 & x1 in L & x2 in L
holds L = Line(x1,x2)
proof let L be line of V;
ex x3,x4 st L = Line(x3,x4) by Def15;
hence thesis by Th75;
end;
theorem
for x1,x2,x3,x4 be Point of V
st x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear
holds x1,x2,x3,x4 are_collinear
proof let x1,x2,x3,x4 be Point of V such that
A1: x1 <> x2;
given L1 being line of V such that
A2: x1 in L1 & x2 in L1 & x3 in L1;
given L2 being line of V such that
A3: x1 in L2 & x2 in L2 & x4 in L2;
L1 = Line(x1,x2) & L2 = Line(x1,x2) by A1,A2,A3,Th80;
hence ex L being line of V st x1 in L & x2 in L & x3 in L & x4 in L
by A2,A3;
end;