Copyright (c) 1999 Association of Mizar Users
environ
vocabulary ABSVALUE, ARYTM_1, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC,
EUCLID, COMPLEX1, SQUARE_1, RLVECT_1, RVSUM_1, TOPREAL1, RELAT_2,
BORSUK_1, TOPS_2, SUBSET_1, RCOMP_1, BOOLE, LATTICES, CONNSP_1, TARSKI,
CONNSP_3, SETFAM_1, GRAPH_1, ARYTM_3, TREAL_1, SEQ_1, FUNCT_4, TOPMETR,
COMPTS_1, FINSEQ_2, METRIC_1, PCOMPS_1, WEIERSTR, SEQ_4, SEQ_2, VECTSP_1,
FUNCOP_1, PARTFUN1, JORDAN3, TBSP_1, CONNSP_2, SPPOL_1, GOBOARD2,
SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1, MCART_1, CARD_1, MATRIX_1,
GOBOARD9, SEQM_3, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2, JORDAN2C,
FINSEQ_4, CARD_3, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, CARD_1,
PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, STRUCT_0, PCOMPS_1,
CONNSP_1, CONNSP_2, TBSP_1, CONNSP_3, TOPRNS_1, TOPMETR, RCOMP_1,
FINSEQ_1, FINSEQ_2, FINSEQ_4, SQUARE_1, ABSVALUE, BORSUK_2, WEIERSTR,
SEQ_4, JORDAN3, BINARITH, FUNCOP_1, FUNCT_3, VECTSP_1, TREAL_1, FUNCT_4,
RVSUM_1, EUCLID, SPPOL_1, PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1,
MATRIX_1, GOBOARD1, JORDAN1, GOBOARD2, GOBOARD5, GOBOARD9, JORDAN2B;
constructors WEIERSTR, REAL_1, TOPS_1, TOPS_2, COMPTS_1, REALSET1, CONNSP_1,
TBSP_1, CONNSP_3, FINSEQ_4, JORDAN1, RCOMP_1, GOBOARD2, GOBOARD9,
FINSEQOP, SQUARE_1, ABSVALUE, BORSUK_2, JORDAN3, TREAL_1, FUNCT_4,
SPPOL_1, SPRECT_1, TOPREAL2, SPRECT_2, PSCOMP_1, BINARITH, JORDAN2B,
PARTFUN1, TOPRNS_1, DOMAIN_1, MEMBERED, XCMPLX_0;
clusters SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, SPRECT_1,
TOPMETR, TOPREAL1, BORSUK_1, FUNCT_1, FUNCOP_1, FINSEQ_1, XREAL_0,
FINSET_1, SPRECT_3, EUCLID, GOBOARD1, GOBOARD2, ARYTM_3, MEMBERED,
ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, TBSP_1, JORDAN1;
theorems PRE_TOPC, CONNSP_1, EUCLID, TBSP_1, TOPREAL3, REAL_1, REAL_2, AXIOMS,
NAT_1, JGRAPH_1, JORDAN1, TOPS_2, FUNCT_2, BORSUK_1, TOPMETR, TOPREAL1,
FINSEQ_2, FINSEQOP, ABSVALUE, RVSUM_1, SQUARE_1, BORSUK_2, TOPREAL5,
WEIERSTR, SPPOL_1, TARSKI, SEQ_4, FUNCT_1, METRIC_1, SUBSET_1, FUNCOP_1,
ZFMISC_1, FINSEQ_1, FINSEQ_4, JORDAN3, BINARITH, RELAT_1, FUNCT_3,
VECTSP_1, BINOP_1, RCOMP_1, FUNCT_4, HEINE, TOPMETR2, TREAL_1, PCOMPS_1,
CONNSP_3, JORDAN6, COMPTS_1, TSEP_1, CONNSP_2, TOPS_1, JORDAN5D,
JORDAN2B, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD6, UNIFORM1, FINSEQ_6,
MATRIX_1, GOBOARD9, GOBRD12, SPRECT_1, CARD_1, CARD_2, ENUMSET1,
PSCOMP_1, SPRECT_2, SPRECT_3, SEQ_2, RELSET_1, SCMFSA_7, SETFAM_1,
XBOOLE_0, XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_1, NAT_1;
begin ::Definitions of Bounded Domain and Unbounded Domain
reserve m,n,i,i2,j for Nat,
r,r1,r2,s for Real,
x,y,z,y1,y2 for set;
theorem Th1: r<=0 implies abs(r)=-r
proof assume
A1:r<=0;
per cases by A1;
suppose r<0;
hence abs(r)=-r by ABSVALUE:def 1;
suppose r=0;
hence abs(r)=-r by ABSVALUE:7;
end;
theorem Th2:for n,m st n<=m & m<=n+2 holds m=n or m=n+1 or m=n+2
proof let n,m;assume A1: n<=m & m<=n+2;
per cases;
suppose m<=n+1;
hence m=n or m=n+1 or m=n+2 by A1,NAT_1:27;
suppose A2:m>n+1;
m<=n+(1+1) by A1;
then m<=n+1+1 by XCMPLX_1:1;
then m=n+1 or m=n+1+1 by A2,NAT_1:27;
then m=n+1 or m=n+(1+1) by XCMPLX_1:1;
hence thesis;
end;
theorem Th3:for n,m st n<=m & m<=n+3 holds m=n or m=n+1 or m=n+2 or m=n+3
proof let n,m;assume A1:n<=m & m<=n+3;
per cases;
suppose m<=n+2;
hence m=n or m=n+1 or m=n+2 or m=n+3 by A1,Th2;
suppose A2:m>n+2;
m<=n+(2+1) by A1;
then m<=n+2+1 by XCMPLX_1:1;
then m=n+2 or m=n+2+1 by A2,NAT_1:27;
then m=n+2 or m=n+(2+1) by XCMPLX_1:1;
hence thesis;
end;
theorem Th4:for n,m st n<=m & m<=n+4 holds
m=n or m=n+1 or m=n+2 or m=n+3 or m=n+4
proof let n,m;assume A1:n<=m & m<=n+4;
per cases;
suppose m<=n+3;
hence m=n or m=n+1 or m=n+2 or m=n+3 or m=n+4 by A1,Th3;
suppose A2:m>n+3;
m<=n+(3+1) by A1;
then m<=n+3+1 by XCMPLX_1:1;
then m=n+3 or m=n+3+1 by A2,NAT_1:27;
then m=n+3 or m=n+(3+1) by XCMPLX_1:1;
hence thesis;
end;
theorem Th5: for a,b being real number st a>=0 & b>=0 holds a+b>=0
proof let a,b be real number;assume a>=0 & b>=0;
then a+b>=0+0 by REAL_1:55;
hence a+b>=0;
end;
theorem Th6: for a,b being real number st a>0 & b>=0 holds a+b>0
proof let a,b be real number;assume a>0 & b>=0;
then a+b>0+0 by REAL_1:67;
hence a+b>0;
end;
theorem Th7: for f being FinSequence st rng f={x,y} & len f=2
holds f.1=x & f.2=y or f.1=y & f.2=x
proof let f be FinSequence;assume A1:rng f={x,y} & len f=2;
then 1 in Seg len f by FINSEQ_1:3;
then 1 in dom f by FINSEQ_1:def 3;
then A2:f.1 in rng f by FUNCT_1:def 5;
2 in Seg len f by A1,FINSEQ_1:3;
then 2 in dom f by FINSEQ_1:def 3;
then A3: f.2 in rng f by FUNCT_1:def 5;
A4:now assume A5:f.1=x & f.2=x;
y in rng f by A1,TARSKI:def 2;
then consider z such that A6:z in dom f & y=f.z by FUNCT_1:def 5;
A7:z in Seg len f by A6,FINSEQ_1:def 3;
reconsider nz=z as Nat by A6;
A8: 1<=nz & nz<=len f by A7,FINSEQ_1:3;
per cases by A1,A8,NAT_1:27;
suppose nz=1; hence f.1=x & f.2=y by A5,A6;
suppose nz=1+1; hence f.1=x & f.2=y by A5,A6;
end;
now assume A9:f.1=y & f.2=y;
x in rng f by A1,TARSKI:def 2;
then consider z such that A10:z in dom f & x=f.z by FUNCT_1:def 5;
A11:z in Seg len f by A10,FINSEQ_1:def 3;
reconsider nz=z as Nat by A10;
A12:1<=nz & nz<=len f by A11,FINSEQ_1:3;
per cases by A1,A12,NAT_1:27;
suppose nz=1; hence f.1=x & f.2=y by A9,A10;
suppose nz=1+1; hence f.1=x & f.2=y by A9,A10;
end;
hence thesis by A1,A2,A3,A4,TARSKI:def 2;
end;
theorem Th8: for f being increasing FinSequence of REAL
st rng f={r,s} & len f=2 & r<=s
holds f.1=r & f.2=s
proof let f be increasing FinSequence of REAL;
assume A1: rng f={r,s} & len f=2 & r<=s;
now assume A2:f.1=s & f.2=r;
1 in Seg len f by A1,FINSEQ_1:3;
then A3:1 in dom f by FINSEQ_1:def 3;
2 in Seg len f by A1,FINSEQ_1:3;
then 2 in dom f by FINSEQ_1:def 3;
hence f.1=r & f.2=s by A1,A2,A3,GOBOARD1:def 1;
end;
hence f.1=r & f.2=s by A1,Th7;
end;
reserve p,p1,p2,p3,q,q1,q2,q3,q4 for Point of TOP-REAL n;
theorem Th9: p1+p2-p3=p1-p3+p2
proof
thus p1+p2-p3=p1+p2+-p3 by EUCLID:45
.=p1+-p3+p2 by EUCLID:30 .=p1-p3+p2 by EUCLID:45;
end;
theorem abs(|.q.|)=|.q.|
proof
|.q.|>=0 by TOPRNS_1:26;
hence thesis by ABSVALUE:def 1;
end;
theorem Th11: abs(|.q1.|- |.q2.|)<=|.q1-q2.|
proof
per cases;
suppose |.q1.|>=|.q2.|;
then |.q1.|- |.q2.|>=0 by SQUARE_1:12;
then |.q1.|- |.q2.|=abs(|.q1.|- |.q2.|) by ABSVALUE:def 1;
hence thesis by TOPRNS_1:33;
suppose |.q1.|<|.q2.|;
then A1: |.q2.|- |.q1.|>0 by SQUARE_1:11;
|.q2.|- |.q1.|<= |.q2-q1.| by TOPRNS_1:33;
then abs(|.q2.|- |.q1.|)<= |.q2-q1.| by A1,ABSVALUE:def 1;
then abs(|.q2.|- |.q1.|)<= |.q1-q2.| by TOPRNS_1:28;
hence thesis by UNIFORM1:13;
end;
theorem Th12: |.|[r]|.|=abs(r)
proof
set p=|[r]|;
reconsider w=|[r]| as Element of REAL 1 by EUCLID:25;
A1: |.p.|=|.w.| by JGRAPH_1:def 5;
A2: |.w.| = sqrt Sum sqr w by EUCLID:def 5;
0 <= Sum sqr w by RVSUM_1:116;
then A3: (|.p.|)^2=Sum sqr w by A1,A2,SQUARE_1:def 4;
A4: |.p.|>=0 by TOPRNS_1:26;
w=<*r*> by JORDAN2B:def 2;
then sqr w=<*r^2*> by RVSUM_1:81;
then (|.p.|)^2 = r^2 by A3,RVSUM_1:103;
then (|.p.|) =sqrt (r^2) by A4,SQUARE_1:89
.=abs r by SQUARE_1:91;
hence thesis;
end;
theorem Th13: q-0.REAL n=q & (0.REAL n)-q = -q
proof
thus q-0.REAL n=q-(q-q) by EUCLID:46 .=q-q+q by EUCLID:51 .=q by EUCLID:52;
thus (0.REAL n)-q =-q--q -q by EUCLID:46.= -q+--q-q by EUCLID:45
.=-q+q-q by EUCLID:39
.=-q by EUCLID:52;
end;
theorem Th14:
for P being Subset of TOP-REAL n st P is convex
holds P is connected
proof let P be Subset of TOP-REAL n; assume that
A1:for w3,w4 being Point of TOP-REAL n
st w3 in P & w4 in P holds LSeg(w3,w4) c= P;
for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P & w1<>w2
ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w2=h.1
proof
let w1,w2 be Point of TOP-REAL n;
assume A2:w1 in P & w2 in P & w1<>w2;
then A3: LSeg(w1,w2) c= P by A1;
LSeg(w1,w2) is_an_arc_of w1,w2 by A2,TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w1,w2) such that
A4: f is_homeomorphism & f.0 = w1 & f.1 = w2 by TOPREAL1:def 2;
A5:f is continuous by A4,TOPS_2:def 5;
A6: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A4,TOPS_2:def 5;
then A7: rng f c= P by A3,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
by A6,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w1,w2))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A8:(TOP-REAL n)|LSeg(w1,w2)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f=[.0 qua Real,1 qua Real.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of [.0 qua Real,1 qua Real.],P
by A7,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt=g as map of I[01],(TOP-REAL n)|P
by BORSUK_1:83;
gt is continuous by A5,A8,TOPMETR:7;
hence thesis by A4;
end;
hence thesis by JORDAN1:5;
end;
theorem Th15:for G being non empty TopSpace,
P being Subset of G,A being Subset of G,
Q being Subset of G|A st P=Q & P is connected
holds Q is connected
proof let G be non empty TopSpace,P be Subset of G,
A be Subset of G,
Q be Subset of G|A;
assume that
A1: P=Q and
A2: P is connected;
A3:G|P is connected by A2,CONNSP_1:def 3;
Q c= the carrier of G|A;
then Q c= A by JORDAN1:1;
then G|P=(G|A)|Q by A1,JORDAN6:47;
hence Q is connected by A3,CONNSP_1:def 3;
end;
definition let n;let A be Subset of TOP-REAL n;
canceled;
attr A is Bounded means
:Def2:ex C being Subset of Euclid n st C=A & C is bounded;
correctness;
end;
theorem Th16:for A,B being Subset of TOP-REAL n st B is Bounded &
A c= B holds A is Bounded
proof let A,B be Subset of TOP-REAL n;
assume A1:B is Bounded & A c= B;
then consider C being Subset of Euclid n
such that A2:C=B & C is bounded by Def2;
A is Subset of Euclid n by A1,A2,XBOOLE_1:1;
then reconsider C2=A as Subset of Euclid n;
C2 is bounded by A1,A2,TBSP_1:21;
hence A is Bounded by Def2;
end;
definition let n;let A be Subset of TOP-REAL n;
let B be Subset of TOP-REAL n;
pred B is_inside_component_of A means
:Def3: B is_a_component_of A` & B is Bounded;
end;
definition let M be non empty MetrStruct;
cluster bounded Subset of M;
existence proof take {}M, 1; thus thesis; end;
end;
theorem Th17: for A being Subset of TOP-REAL n,
B being Subset of TOP-REAL n holds
B is_inside_component_of A iff
ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n
proof let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
A1: B is_a_component_of A` iff
ex C being Subset of (TOP-REAL n)|(A`) st
C=B & C is_a_component_of (TOP-REAL n)|(A`) by CONNSP_1:def 6;
A2:B is_inside_component_of A iff
B is_a_component_of A` & B is Bounded by Def3;
thus B is_inside_component_of A implies
(ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n)
proof assume A3: B is_inside_component_of A;
then consider C being Subset of ((TOP-REAL n)|(A`)) such that
A4:C=B & C is_a_component_of ((TOP-REAL n)|(A`)) by A1,Def3;
consider D1 being Subset of Euclid n such that
A5: D1=B & D1 is bounded by A2,A3,Def2;
thus thesis by A4,A5;
end;
given C being Subset of ((TOP-REAL n)|(A`)) such that
A6:C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n;
A7:B is Bounded by A6,Def2;
B is_a_component_of A` by A6,CONNSP_1:def 6;
hence thesis by A7,Def3;
end;
definition let n;let A be Subset of TOP-REAL n;
let B be Subset of TOP-REAL n;
pred B is_outside_component_of A means
:Def4: B is_a_component_of A` & B is not Bounded;
end;
theorem Th18: for A being Subset of TOP-REAL n,
B being Subset of TOP-REAL n holds
B is_outside_component_of A iff
ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is not bounded Subset of Euclid n
proof let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
A1: B is_a_component_of A` iff
ex C being Subset of (TOP-REAL n)|(A`) st
C=B & C is_a_component_of (TOP-REAL n)|(A`) by CONNSP_1:def 6;
A2: B is_outside_component_of A iff
B is_a_component_of A` & not B is Bounded by Def4;
thus B is_outside_component_of A implies
(ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is not bounded Subset of Euclid n)
proof assume A3: B is_outside_component_of A;
then consider C being Subset of (TOP-REAL n)|(A`) such that
A4:C=B & C is_a_component_of (TOP-REAL n)|(A`) by A1,Def4;
B is Subset of Euclid n by TOPREAL3:13;
then reconsider D2=B as Subset of Euclid n;
now assume for D being Subset of Euclid n st D=C holds D is bounded;
then D2 is bounded by A4;
hence contradiction by A2,A3,Def2;
end;
hence thesis by A4;
end;
given C being Subset of ((TOP-REAL n)|(A`)) such that
A5:C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is not bounded Subset of Euclid n;
for D4 being Subset of Euclid n
st D4=B holds not D4 is bounded by A5;
then A6:not B is Bounded by Def2;
B is_a_component_of A` by A5,CONNSP_1:def 6;
hence thesis by A6,Def4;
end;
theorem for A,B being Subset of TOP-REAL n st
B is_inside_component_of A holds B c= A`
proof let A,B be Subset of TOP-REAL n;
assume B is_inside_component_of A;
then B is_a_component_of A` by Def3;
hence B c= A` by SPRECT_1:7;
end;
theorem for A,B being Subset of TOP-REAL n st
B is_outside_component_of A holds B c= A`
proof let A,B be Subset of TOP-REAL n;
assume B is_outside_component_of A;
then B is_a_component_of A` by Def4;
hence B c= A` by SPRECT_1:7;
end;
definition let n;let A be Subset of TOP-REAL n;
func BDD A -> Subset of TOP-REAL n equals
:Def5: union{B where B is Subset of TOP-REAL n: B is_inside_component_of A};
correctness
proof
union{B where B is Subset of TOP-REAL n:
B is_inside_component_of A} c= the carrier of TOP-REAL n
proof let x;assume x in union{B where B is Subset of TOP-REAL n:
B is_inside_component_of A};
then consider y being set such that
A1: x in y & y in
{B where B is Subset of TOP-REAL n:
B is_inside_component_of A} by TARSKI:def 4;
consider B being Subset of TOP-REAL n such that
A2:y=B & B is_inside_component_of A by A1;
thus x in the carrier of TOP-REAL n by A1,A2;
end;
hence thesis;
end;
end;
definition let n;let A be Subset of TOP-REAL n;
func UBD A -> Subset of TOP-REAL n equals
:Def6: union{B where B is Subset of TOP-REAL n: B is_outside_component_of A};
correctness
proof
union{B where B is Subset of TOP-REAL n:
B is_outside_component_of A} c= the carrier of TOP-REAL n
proof let x;assume x in
union{B where B is Subset of TOP-REAL n:
B is_outside_component_of A};
then consider y being set such that
A1: x in y & y in
{B where B is Subset of TOP-REAL n:
B is_outside_component_of A} by TARSKI:def 4;
consider B being Subset of TOP-REAL n such that
A2:y=B & B is_outside_component_of A by A1;
thus x in the carrier of TOP-REAL n by A1,A2;
end;
hence thesis;
end;
end;
theorem Th21: [#](TOP-REAL n) is convex
proof
let w1,w2 be Point of TOP-REAL n;
LSeg(w1,w2) c= the carrier of TOP-REAL n;
hence thesis by PRE_TOPC:12;
end;
theorem Th22: [#](TOP-REAL n) is connected
proof [#](TOP-REAL n) is convex by Th21;
hence [#](TOP-REAL n) is connected by Th14;
end;
definition let n;
cluster [#](TOP-REAL n) -> connected;
coherence by Th22;
end;
theorem Th23: [#](TOP-REAL n) is_a_component_of TOP-REAL n
proof
set A=[#](TOP-REAL n);
for B being Subset of TOP-REAL n st
B is connected holds A c= B implies A = B
proof let B be Subset of TOP-REAL n;
assume B is connected;
thus A c= B implies A = B
proof assume A1:A c= B;
B c= the carrier of TOP-REAL n;
then B c= [#] (TOP-REAL n) by PRE_TOPC:12;
hence A=B by A1,XBOOLE_0:def 10;
end;
end;
hence thesis by CONNSP_1:def 5;
end;
theorem Th24:for A being Subset of TOP-REAL n holds
BDD A is a_union_of_components of (TOP-REAL n)|A`
proof let A be Subset of TOP-REAL n;
{B where B is Subset of TOP-REAL n:
B is_inside_component_of A} c= bool (the carrier of ((TOP-REAL n)|A`))
proof let x; assume x in {B where B is Subset of TOP-REAL n:
B is_inside_component_of A};
then consider B being Subset of TOP-REAL n such that
A1: x=B & B is_inside_component_of A;
consider C being Subset of ((TOP-REAL n)|(A`)) such that
A2: C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n by A1,Th17;
thus x in bool (the carrier of ((TOP-REAL n)|A`)) by A1,A2;
end;
then reconsider F0={B where B is Subset of TOP-REAL n:
B is_inside_component_of A} as Subset-Family of
the carrier of ((TOP-REAL n)|A`) by SETFAM_1:def 7;
reconsider F0 as Subset-Family of (TOP-REAL n)|A`;
A3: BDD A=union F0 by Def5;
for B0 being Subset of ((TOP-REAL n)|A`) st B0 in F0
holds B0 is_a_component_of ((TOP-REAL n)|A`)
proof let B0 be Subset of ((TOP-REAL n)|A`);
assume B0 in F0;
then consider B being Subset of TOP-REAL n such that
A4:B=B0 & B is_inside_component_of A;
consider
C being Subset of ((TOP-REAL n)|(A`)) such that
A5: C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n by A4,Th17;
thus B0 is_a_component_of ((TOP-REAL n)|A`) by A4,A5;
end;
hence thesis by A3,CONNSP_3:def 2;
end;
theorem Th25:for A being Subset of TOP-REAL n holds
UBD A is a_union_of_components of (TOP-REAL n)|A`
proof let A be Subset of TOP-REAL n;
{B where B is Subset of TOP-REAL n:
B is_outside_component_of A} c= bool (the carrier of ((TOP-REAL n)|A`))
proof let x;assume x in {B where B is Subset of TOP-REAL n:
B is_outside_component_of A};
then consider B being Subset of TOP-REAL n such that
A1: x=B & B is_outside_component_of A;
ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is not bounded Subset of Euclid n by A1,Th18;
hence thesis by A1;
end;
then reconsider F0={B where B is Subset of TOP-REAL n:
B is_outside_component_of A} as Subset-Family of
the carrier of ((TOP-REAL n)|A`) by SETFAM_1:def 7;
reconsider F0 as Subset-Family of ((TOP-REAL n)|A`);
A2: UBD A=union F0 by Def6;
for B0 being Subset of ((TOP-REAL n)|A`) st B0 in F0
holds B0 is_a_component_of ((TOP-REAL n)|A`)
proof let B0 be Subset of ((TOP-REAL n)|A`);
assume B0 in F0;
then consider B being Subset of TOP-REAL n such that
A3:B=B0 & B is_outside_component_of A;
ex C being Subset of ((TOP-REAL n)|(A`)) st
C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is not bounded Subset of Euclid n by A3,Th18;
hence thesis by A3;
end;
hence thesis by A2,CONNSP_3:def 2;
end;
theorem Th26: for A being Subset of TOP-REAL n,
B being Subset of TOP-REAL n st B is_inside_component_of A
holds B c= BDD A
proof let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
assume A1:B is_inside_component_of A;
let x;assume A2:x in B;
B in {B2 where B2 is Subset of TOP-REAL n:
B2 is_inside_component_of A} by A1;
then x in union{B2 where B2 is Subset of TOP-REAL n:
B2 is_inside_component_of A} by A2,TARSKI:def 4;
hence x in BDD A by Def5;
end;
theorem Th27: for A being Subset of TOP-REAL n,
B being Subset of TOP-REAL n st B is_outside_component_of A
holds B c= UBD A
proof let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
assume A1:B is_outside_component_of A;
let x;assume A2:x in B;
B in {B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of A} by A1;
then x in union{B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of A} by A2,TARSKI:def 4;
hence x in UBD A by Def6;
end;
theorem Th28:for A being Subset of TOP-REAL n holds
BDD A misses UBD A
proof let A be Subset of TOP-REAL n;
assume A1:(BDD A) /\ (UBD A) <>{};
consider x being Element of (BDD A) /\ (UBD A);
A2:x in BDD A & x in UBD A by A1,XBOOLE_0:def 3;
then x in union{B where B is Subset of TOP-REAL n:
B is_inside_component_of A} by Def5;
then consider y being set such that
A3:x in y & y in {B where B is Subset of TOP-REAL n:
B is_inside_component_of A} by TARSKI:def 4;
consider B being Subset of TOP-REAL n such that
A4:y=B & B is_inside_component_of A by A3;
consider C being Subset of ((TOP-REAL n)|(A`)) such that
A5: C=B & C is_a_component_of ((TOP-REAL n)|(A`)) &
C is bounded Subset of Euclid n by A4,Th17;
x in union{B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of A} by A2,Def6;
then consider y2 being set such that
A6:x in y2 & y2 in {B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of A} by TARSKI:def 4;
consider B2 being Subset of TOP-REAL n such that
A7:y2=B2 & B2 is_outside_component_of A by A6;
consider C2 being Subset of ((TOP-REAL n)|(A`)) such that
A8: C2=B2 & C2 is_a_component_of ((TOP-REAL n)|(A`)) &
C2 is not bounded Subset of Euclid n by A7,Th18;
C /\ C2<>{}((TOP-REAL n)|(A`)) by A3,A4,A5,A6,A7,A8,XBOOLE_0:def 3;
then C meets C2 by XBOOLE_0:def 7;
hence contradiction by A5,A8,CONNSP_1:37;
end;
theorem Th29:for A being Subset of TOP-REAL n holds
BDD A c= A`
proof let A be Subset of TOP-REAL n;
reconsider D=BDD A as Subset of (TOP-REAL n)|A` by Th24;
D c= the carrier of ((TOP-REAL n)|A`);
hence thesis by JORDAN1:1;
end;
theorem Th30:for A being Subset of TOP-REAL n holds
UBD A c= A`
proof let A be Subset of TOP-REAL n;
reconsider D=UBD A as Subset of (TOP-REAL n)|A` by Th25;
D c= the carrier of ((TOP-REAL n)|A`);
hence thesis by JORDAN1:1;
end;
theorem Th31:for A being Subset of TOP-REAL n holds
(BDD A) \/ (UBD A) = A`
proof let A be Subset of TOP-REAL n;
A1:(BDD A) c= A` by Th29;
(UBD A) c= A` by Th30;
then A2:(BDD A) \/ (UBD A) c= A` by A1,XBOOLE_1:8;
A` c= (BDD A) \/ (UBD A)
proof let z be set;assume A3:z in A`;
then reconsider p=z as Element of A`;
reconsider q=p as Point of (TOP-REAL n)|A` by JORDAN1:1;
reconsider B=A` as non empty Subset of TOP-REAL n by A3;
A4:(TOP-REAL n)|B is non empty;
then A5:skl q is_a_component_of (TOP-REAL n)|A` by CONNSP_1:43;
skl q is Subset of [#]((TOP-REAL n)|A`) by PRE_TOPC:12;
then skl q is Subset of A` by PRE_TOPC:def 10;
then skl q is Subset of TOP-REAL n by XBOOLE_1:1;
then reconsider G=skl q as Subset of TOP-REAL n;
A6:q in G by A4,CONNSP_1:40;
A7:G is_a_component_of A` by A5,CONNSP_1:def 6;
per cases;
suppose G is Bounded;
then G is_inside_component_of A by A7,Def3;
then G c= BDD A by Th26;
hence z in (BDD A) \/ (UBD A) by A6,XBOOLE_0:def 2;
suppose not G is Bounded;
then G is_outside_component_of A by A7,Def4;
then G c= UBD A by Th27;
hence z in (BDD A) \/ (UBD A) by A6,XBOOLE_0:def 2;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
reserve u for Point of Euclid n;
theorem Th32:
for G being non empty TopSpace,
w1,w2,w3 being Point of G,
h1,h2 being map of I[01],G
st h1 is continuous & w1=h1.0 & w2=h1.1 &
h2 is continuous & w2=h2.0 & w3=h2.1 holds
ex h3 being map of I[01],G st h3 is continuous & w1=h3.0 & w3=h3.1 &
rng h3 c= (rng h1) \/ (rng h2)
proof
let G be non empty TopSpace,
w1,w2,w3 be Point of G,
h1,h2 be map of I[01],G;
assume A1:h1 is continuous & w1=h1.0 & w2=h1.1 &
h2 is continuous & w2=h2.0 & w3=h2.1;
then reconsider g1=h1 as Path of w1,w2 by BORSUK_2:def 1;
reconsider g2=h2 as Path of w2,w3 by A1,BORSUK_2:def 1;
set P1=g1,P2=g2,p1=w1,p3=w3;
ex P0 being Path of p1,p3 st P0 is continuous & P0.0=p1 & P0.1=p3 &
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies P0.t = P1.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies P0.t = P2.(2*t'-1) )
proof ::This proof is almost a copy of BORSUK_2:def 4(proof of Existence)
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set E1 = P1 * e1;
set E2 = P2 * e2;
set f = E1 +* E2;
A2:dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:25;
A3:dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1 qua Real.] by TOPMETR:25;
A4: dom P1 = the carrier of I[01] & dom P2 = the carrier of I[01]
by FUNCT_2:def 1;
then A5:rng e1 c= dom P1 by TOPMETR:27;
rng e2 c= the carrier of Closed-Interval-TSpace(0,1);
then A6: dom E2 = dom e2 by A4,RELAT_1:46,TOPMETR:27;
A7: dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1 qua Real.] by A2,A3,A5,A6,RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83,TREAL_1:2;
A8: for t' being Real st 0 <= t' & t' <= 1/2 holds E1.t' = P1.(2*t')
proof
let t' be Real such that
A9: 0 <= t' & t' <= 1/2;
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then dom e1 = [.0, 1/2.] by TOPMETR:25
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
then A10: t' in dom e1 by A9;
then reconsider s = t' as Point of Closed-Interval-TSpace (0, 1/2)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e1.s = ((r2 - r1)/(1/2 - 0))*t' + ((1/2)*r1 - 0 * r2)/(1/2 - 0)
by TREAL_1:14
.= 2*t' by BORSUK_1:def 17,def 18,TREAL_1:8;
hence thesis by A10,FUNCT_1:23;
end;
not 0 in { r : 1/2 <= r & r <= 1 }
proof
assume 0 in { r : 1/2 <= r & r <= 1 };
then ex rr being Real st rr = 0 & 1/2 <= rr & rr <= 1;
hence thesis;
end;
then not 0 in dom E2 by A3,A6,RCOMP_1:def 1;
then A11:f.0 = E1.0 by FUNCT_4:12
.= P1.(2*0) by A8
.= p1 by A1;
rng E1 c= rng P1 & rng E2 c= rng P2 by RELAT_1:45;
then A12:rng E1 c= the carrier of G &
rng E2 c= the carrier of G by XBOOLE_1:1;
A13: rng f c= rng E1 \/ rng E2 by FUNCT_4:18;
rng E1 \/ rng E2 c= (the carrier of G) \/ the carrier of G
by A12,XBOOLE_1:13;
then rng f c= the carrier of G by A13,XBOOLE_1:1;
then f is Function of the carrier of I[01], the carrier of G
by A7,FUNCT_2:def 1,RELSET_1:11;
then reconsider f as map of I[01], G ;
reconsider T1 = Closed-Interval-TSpace (0, 1/2),
T2 = Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01]
by TOPMETR:27,TREAL_1:6;
A14:e1 is continuous by TREAL_1:15;
A15:e2 is continuous by TREAL_1:15;
E1 is Function of the carrier of Closed-Interval-TSpace (0, 1/2),
the carrier of G by FUNCT_2:19,TOPMETR:27;
then reconsider ff = E1 as map of T1, G ;
A16:E2 is Function of the carrier of Closed-Interval-TSpace (1/2, 1),
the carrier of G by FUNCT_2:19,TOPMETR:27;
then reconsider gg = E2 as map of T2, G ;
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:83,RCOMP_1:def 1;
A17:ff is continuous & gg is continuous by A1,A14,A15,TOPMETR:27,TOPS_2:58;
A18:[#] T1 = the carrier of T1 by PRE_TOPC:12
.= [.0,1/2.] by TOPMETR:25;
A19:[#] T2 = the carrier of T2 by PRE_TOPC:12
.= [.1/2,1 qua Real.] by TOPMETR:25;
then A20: ([#] T1) \/ ([#] T2) = [.0,1 qua Real.] by A18,TREAL_1:2
.= [#] I[01] by BORSUK_1:83,PRE_TOPC:12;
A21: for t' being Real st 1/2 <= t' & t' <= 1 holds E2.t' = P2.(2*t'-1)
proof
let t' be Real such that
A22: 1/2 <= t' & t' <= 1;
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then dom e2 = [.1/2,1 qua Real.] by TOPMETR:25
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
then A23: t' in dom e2 by A22;
then reconsider s = t' as Point of Closed-Interval-TSpace (1/2,1)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e2.s = ((r2 - r1)/(1 - 1/2))*t' + (1 * r1 - (1/2)*r2)/(1 - 1/2)
by TREAL_1:14
.= 2*t' + (- 1) by BORSUK_1:def 17,def 18,TREAL_1:8
.= 2*t' - 1 by XCMPLX_0:def 8;
hence thesis by A23,FUNCT_1:23;
end;
A24:ff.(1/2) = P2.(2*(1/2)-1) by A1,A8
.= gg.pol by A21;
A25:([#] T1) /\ ([#] T2) = {pol} by A18,A19,TOPMETR2:1;
R^1 is_T2 by PCOMPS_1:38,TOPMETR:def 7;
then T1 is compact & T2 is compact & I[01] is_T2 & ff.pol = gg.pol
by A24,HEINE:11,TOPMETR:3;
then consider h being map of I[01], G such that
A26: h = ff+*gg & h is continuous by A17,A20,A25,TOPMETR2:4;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A3,A6,RCOMP_1:def 1;
then A27: f.1 = E2.1 by FUNCT_4:14
.= P2.(2*1-1) by A21
.= p3 by A1;
then reconsider f as Path of p1, p3 by A11,A26,BORSUK_2:def 1;
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies f.t = P1.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies f.t = P2.(2*t'-1) )
proof
let t be Point of I[01], t' be Real;
assume A28: t = t';
thus 0 <= t' & t' <= 1/2 implies f.t = P1.(2*t')
proof
assume A29: 0 <= t' & t' <= 1/2;
then t' in { r : 0 <= r & r <= 1/2 };
then A30: t' in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose A31: t' <> 1/2;
not t' in dom E2
proof
assume t' in dom E2;
then t' in [.0,1/2.] /\ [.1/2,1 qua Real.] by A3,A6,A30,XBOOLE_0:def 3;
then t' in {1/2} by TOPMETR2:1;
hence thesis by A31,TARSKI:def 1;
end;
then f.t = E1.t by A28,FUNCT_4:12
.= P1.(2*t') by A8,A28,A29;
hence thesis;
suppose A32: t' = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1 qua Real.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1)
by TOPMETR:25;
then t in dom E2 by A16,A28,A32,FUNCT_2:def 1;
then f.t = E2.(1/2) by A28,A32,FUNCT_4:14
.= P1.(2*t') by A8,A24,A32;
hence thesis;
end;
thus 1/2 <= t' & t' <= 1 implies f.t = P2.(2*t'-1)
proof
assume A33: 1/2 <= t' & t' <= 1;
then t' in { r : 1/2 <= r & r <= 1 };
then t' in [.1/2,1 qua Real.] by RCOMP_1:def 1;
then f.t = E2.t by A3,A6,A28,FUNCT_4:14
.= P2.(2*t'-1) by A21,A28,A33;
hence thesis;
end;
end;
hence thesis by A11,A26,A27;
end;
then consider P0 being Path of p1,p3 such that
A34: P0 is continuous & P0.0=p1 & P0.1=p3 &
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies P0.t = P1.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies P0.t = P2.(2*t'-1) );
rng P0 c= (rng P1) \/ (rng P2)
proof let x be set;assume x in rng P0;
then consider z being set such that
A35:z in dom P0 & x=P0.z by FUNCT_1:def 5;
A36: dom P0=the carrier of I[01] by FUNCT_2:def 1;
then reconsider r=z as Real by A35,BORSUK_1:83;
A37:0<=r & r<=1 by A35,A36,BORSUK_1:83,TOPREAL5:1;
A38:dom g1=the carrier of I[01] by FUNCT_2:def 1;
A39:dom g2=the carrier of I[01] by FUNCT_2:def 1;
per cases;
suppose A40:r<=1/2;
then A41:P0.z=P1.(2*r) by A34,A35,A36,A37;
A42:0<=2*r by A37,REAL_2:121;
2*r <= 2*(1/2) by A40,AXIOMS:25;
then 2*r in the carrier of I[01] by A42,BORSUK_1:83,TOPREAL5:1;
then P0.z in rng g1 by A38,A41,FUNCT_1:def 5;
hence x in (rng P1) \/ (rng P2) by A35,XBOOLE_0:def 2;
suppose A43:r>1/2;
then A44:P0.z=P2.(2*r-1) by A34,A35,A36,A37;
2*(1/2)=1;
then 0+1<=2*r by A43,AXIOMS:25;
then A45:0<=2*r-1 by REAL_1:84;
2*r<=2*1 by A37,AXIOMS:25;
then 2*r<=1+1;
then 2*r-1<=1 by REAL_1:86;
then 2*r-1 in the carrier of I[01] by A45,BORSUK_1:83,TOPREAL5:1;
then P0.z in rng g2 by A39,A44,FUNCT_1:def 5;
hence x in (rng P1) \/ (rng P2) by A35,XBOOLE_0:def 2;
end;
hence thesis by A34;
end;
theorem Th33: for P being Subset of TOP-REAL n
st P=REAL n holds P is connected
proof let P be Subset of TOP-REAL n;
assume A1:P=(REAL n);
for p1,p2 being Point of TOP-REAL n
st p1 in P & p2 in P holds LSeg(p1,p2) c= P
proof let p1,p2 be Point of TOP-REAL n;
assume p1 in P & p2 in P;
the carrier of TOP-REAL n=REAL n by EUCLID:25;
hence LSeg(p1,p2) c= P by A1;
end;
then P is convex by JORDAN1:def 1;
hence P is connected by Th14;
end;
definition let n;
func 1*n -> FinSequence of REAL equals :Def7:
n |-> (1 qua Real);
coherence by FINSEQ_2:77;
end;
definition let n;
redefine func 1*n -> Element of REAL n;
coherence
proof
A1:n-tuples_on REAL = REAL n & 1*n = n |-> (1 qua Real)
by Def7,EUCLID:def 1;
reconsider f=1*n as FinSequence;
len f = len (n|->(1 qua Real)) by Def7 .=n by FINSEQ_2:69;
hence thesis by A1,FINSEQ_2:110;
end;
end;
definition let n;
func 1.REAL n -> Point of TOP-REAL n equals
:Def8: 1*n;
coherence by EUCLID:25;
end;
theorem abs 1*n = n |-> (1 qua Real)
proof
reconsider f= (n |-> (1 qua Real)) as FinSequence of REAL by FINSEQ_2:77;
thus abs 1*n = abs f by Def7
.= absreal*(n |-> (1 qua Real)) by EUCLID:def 3
.= n |-> absreal.(1 qua Real) by FINSEQOP:17
.= n |-> abs(1 qua Real) by EUCLID:def 2
.= n |-> 1 by ABSVALUE:def 1;
end;
theorem Th35: |.1*n.| = sqrt n
proof
reconsider f= (n |-> (1 qua Real)) as FinSequence of REAL by FINSEQ_2:77;
thus |.1*n .| = sqrt Sum sqr 1*n by EUCLID:def 5
.= sqrt Sum sqr f by Def7
.= sqrt Sum f by RVSUM_1:82,SQUARE_1:59
.= sqrt (n*1) by RVSUM_1:110
.= sqrt n;
end;
theorem Th36: 1.REAL 1 = <* 1 qua Real *>
proof
reconsider f= (1 |-> (1 qua Real)) as FinSequence of REAL by FINSEQ_2:77;
thus 1.REAL 1=1*1 by Def8 .=f by Def7 .=<* 1 qua Real *> by FINSEQ_2:73;
end;
theorem Th37: |. (1.REAL n) .| = sqrt n
proof A1:1.REAL n=1*n by Def8;
|. 1*n .|=sqrt n by Th35;
hence thesis by A1,JGRAPH_1:def 5;
end;
theorem Th38:
1<=n implies 1<=|. (1.REAL n) .|
proof assume A1: 1<=n;
|.1.REAL n.|=sqrt n by Th37;
hence thesis by A1,SQUARE_1:83,94;
end;
theorem Th39: for W being Subset of Euclid n
st n>=1 & W=REAL n holds W is not bounded
proof let W be Subset of Euclid n;
assume A1:n>=1 & W=(REAL n);
assume W is bounded;
then consider r being Real such that
A2:0<r & for x,y being Point of Euclid n st
x in W & y in W holds dist(x,y)<=r by TBSP_1:def 9;
reconsider x0=(r+1)*(1.REAL n) as Point of Euclid n by TOPREAL3:13;
(r+1)*(1.REAL n) in the carrier of TOP-REAL n;
then A3:x0 in W by A1,EUCLID:25;
reconsider y0=0.REAL n as Point of Euclid n by TOPREAL3:13;
0.REAL n in the carrier of TOP-REAL n;
then y0 in W by A1,EUCLID:25;
then dist(x0,y0)<=r by A2,A3;
then |.(r+1)*(1.REAL n) -0.REAL n.|<=r by JGRAPH_1:45;
then |.(r+1)*(1.REAL n).|<=r by Th13;
then abs(r+1)*|.(1.REAL n).|<=r by TOPRNS_1:8;
then A4:abs(r+1)*(sqrt n)<=r by Th37;
r+1>r by REAL_1:69;
then A5:r+1>0 by A2,AXIOMS:22;
then A6:(r+1)*(sqrt n)<=r by A4,ABSVALUE:def 1;
(sqrt 1)<=(sqrt n) by A1,SQUARE_1:94;
then (r+1)*1<=(r+1)*(sqrt n) by A5,AXIOMS:25,SQUARE_1:83;
then (r+1)*1<=r by A6,AXIOMS:22;
then (r+1)-r<=r-r by REAL_1:49;
then 1<=r-r by XCMPLX_1:26;
then 1<=0 by XCMPLX_1:14;
hence contradiction;
end;
theorem Th40: for A being Subset of TOP-REAL n holds
A is Bounded iff ex r being Real st for q being Point of TOP-REAL n st
q in A holds |.q.|<r
proof let A be Subset of TOP-REAL n;
hereby assume A is Bounded;
then consider C being Subset of Euclid n such that
A1:C=A & C is bounded by Def2;
per cases;
suppose A2:C<>{};
consider x0 being Element of C;
x0 in C by A2;
then reconsider x0 as Point of Euclid n;
consider r being Real such that
A3: 0<r & for x,y being Point of (Euclid n) st x in C & y in C holds
dist(x,y) <= r by A1,TBSP_1:def 9;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
set R0=r+dist(o,x0)+1;
for q being Point of TOP-REAL n st q in A holds |.q.|<R0
proof let q1 be Point of TOP-REAL n;
assume A4:q1 in A;
reconsider z=q1 as Point of Euclid n by TOPREAL3:13;
|.q1-(0.REAL n).|=dist(o,z) by JGRAPH_1:45;
then A5: |.q1.|=dist(o,z) by Th13;
A6:dist(x0,z)<=r by A1,A3,A4;
A7:dist(o,z)<=dist(o,x0)+dist(x0,z) by METRIC_1:4;
dist(o,x0)+dist(x0,z)<=dist(o,x0)+r by A6,AXIOMS:24;
then A8: dist(o,z)<=dist(o,x0)+r by A7,AXIOMS:22;
r+dist(o,x0)<r+dist(o,x0)+1 by REAL_1:69;
hence |.q1.|<R0 by A5,A8,AXIOMS:22;
end;
hence ex r2 being Real st for q being Point of TOP-REAL n st
q in A holds |.q.|<r2;
suppose C={};
then for q being Point of TOP-REAL n st q in A holds |.q.|<1 by A1;
hence ex r2 being Real st for q being Point of TOP-REAL n st
q in A holds |.q.|<r2;
end;
given r being Real such that
A9: for q being Point of TOP-REAL n st q in A holds |.q.|<r;
A is Subset of Euclid n by TOPREAL3:13;
then reconsider C=A as Subset of Euclid n;
now per cases;
suppose A10:C<>{};
consider x0 being Element of C;
x0 in C by A10;
then reconsider x0 as Point of Euclid n;
reconsider q0=x0 as Point of TOP-REAL n by TOPREAL3:13;
|.q0.|<r by A9,A10;
then A11:0<r by TOPRNS_1:26;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
set R0=r+r;
A12:0<R0 by A11,Th6;
for x,y being Point of (Euclid n) st x in C & y in C holds dist(x,y) <=
R0
proof let x,y be Point of (Euclid n);
assume A13:x in C & y in C;
then reconsider q1=x as Point of TOP-REAL n;
reconsider q2=y as Point of TOP-REAL n by A13;
A14:dist(x,y)<=dist(x,o)+dist(o,y) by METRIC_1:4;
dist(x,o)=|.q1-0.REAL n.| by JGRAPH_1:45
.=|.q1.| by Th13;
then A15:dist(x,o) <r by A9,A13;
dist(o,y)=|.q2-(0.REAL n) .| by JGRAPH_1:45
.=|.q2.| by Th13;
then dist(o,y) <r by A9,A13;
then dist(x,o)+dist(o,y)<=r+r by A15,REAL_1:55;
hence dist(x,y) <= R0 by A14,AXIOMS:22;
end;
hence C is bounded by A12,TBSP_1:def 9;
suppose C={};
then C = {}Euclid n;
hence C is bounded by TBSP_1:14;
end;
hence A is Bounded by Def2;
end;
theorem Th41: n>=1 implies not [#](TOP-REAL n) is Bounded
proof assume A1:n>=1;
assume [#](TOP-REAL n) is Bounded;
then consider C being Subset of Euclid n
such that A2:C=[#](TOP-REAL n) & C is bounded by Def2;
C=the carrier of TOP-REAL n by A2,PRE_TOPC:12;
then C=REAL n by EUCLID:25;
hence contradiction by A1,A2,Th39;
end;
theorem Th42: n>=1 implies UBD {}(TOP-REAL n)=REAL n
proof assume A1:n>=1;
UBD {}(TOP-REAL n) c= the carrier of TOP-REAL n;
hence UBD {}(TOP-REAL n) c= REAL n by EUCLID:25;
let x be set;assume x in REAL n;
then A2:x in the carrier of TOP-REAL n by EUCLID:25;
set A={}(TOP-REAL n);
A`=[#](TOP-REAL n) by PRE_TOPC:27;
then A3:A`=[#](TOP-REAL n);
A4:(TOP-REAL n)| [#](TOP-REAL n)=TOP-REAL n by TSEP_1:3;
A5: [#]((TOP-REAL n)|A`) = [#](TOP-REAL n) by A3,TSEP_1:3;
A6:[#]((TOP-REAL n)|A`) is_a_component_of (TOP-REAL n)|A` by A3,A4,Th23;
now assume A7:for D being Subset of Euclid n
st D=[#]((TOP-REAL n)|A`) holds D is bounded;
[#]((TOP-REAL n)|A`)=the carrier of TOP-REAL n by A3,A4,PRE_TOPC:12;
then [#]((TOP-REAL n)|A`) c= the carrier of Euclid n by TOPREAL3:13;
then reconsider D1=[#]((TOP-REAL n)|A`) as Subset of Euclid n
;
D1 is bounded by A7;
then [#](TOP-REAL n) is Bounded by A3,A4,Def2;
hence contradiction by A1,Th41;
end;
then x in [#](TOP-REAL n) &
[#](TOP-REAL n) is_outside_component_of {}(TOP-REAL n)
by A2,A5,A6,Th18,PRE_TOPC:12;
then x in [#](TOP-REAL n) & [#](TOP-REAL n) in
{B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of {}(TOP-REAL n)};
then x in union{B2 where B2 is Subset of TOP-REAL n:
B2 is_outside_component_of {}(TOP-REAL n)} by TARSKI:def 4;
hence x in UBD {}(TOP-REAL n) by Def6;
end;
theorem Th43:for w1,w2,w3 being Point of TOP-REAL n,
P being non empty Subset of TOP-REAL n,
h1,h2 being map of I[01],(TOP-REAL n)|P st
h1 is continuous & w1=h1.0 & w2=h1.1 &
h2 is continuous & w2=h2.0 & w3=h2.1
holds ex h3 being map of I[01],(TOP-REAL n)|P st
h3 is continuous & w1=h3.0 & w3=h3.1
proof let w1,w2,w3 be Point of TOP-REAL n,
P be non empty Subset of TOP-REAL n,
h1,h2 be map of I[01],(TOP-REAL n)|P;
assume A1:h1 is continuous & w1=h1.0 & w2=h1.1 &
h2 is continuous & w2=h2.0 & w3=h2.1;
A2: 0 in [.0 qua Real,1 qua Real.] by TOPREAL5:1;
1 in [.0 qua Real,1 qua Real.] by TOPREAL5:1;
then reconsider p1=w1,p2=w2,p3=w3 as Point of (TOP-REAL n)|P
by A1,A2,BORSUK_1:83,FUNCT_2:7;
reconsider P1=h1 as Path of p1,p2 by A1,BORSUK_2:def 1;
reconsider P2=h2 as Path of p2,p3 by A1,BORSUK_2:def 1;
ex P0 being Path of p1,p3 st P0 is continuous & P0.0=p1 & P0.1=p3 &
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies P0.t = P1.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies P0.t = P2.(2*t'-1) )
proof ::This proof is almost a copy of BORSUK_2:def 4(proof of Existence)
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set E1 = P1 * e1;
set E2 = P2 * e2;
set f = E1 +* E2;
A3:dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:25;
A4:dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1 qua Real.] by TOPMETR:25;
A5: dom P1 = the carrier of I[01] & dom P2 = the carrier of I[01]
by FUNCT_2:def 1;
then A6:rng e1 c= dom P1 by TOPMETR:27;
rng e2 c= the carrier of Closed-Interval-TSpace(0,1);
then A7: dom E2 = dom e2 by A5,RELAT_1:46,TOPMETR:27;
A8: dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1 qua Real.] by A3,A4,A6,A7,RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83,TREAL_1:2;
A9: for t' being Real st 0 <= t' & t' <= 1/2 holds E1.t' = P1.(2*t')
proof
let t' be Real such that
A10:0 <= t' & t' <= 1/2;
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then dom e1 = [.0, 1/2.] by TOPMETR:25
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
then A11: t' in dom e1 by A10;
then reconsider s = t' as Point of Closed-Interval-TSpace (0, 1/2)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e1.s = ((r2 - r1)/(1/2 - 0))*t' + ((1/2)*r1 - 0 * r2)/(1/2 - 0)
by TREAL_1:14
.= 2*t' by BORSUK_1:def 17,def 18,TREAL_1:8;
hence thesis by A11,FUNCT_1:23;
end;
not 0 in { r : 1/2 <= r & r <= 1 }
proof
assume 0 in { r : 1/2 <= r & r <= 1 };
then ex rr being Real st rr = 0 & 1/2 <= rr & rr <= 1;
hence thesis;
end;
then not 0 in dom E2 by A4,A7,RCOMP_1:def 1;
then A12:f.0 = E1.0 by FUNCT_4:12
.= P1.(2*0) by A9
.= p1 by A1;
rng E1 c= rng P1 & rng E2 c= rng P2 by RELAT_1:45;
then A13:rng E1 c= the carrier of ((TOP-REAL n)|P) &
rng E2 c= the carrier of ((TOP-REAL n)|P) by XBOOLE_1:1;
A14: rng f c= rng E1 \/ rng E2 by FUNCT_4:18;
rng E1 \/ rng E2 c= (the carrier of ((TOP-REAL n)|P))
\/ the carrier of ((TOP-REAL n)|P)
by A13,XBOOLE_1:13;
then rng f c= the carrier of ((TOP-REAL n)|P) by A14,XBOOLE_1:1;
then f is Function of the carrier of I[01], the carrier of ((TOP-REAL n)|P)
by A8,FUNCT_2:def 1,RELSET_1:11;
then reconsider f as map of I[01], ((TOP-REAL n)|P) ;
reconsider T1 = Closed-Interval-TSpace (0, 1/2),
T2 = Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01]
by TOPMETR:27,TREAL_1:6;
A15:e1 is continuous by TREAL_1:15;
A16:e2 is continuous by TREAL_1:15;
E1 is Function of the carrier of Closed-Interval-TSpace (0, 1/2),
the carrier of ((TOP-REAL n)|P) by FUNCT_2:19,TOPMETR:27;
then reconsider ff = E1 as map of T1, ((TOP-REAL n)|P) ;
A17:E2 is Function of the carrier of Closed-Interval-TSpace (1/2, 1),
the carrier of ((TOP-REAL n)|P) by FUNCT_2:19,TOPMETR:27;
then reconsider gg = E2 as map of T2, ((TOP-REAL n)|P) ;
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:83,RCOMP_1:def 1;
A18:ff is continuous & gg is continuous by A1,A15,A16,TOPMETR:27,TOPS_2:58;
A19:[#] T1 = the carrier of T1 by PRE_TOPC:12
.= [.0,1/2.] by TOPMETR:25;
A20:[#] T2 = the carrier of T2 by PRE_TOPC:12
.= [.1/2,1 qua Real.] by TOPMETR:25;
then A21: ([#] T1) \/ ([#] T2) = [.0,1 qua Real.] by A19,TREAL_1:2
.= [#] I[01] by BORSUK_1:83,PRE_TOPC:12;
A22: for t' being Real st 1/2 <= t' & t' <= 1 holds E2.t' = P2.(2*t'-1)
proof
let t' be Real such that
A23: 1/2 <= t' & t' <= 1;
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then dom e2 = [.1/2,1 qua Real.] by TOPMETR:25
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
then A24: t' in dom e2 by A23;
then reconsider s = t' as Point of Closed-Interval-TSpace (1/2,1)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e2.s = ((r2 - r1)/(1 - 1/2))*t' + (1 * r1 - (1/2)*r2)/(1 - 1/2)
by TREAL_1:14
.= 2*t' + (- 1) by BORSUK_1:def 17,def 18,TREAL_1:8
.= 2*t' - 1 by XCMPLX_0:def 8;
hence thesis by A24,FUNCT_1:23;
end;
A25:ff.(1/2) = P2.(2*(1/2)-1) by A1,A9
.= gg.pol by A22;
A26:([#] T1) /\ ([#] T2) = {pol} by A19,A20,TOPMETR2:1;
R^1 is_T2 by PCOMPS_1:38,TOPMETR:def 7;
then T1 is compact & T2 is compact & I[01] is_T2 & ff.pol = gg.pol
by A25,HEINE:11,TOPMETR:3;
then consider h being map of I[01], ((TOP-REAL n)|P) such that
A27: h = ff+*gg & h is continuous by A18,A21,A26,TOPMETR2:4;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A4,A7,RCOMP_1:def 1;
then A28: f.1 = E2.1 by FUNCT_4:14
.= P2.(2*1-1) by A22
.= p3 by A1;
then reconsider f as Path of p1, p3 by A12,A27,BORSUK_2:def 1;
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies f.t = P1.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies f.t = P2.(2*t'-1) )
proof
let t be Point of I[01], t' be Real;
assume A29: t = t';
thus 0 <= t' & t' <= 1/2 implies f.t = P1.(2*t')
proof
assume A30: 0 <= t' & t' <= 1/2;
then t' in { r : 0 <= r & r <= 1/2 };
then A31: t' in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose A32: t' <> 1/2;
not t' in dom E2
proof
assume t' in dom E2;
then t' in [.0,1/2.] /\ [.1/2,1 qua Real.] by A4,A7,A31,XBOOLE_0:def 3;
then t' in {1/2} by TOPMETR2:1;
hence thesis by A32,TARSKI:def 1;
end;
then f.t = E1.t by A29,FUNCT_4:12
.= P1.(2*t') by A9,A29,A30;
hence thesis;
suppose A33: t' = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1 qua Real.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1)
by TOPMETR:25;
then t in dom E2 by A17,A29,A33,FUNCT_2:def 1;
then f.t = E2.(1/2) by A29,A33,FUNCT_4:14
.= P1.(2*t') by A9,A25,A33;
hence thesis;
end;
thus 1/2 <= t' & t' <= 1 implies f.t = P2.(2*t'-1)
proof
assume A34: 1/2 <= t' & t' <= 1;
then t' in { r : 1/2 <= r & r <= 1 };
then t' in [.1/2,1 qua Real.] by RCOMP_1:def 1;
then f.t = E2.t by A4,A7,A29,FUNCT_4:14
.= P2.(2*t'-1) by A22,A29,A34;
hence thesis;
end;
end;
hence thesis by A12,A27,A28;
end;
hence thesis;
end;
theorem Th44: for P being Subset of TOP-REAL n,
w1,w2,w3 being Point of TOP-REAL n
st w1 in P & w2 in P & w3 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P
ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1
proof let P be Subset of TOP-REAL n,
w1,w2,w3 be Point of TOP-REAL n;
assume A1:w1 in P & w2 in P & w3 in P & LSeg(w1,w2) c= P
& LSeg(w2,w3) c= P;
then reconsider Y = P as non empty Subset of TOP-REAL n;
per cases;
suppose A2:w1<>w2;
then LSeg(w1,w2) is_an_arc_of w1,w2 by TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w1,w2)
such that A3: f is_homeomorphism & f.0 = w1 & f.1 = w2 by TOPREAL1:
def 2;
A4:f is continuous by A3,TOPS_2:def 5;
A5: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A3,TOPS_2:def 5;
then A6: rng f c= P by A1,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
by A5,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w1,w2))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A7:(TOP-REAL n)|LSeg(w1,w2)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f= ([.0 qua Real ,1 qua Real.]) by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of ([.0 qua Real,1 qua Real.]),P
by A6,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt=g as map of I[01],(TOP-REAL n)|Y
by BORSUK_1:83;
now per cases;
suppose w2<>w3;
then LSeg(w2,w3) is_an_arc_of w2,w3 by TOPREAL1:15;
then consider f2 being map of I[01], (TOP-REAL n)|LSeg(w2,w3)
such that A8: f2 is_homeomorphism & f2.0 = w2 & f2.1 = w3 by
TOPREAL1:def 2;
A9:f2 is continuous by A8,TOPS_2:def 5;
A10: rng f2 = [#]((TOP-REAL n)|LSeg(w2,w3)) by A8,TOPS_2:def 5;
then A11: rng f2 c= P by A1,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w2,w3)) c= [#]((TOP-REAL n)|P)
by A10,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w2,w3))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w2,w3))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A12:(TOP-REAL n)|LSeg(w2,w3)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f2=[.0 qua Real,1 qua Real.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g2=f2 as Function of ([.0 qua Real,1 qua Real.]),P
by A11,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt2=g2 as map of I[01],(TOP-REAL n)|Y
by BORSUK_1:83;
A13:gt2 is continuous by A9,A12,TOPMETR:7;
[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
then reconsider w1'=w1,w2'=w2,w3'=w3 as Point of (TOP-REAL n)|P by A1;
gt is continuous & w1'=gt.0 & w2'=gt.1 by A3,A4,A7,TOPMETR:7;
then ex h being map of I[01],(TOP-REAL n)|Y st h is continuous
& w1'=h.0 & w3'=h.1 & rng h c= (rng gt) \/ (rng gt2)
by A8,A13,Th32;
hence ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1;
suppose A14:w2=w3;
then LSeg(w1,w3) is_an_arc_of w1,w3 by A2,TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w1,w3)
such that A15: f is_homeomorphism & f.0 = w1 & f.1 = w3 by TOPREAL1
:def 2;
A16:f is continuous by A15,TOPS_2:def 5;
A17: rng f = [#]((TOP-REAL n)|LSeg(w1,w3)) by A15,TOPS_2:def 5;
then A18: rng f c= P by A1,A14,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w3)) c= [#]((TOP-REAL n)|P)
by A17,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w3))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w1,w3))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A19:(TOP-REAL n)|LSeg(w1,w3)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f=[.0 qua Real ,1 qua Real.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of ([.0 qua Real,1 qua Real.]),P
by A18,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt=g as map of I[01],(TOP-REAL n)|Y
by BORSUK_1:83;
gt is continuous by A16,A19,TOPMETR:7;
hence ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1 by A15;
end;
hence ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1;
suppose A20:w1=w2;
now per cases;
case w2<>w3;
then LSeg(w1,w3) is_an_arc_of w1,w3 by A20,TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w1,w3)
such that A21: f is_homeomorphism & f.0 = w1 & f.1 = w3 by TOPREAL1
:def 2;
A22:f is continuous by A21,TOPS_2:def 5;
A23: rng f = [#]((TOP-REAL n)|LSeg(w1,w3)) by A21,TOPS_2:def 5;
then A24: rng f c= P by A1,A20,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w3)) c= [#]((TOP-REAL n)|P)
by A23,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w3))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w1,w3))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A25:(TOP-REAL n)|LSeg(w1,w3)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f=[.0 qua Real,1 qua Real.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of [.0 qua Real,1 qua Real.],P
by A24,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt=g as map of I[01],(TOP-REAL n)|Y
by BORSUK_1:83;
gt is continuous by A22,A25,TOPMETR:7;
hence ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1 by A21;
case A26:w2=w3;
[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
then reconsider w1'=w1,w3'=w3 as Point of (TOP-REAL n)|P by A1;
ex f be map of I[01], (TOP-REAL n)|Y st
f is continuous & f.0 = w1' & f.1 = w3' by A20,A26,BORSUK_2:4;
hence ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w3=h.1;
end;
hence thesis;
end;
theorem Th45: for P being Subset of TOP-REAL n,
w1,w2,w3,w4 being Point of TOP-REAL n
st w1 in P & w2 in P & w3 in P & w4 in P &
LSeg(w1,w2) c= P & LSeg(w2,w3) c= P &
LSeg(w3,w4) c= P
ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w4=h.1
proof let P be Subset of TOP-REAL n,
w1,w2,w3,w4 be Point of TOP-REAL n;
assume A1: w1 in P & w2 in P & w3 in P & w4 in P &
LSeg(w1,w2) c= P & LSeg(w2,w3) c= P &
LSeg(w3,w4) c= P;
then consider h2 being map of I[01],(TOP-REAL n)|P such that
A2: h2 is continuous & w1=h2.0 & w3=h2.1 by Th44;
reconsider Y = P as non empty Subset of TOP-REAL n by A1;
per cases;
suppose w3<>w4;
then LSeg(w3,w4) is_an_arc_of w3,w4 by TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w3,w4)
such that A3: f is_homeomorphism & f.0 = w3 & f.1 = w4 by TOPREAL1:
def 2;
A4:f is continuous by A3,TOPS_2:def 5;
A5: rng f = [#]((TOP-REAL n)|LSeg(w3,w4)) by A3,TOPS_2:def 5;
then A6: rng f c= P by A1,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w3,w4)) c= [#]((TOP-REAL n)|P)
by A5,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w3,w4))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w3,w4))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A7:(TOP-REAL n)|LSeg(w3,w4)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f=[.0 qua Real,1 qua Real.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of [.0 qua Real,1 qua Real.],P
by A6,FUNCT_2:4;
the carrier of (TOP-REAL n)|P = P by JORDAN1:1;
then reconsider gt=g as map of I[01],(TOP-REAL n)|Y
by BORSUK_1:83;
A8:gt is continuous by A4,A7,TOPMETR:7;
[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
then reconsider w1'=w1,w3'=w3,w4'=w4 as Point of (TOP-REAL n)|P by A1;
h2 is continuous & w1'=h2.0 & w3'=h2.1 by A2;
then ex h being map of I[01],(TOP-REAL n)|Y st h is continuous
& w1'=h.0 & w4'=h.1 & rng h c= (rng h2) \/ (rng gt) by A3,A8,Th32;
hence thesis;
suppose w3=w4;
hence thesis by A2;
end;
theorem Th46: for P being Subset of TOP-REAL n,
w1,w2,w3,w4,w5,w6,w7 being Point of TOP-REAL n
st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P &
LSeg(w1,w2) c= P & LSeg(w2,w3) c= P &
LSeg(w3,w4) c= P & LSeg(w4,w5) c= P & LSeg(w5,w6) c= P
& LSeg(w6,w7) c= P
ex h being map of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w7=h.1
proof let P be Subset of TOP-REAL n,
w1,w2,w3,w4,w5,w6,w7 be Point of TOP-REAL n;
assume A1: w1 in P & w2 in P & w3 in P &
w4 in P & w5 in P & w6 in P & w7 in P &
LSeg(w1,w2) c= P & LSeg(w2,w3) c= P &
LSeg(w3,w4) c= P & LSeg(w4,w5) c= P & LSeg(w5,w6) c= P
& LSeg(w6,w7) c= P;
then A2: ex h2 being map of I[01],(TOP-REAL n)|P st
h2 is continuous & w1=h2.0 & w4=h2.1 by Th45;
ex h4 being map of I[01],(TOP-REAL n)|P st
h4 is continuous & w4=h4.0 & w7=h4.1 by A1,Th45;
hence thesis by A1,A2,Th43;
end;
reserve s2 for Real;
theorem Th47: for w1,w2 being Point of TOP-REAL n st
not (ex r being Real st w1=r*w2 or w2=r*w1)
holds not (0.REAL n) in LSeg(w1,w2)
proof let w1,w2 be Point of TOP-REAL n;
assume A1:not (ex r being Real st w1=r*w2 or w2=r*w1);
assume (0.REAL n) in LSeg(w1,w2);
then (0.REAL n) in { (1-s)*w1 + s*w2 : 0 <= s & s <= 1 } by TOPREAL1:def 4;
then consider s being Real such that
A2:(0.REAL n)=(1-s)*w1 + s*w2 &( 0 <= s & s <= 1 );
(0.REAL n)-s*w2=(1-s)*w1 by A2,EUCLID:52;
then -s*w2=(1-s)*w1 by Th13;
then A3:(-s)*w2=(1-s)*w1 by EUCLID:44;
per cases;
suppose A4: -s<>0;
((-s)"*(-s))*w2=(-s)"*((1-s)*w1) by A3,EUCLID:34;
then ((-s)"*(-s))*w2=((-s)"*(1-s))*w1 by EUCLID:34;
then (1)*w2=((-s)"*(1-s))*w1 by A4,XCMPLX_0:def 7;
then w2=((-s)"*(1-s))*w1 by EUCLID:33;
hence contradiction by A1;
suppose -s=0; then 1+-s=1+0; then 1-s=1 by XCMPLX_0:def 8;
then (-s)*w2=w1 by A3,EUCLID:33;
hence contradiction by A1;
end;
theorem Th48: for w1,w2 being Point of TOP-REAL n,P being Subset of
TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)&
not (0.REAL n) in LSeg(w1,w2) holds ex w0 being Point of TOP-REAL n st
w0 in LSeg(w1,w2) & |.w0.|>0 & |.w0.|=(dist_min(P)).(0.REAL n)
proof let w1,w2 be Point of TOP-REAL n,P be Subset of
TopSpaceMetr(Euclid n);
assume A1:P=LSeg(w1,w2)& not 0.REAL n in LSeg(w1,w2);
set M=Euclid n;
reconsider P0=P as Subset of TopSpaceMetr(M);
reconsider P1=P as Subset of TOP-REAL n by EUCLID:def 8;
reconsider o=0.REAL n as Point of M by TOPREAL3:13;
A2:TOP-REAL n=TopSpaceMetr(M) by EUCLID:def 8;
reconsider o2=0.REAL n as Point of TopSpaceMetr(M) by EUCLID:def 8;
A3:P0 is compact by A1,A2,SPPOL_1:28;
reconsider Q={0.REAL n} as Subset of TopSpaceMetr(M) by EUCLID:def 8;
0.REAL n is Point of TopSpaceMetr(M) by EUCLID:def 8;
then Q is compact by BORSUK_1:41;
then consider x1,x2 being Point of M such that
A4:x1 in P0 & x2 in Q &
dist(x1,x2) = min_dist_min(P0,Q) by A1,A3,WEIERSTR:36;
A5: for x being set holds x in (dist_min(P0)).:(Q) iff x=(dist_min(P0)).o
proof let x be set;
hereby assume x in (dist_min(P0)).:(Q);
then consider y being set such that
A6: y in dom(dist_min(P0)) &
y in Q & x=(dist_min(P0)).y by FUNCT_1:def 12;
thus x=(dist_min(P0)).o by A6,TARSKI:def 1;
end;
assume A7:x=(dist_min(P0)).o;
A8:o in Q by TARSKI:def 1;
o2 in the carrier of TopSpaceMetr(M);
then o in dom (dist_min(P0)) by FUNCT_2:def 1;
hence thesis by A7,A8,FUNCT_1:def 12;
end;
A9:[#] ((dist_min(P0)).:(Q))=(dist_min(P0)).:(Q) by WEIERSTR:def 3;
A10: (dist_min(P0)).:(Q)={(dist_min(P0)).o} by A5,TARSKI:def 1;
lower_bound([#] ((dist_min(P0)).:(Q)))=lower_bound((dist_min(P0)).:(Q))
by WEIERSTR:def 5;
then lower_bound((dist_min(P0)).:(Q))=(dist_min(P0)).o
by A9,A10,SEQ_4:22;
then A11:dist(x1,x2)=(dist_min(P)).(0.REAL n) by A4,WEIERSTR:def 9;
A12:x2=0.REAL n by A4,TARSKI:def 1;
x1 in P1 by A4;
then reconsider w01=x1 as Point of TOP-REAL n;
A13: |.w01.|=|.w01-0.REAL n.| by Th13 .=dist(x1,x2) by A12,JGRAPH_1:45;
A14: |.w01.|>=0 by TOPRNS_1:26;
|.w01.| <> 0 by A1,A4,TOPRNS_1:25;
hence thesis by A1,A4,A11,A13,A14;
end;
theorem Th49: for a being Real,
Q being Subset of TOP-REAL n,
w1,w4 being Point of TOP-REAL n
st Q={q : (|.q.|) > a } & w1 in Q & w4 in Q &
not (ex r being Real st w1=r*w4 or w4=r*w1)
holds ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q
proof let a be Real,
Q be Subset of TOP-REAL n,
w1,w4 be Point of TOP-REAL n;
assume A1: Q={q : (|.q.|) > a } & w1 in Q & w4 in Q &
not (ex r being Real st w1=r*w4 or w4=r*w1);
then A2:not (0.REAL n) in LSeg(w1,w4) by Th47;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
consider w0 being Point of TOP-REAL n such that
A3:w0 in LSeg(w1,w4) & |.w0.|>0 & |.w0.|=(dist_min(P)).(0.REAL n)
by A2,Th48;
set l'=(a+1)/|.w0.|;
set w2= l'*w1,w3=l'*w4;
A4:LSeg(w2,w3)c=Q
proof let x be set;assume x in LSeg(w2,w3);
then x in { (1-r)*w2 + r*w3 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A5: x=(1-r)*w2 + r*w3 &( 0 <= r & r <= 1);
reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w1 + r1*w4:0 <= r1 & r1 <= 1} by A5;
then A6:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A7:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
(dist(o)).:(P) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A8: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A8,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A8;
end;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
A9:w5' in the carrier of TopSpaceMetr(Euclid n) by A7,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A10:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A10,TOPREAL3:13;
r=dist(w0,o) by A10,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A11:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A9,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A6,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A11,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A12: |.w5.| >=|.w0.| by Th13;
A13:abs(a+1)>=0 by ABSVALUE:5;
A14: |.w0.| >= 0 by TOPRNS_1:26;
A15:abs l' = abs(a+1)/abs |.w0.| by ABSVALUE:16
.=abs(a+1)/|.w0.| by A14,ABSVALUE:def 1;
|.w5.|/|.w0.|>=1 by A3,A12,REAL_2:143;
then abs(a+1)*(|.w5.|/|.w0.|)>=abs(a+1)*1 by A13,REAL_2:197;
then abs(a+1)*(|.w0.|"*|.w5.|)>=abs(a+1) by XCMPLX_0:def 9;
then abs(a+1)*|.w0.|"*|.w5.|>=abs(a+1) by XCMPLX_1:4;
then A16:abs(a+1)/|.w0.|*|.w5.|>=abs(a+1) by XCMPLX_0:def 9;
A17:a+1>a by REAL_1:69;
abs(a+1)>=a+1 by ABSVALUE:11;
then abs(a+1)>a by A17,AXIOMS:22;
then abs(a+1)/|.w0.|*|.w5.|>a by A16,AXIOMS:22;
then |.l'*((1-r)*w1 + r*w4).|>a by A15,TOPRNS_1:8;
then |.l'*((1-r)*w1) + l'*(r*w4).|>a by EUCLID:36;
then |.l'*((1-r)*w1) + (l'*r)*w4.|>a by EUCLID:34;
then |.(l'*(1-r))*w1 + (l'*r)*w4.|>a by EUCLID:34;
then |.((1-r)*l')*w1 + r*(l'*w4).|>a by EUCLID:34;
then |.(1-r)*w2 + r*w3.|>a by EUCLID:34;
hence x in Q by A1,A5;
end;
A18:w2 in LSeg(w2,w3) & w3 in LSeg(w2,w3) by TOPREAL1:6;
then A19:w2 in Q by A4;
A20:w3 in Q by A4,A18;
A21: LSeg(w1,w2) c=Q
proof let x be set;assume x in LSeg(w1,w2);
then x in { (1-r)*w1 + r*w2 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A22: x=(1-r)*w1 + r*w2 &( 0 <= r & r <= 1);
now per cases;
case A23:a>=0; a+1>a by REAL_1:69;
then (a+1)/|.w0.|>0 by A3,A23,REAL_2:127;
then A24: r*l'>=0 by A22,REAL_2:121;
reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n;
A25:(1-0)*w1+0 * w4=(1-0)*w1+0.REAL n by EUCLID:33
.=(1-0)*w1 by EUCLID:31
.=w1 by EUCLID:33;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w1 + r1*w4:0 <= r1 & r1 <= 1};
then A26:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A27:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
((dist(o)).:(P)) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A28: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A28,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A28;
end;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
A29:w5' in the carrier of TopSpaceMetr(Euclid n) by A27,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A30:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A30,TOPREAL3:13;
r=dist(w0,o) by A30,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A31:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A29,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A26,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A31,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A32: |.w5.| >=|.w0.| by Th13;
r*l'*|.w0.|
=r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:75
.=r*(a+1) by A3,XCMPLX_1:88;
then A33:r*l'*|.w1.|>= r*(a+1) by A24,A25,A32,AXIOMS:25;
consider q1 being Point of TOP-REAL n such that
A34:q1=w1 & |.q1.| > a by A1;
consider q2 being Point of TOP-REAL n such that
A35:q2=w2 & |.q2.| > a by A1,A19;
A36:1-r>=0 by A22,SQUARE_1:12;
A37: a+r>=a+0 by A22,AXIOMS:24;
now per cases;
case 1-r>0;
then A38:(1-r)*|.w1.|>(1-r)*a by A34,REAL_1:70;
(1-r)+ r*l'>=0 by A24,A36,Th5;
then abs((1-r)+ r*l')*|.w1.|=((1-r)+ r*l')*|.w1.| by ABSVALUE:def 1
.= (1-r)*|.w1.|+r*l'*|.w1.| by XCMPLX_1:8;
then A39:abs((1-r)+ r*l')*|.w1.|>r*(a+1)+(1-r)*a by A33,A38,REAL_1:67;
r*(a+1)+(1-r)*a=r*a +r*1 +(1-r)*a by XCMPLX_1:8
.=r*a +(1-r)*a+r*1 by XCMPLX_1:1
.=(r+(1-r))*a+r*1 by XCMPLX_1:8
.=1 * a+r*1 by XCMPLX_1:27
.=a+r;
then abs((1-r)+ r*l')*|.w1.|>a by A37,A39,AXIOMS:22;
then |.((1-r)+ r*l')*w1.|>a by TOPRNS_1:8;
then |.(1-r)*w1 + r*l'*w1.|>a by EUCLID:37;
hence |.(1-r)*w1 + r*w2.|>a by EUCLID:34;
case 1-r<=0; then 1-r+r<=0+r by AXIOMS:24;
then 1<=0+r by XCMPLX_1:27;
then r=1 by A22,AXIOMS:21;
then (1-r)*w1+r*w2=0.REAL n +1 * w2 by EUCLID:33
.=0.REAL n +w2 by EUCLID:33
.=w2 by EUCLID:31;
hence |.(1-r)*w1 + r*w2.|>a by A35;
end;
hence |.(1-r)*w1 + r*w2.|>a;
case A40:a<0;
|.(1-r)*w1 + r*w2.|>=0 by TOPRNS_1:26;
hence |.(1-r)*w1 + r*w2.|>a by A40;
end;
hence x in Q by A1,A22;
end;
LSeg(w4,w3) c=Q
proof let x be set;assume x in LSeg(w4,w3);
then x in { (1-r)*w4 + r*w3 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A41: x=(1-r)*w4 + r*w3 &( 0 <= r & r <= 1);
now per cases;
case A42:a>=0;
a<a+1 by REAL_1:69;
then (a+1)/|.w0.|>0 by A3,A42,REAL_2:127;
then A43: r*l'>=0 by A41,REAL_2:121;
reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n;
A44:(1-0)*w4+0 * w1=(1-0)*w4+0.REAL n by EUCLID:33
.=(1-0)*w4 by EUCLID:31
.=w4 by EUCLID:33;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1};
then A45:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A46:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
(dist(o)).:(P) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A47: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A47,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A47;
end;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
A48:w5' in the carrier of TopSpaceMetr(Euclid n) by A46,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A49:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A49,TOPREAL3:13;
r=dist(w0,o) by A49,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A50:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A48,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A45,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A50,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A51: |.w5.| >=|.w0.| by Th13;
r*l'*|.w0.|
=r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:75
.=r*(a+1) by A3,XCMPLX_1:88;
then A52:r*l'*|.w4.|>= r*(a+1) by A43,A44,A51,AXIOMS:25;
consider q1 being Point of TOP-REAL n such that
A53:q1=w4 & |.q1.| > a by A1;
A54:1-r>=0 by A41,SQUARE_1:12;
A55: a+r>=a+0 by A41,AXIOMS:24;
now per cases;
case 1-r>0;
then A56:(1-r)*|.w4.|>(1-r)*a by A53,REAL_1:70;
(1-r)+ r*l'>=0 by A43,A54,Th5;
then abs((1-r)+ r*l')*|.w4.|=((1-r)+ r*l')*|.w4.| by ABSVALUE:def 1
.= (1-r)*|.w4.|+r*l'*|.w4.| by XCMPLX_1:8;
then A57:abs((1-r)+r*l')*|.w4.|>r*(a+1)+(1-r)*a by A52,A56,REAL_1:67;
r*(a+1)+(1-r)*a=r*a +r*1 +(1-r)*a by XCMPLX_1:8
.=r*a +(1-r)*a+r*1 by XCMPLX_1:1
.=(r+(1-r))*a+r*1 by XCMPLX_1:8
.=1 * a+r*1 by XCMPLX_1:27
.=a+r;
then abs((1-r)+r*l')*|.w4.|>a by A55,A57,AXIOMS:22;
then |.((1-r)+ r*l')*w4.|>a by TOPRNS_1:8;
then |.(1-r)*w4 + r*l'*w4.|>a by EUCLID:37;
hence |.(1-r)*w4 + r*w3.|>a by EUCLID:34;
case 1-r<=0; then 1-r+r<=0+r by AXIOMS:24;
then 1<=0+r by XCMPLX_1:27;
then r=1 by A41,AXIOMS:21;
then A58:(1-r)*w4+r*w3=0.REAL n +1 * w3 by EUCLID:33
.=0.REAL n +w3 by EUCLID:33
.=w3 by EUCLID:31;
consider q3 being Point of TOP-REAL n such that
A59:q3=w3 & |.q3.| > a by A1,A20;
thus |.(1-r)*w4 + r*w3.|>a by A58,A59;
end;
hence |.(1-r)*w4 + r*w3.|>a;
case A60:a<0;
|.(1-r)*w4 + r*w3.|>=0 by TOPRNS_1:26;
hence |.(1-r)*w4 + r*w3.|>a by A60;
end;
hence x in Q by A1,A41;
end;
hence thesis by A4,A18,A21;
end;
theorem Th50: for a being Real,
Q being Subset of TOP-REAL n,
w1,w4 being Point of TOP-REAL n
st Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w4 in Q &
not (ex r being Real st w1=r*w4 or w4=r*w1)
holds ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q
proof let a be Real,
Q be Subset of TOP-REAL n,
w1,w4 be Point of TOP-REAL n;
assume A1: Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w4 in Q &
not (ex r being Real st w1=r*w4 or w4=r*w1);
then A2:not (0.REAL n) in LSeg(w1,w4) by Th47;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
consider w0 being Point of TOP-REAL n such that
A3:w0 in LSeg(w1,w4) & |.w0.|>0 & |.w0.|=(dist_min(P)).(0.REAL n)
by A2,Th48;
set l'=a/|.w0.|;
set w2= l'*w1,w3=l'*w4;
A4:(REAL n)\ {q : (|.q.|) < a } = {q1 : (|.q1.|) >= a }
proof thus (REAL n)\ {q : (|.q.|) < a } c= {q1 : (|.q1.|) >= a }
proof let z be set;assume z in (REAL n)\ {q : (|.q.|) < a };
then A5:z in REAL n & not z in {q : (|.q.|) < a } by XBOOLE_0:def 4;
then reconsider q2=z as Point of TOP-REAL n by EUCLID:25;
|.q2.| >= a by A5;
hence z in {q1 : (|.q1.|) >= a };
end;
let z be set;assume z in {q1 : (|.q1.|) >= a };
then consider q1 such that A6:z=q1 & (|.q1.|) >= a;
A7: q1 in the carrier of TOP-REAL n;
for q st q=z holds (|.q.|) >= a by A6;
then z in REAL n & not z in {q : (|.q.|) < a } by A6,A7,EUCLID:25;
hence thesis by XBOOLE_0:def 4;
end;
A8:LSeg(w2,w3)c=Q
proof let x be set;assume x in LSeg(w2,w3);
then x in {(1-r)*w2 + r*w3 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A9: x=(1-r)*w2 + r*w3 &( 0 <= r & r <= 1);
reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w1 + r1*w4:0 <= r1 & r1 <= 1} by A9;
then A10:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A11:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
((dist(o)).:(P)) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A12: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A12,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A12;
end;
then reconsider F=(dist(o)).:(P) as Subset of REAL;
A13:w5' in the carrier of TopSpaceMetr(Euclid n) by A11,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A14:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A14,TOPREAL3:13;
r=dist(w0,o) by A14,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A15:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A13,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A10,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A15,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A16: |.w5.| >=|.w0.| by Th13;
A17:abs(a)>=0 by ABSVALUE:5;
A18: |.w0.| >= 0 by TOPRNS_1:26;
A19:abs l'=abs(a)/(abs|.w0.|) by ABSVALUE:16
.=abs(a)/|.w0.| by A18,ABSVALUE:def 1;
|.w5.|/|.w0.|>=1 by A3,A16,REAL_2:143;
then abs(a)*(|.w5.|/|.w0.|)>=abs(a)*1 by A17,REAL_2:197;
then abs(a)*(|.w5.|*|.w0.|")>=abs(a) by XCMPLX_0:def 9;
then abs(a)*|.w0.|"*|.w5.|>=abs(a) by XCMPLX_1:4;
then A20:abs(a)/|.w0.|*|.w5.|>=abs(a) by XCMPLX_0:def 9;
abs(a)>=a by ABSVALUE:11;
then abs(a)/|.w0.|*|.w5.|>=a by A20,AXIOMS:22;
then |.l'*((1-r)*w1 + r*w4).|>=a by A19,TOPRNS_1:8;
then |.l'*((1-r)*w1) + l'*(r*w4).|>=a by EUCLID:36;
then |.l'*((1-r)*w1) + (l'*r)*w4.|>=a by EUCLID:34;
then |.(l'*(1-r))*w1 + (l'*r)*w4.|>=a by EUCLID:34;
then |.((1-r)*l')*w1 + r*(l'*w4).|>=a by EUCLID:34;
then |.(1-r)*w2 + r*w3.|>=a by EUCLID:34;
hence x in Q by A1,A4,A9;
end;
A21:w2 in LSeg(w2,w3) & w3 in LSeg(w2,w3) by TOPREAL1:6;
A22: LSeg(w1,w2) c=Q
proof let x be set;assume x in LSeg(w1,w2);
then x in { (1-r)*w1 + r*w2 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A23: x=(1-r)*w1 + r*w2 &( 0 <= r & r <= 1);
now per cases;
case a>0;
then a/|.w0.|>0 by A3,REAL_2:127;
then A24: r*l'>=0 by A23,REAL_2:121;
reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n;
A25:(1-0)*w1+0 * w4=(1-0)*w1+0.REAL n
by EUCLID:33.=(1-0)*w1 by EUCLID:31
.=w1 by EUCLID:33;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w1 + r1 * w4:0 <= r1 & r1 <= 1};
then A26:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A27:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
((dist(o)).:(P)) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A28: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A28,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A28;
end;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
A29:w5' in the carrier of TopSpaceMetr(Euclid n) by A27,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A30:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A30,TOPREAL3:13;
r=dist(w0,o) by A30,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A31:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A29,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A26,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A31,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A32: |.w5.| >=|.w0.| by Th13;
r*l'*|.w0.|
=r*a/|.w0.|*|.w0.| by XCMPLX_1:75
.=r*a by A3,XCMPLX_1:88;
then A33:r*l'*|.w1.|>= r*a by A24,A25,A32,AXIOMS:25;
consider q1 being Point of TOP-REAL n such that
A34:q1=w1 & |.q1.| >= a by A1,A4;
A35:1-r>=0 by A23,SQUARE_1:12;
then A36:(1-r)*|.w1.|>=(1-r)*a by A34,AXIOMS:25;
(1-r)+ r*l'>=0 by A24,A35,Th5;
then abs((1-r)+r*l')*|.w1.|=((1-r)+ r*l')*|.w1.| by ABSVALUE:def 1
.= (1-r)*|.w1.|+r*l'*|.w1.| by XCMPLX_1:8;
then A37:abs((1-r)+r*l')*|.w1.|>=r*a+(1-r)*a by A33,A36,REAL_1:55;
r*a+(1-r)*a
=(r+(1-r))*a by XCMPLX_1:8
.=1 * a by XCMPLX_1:27
.=a;
then |.((1-r)+ r*l')*w1.|>=a by A37,TOPRNS_1:8;
then |.(1-r)*w1 + r*l'*w1.|>=a by EUCLID:37;
hence |.(1-r)*w1 + r*w2.|>=a by EUCLID:34;
case a<=0;
hence |.(1-r)*w1 + r*w2.|>=a by TOPRNS_1:26;
end;
hence x in Q by A1,A4,A23;
end;
LSeg(w4,w3) c=Q
proof let x be set;assume x in LSeg(w4,w3);
then x in { (1-r)*w4 + r*w3 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A38: x=(1-r)*w4 + r*w3 &( 0 <= r & r <= 1);
now per cases;
case a>0;
then a/|.w0.|>0 by A3,REAL_2:127;
then A39: r*l'>=0 by A38,REAL_2:121;
reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n;
A40:(1-0)*w4+0 * w1=(1-0)*w4+0.REAL n by EUCLID:33
.=(1-0)*w4 by EUCLID:31
.=w4 by EUCLID:33;
reconsider w5'=w5 as Point of Euclid n by TOPREAL3:13;
w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1};
then A41:w5 in LSeg(w1,w4) by TOPREAL1:def 4;
A42:w5' in the carrier of TOP-REAL n;
reconsider o=0.REAL n as Point of Euclid n by TOPREAL3:13;
reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n)
by EUCLID:def 8;
((dist(o)).:(P)) c= REAL
proof let x be set;assume x in ((dist(o)).:(P));
then consider z being set such that
A43: z in dom (dist(o)) & z in P & x=(dist(o)).z by FUNCT_1:def 12;
reconsider z2=z as Point of Euclid n by A43,TOPREAL3:13;
(dist(o)).z2 =dist(z2,o) by WEIERSTR:def 6;
hence x in REAL by A43;
end;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
A44:w5' in the carrier of TopSpaceMetr(Euclid n) by A42,EUCLID:def 8;
for r being real number st r in ((dist(o)).:(P)) holds 0<=r
proof let r be real number;assume r in ((dist(o)).:(P));
then consider x being set
such that A45:x in dom (dist(o)) &
x in P & r=(dist(o)).x by FUNCT_1:def 12;
reconsider w0=x as Point of Euclid n by A45,TOPREAL3:13;
r=dist(w0,o) by A45,WEIERSTR:def 6;
hence 0<=r by METRIC_1:5;
end;
then A46:F is bounded_below by SEQ_4:def 2;
w5' in dom (dist(o)) & dist(w5',o)=(dist(o)).w5'
by A44,FUNCT_2:def 1,WEIERSTR:def 6;
then dist(w5',o) in ((dist(o)).:(P)) by A41,FUNCT_1:def 12;
then lower_bound F <=dist(w5',o) by A46,SEQ_4:def 5;
then dist(w5',o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 3;
then dist(w5',o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 5;
then dist(w5',o)>=|.w0.| by A3,WEIERSTR:def 8;
then |.w5-0.REAL n.| >=|.w0.| by JGRAPH_1:45;
then A47: |.w5.| >=|.w0.| by Th13;
r*l'*|.w0.|
=r*a/|.w0.|*|.w0.| by XCMPLX_1:75
.=r*a by A3,XCMPLX_1:88;
then A48:r*l'*|.w4.|>= r*a by A39,A40,A47,AXIOMS:25;
consider q1 being Point of TOP-REAL n such that
A49:q1=w4 & |.q1.| >= a by A1,A4;
A50:1-r>=0 by A38,SQUARE_1:12;
then A51:(1-r)*|.w4.|>=(1-r)*a by A49,AXIOMS:25;
(1-r)+ r*l'>=0 by A39,A50,Th5;
then abs((1-r)+r*l')*|.w4.|=((1-r)+ r*l')*|.w4.| by ABSVALUE:def 1
.= (1-r)*|.w4.|+r*l'*|.w4.| by XCMPLX_1:8;
then A52:abs((1-r)+r*l')*|.w4.|>=r*a+(1-r)*a by A48,A51,REAL_1:55;
r*a+(1-r)*a
=(r+(1-r))*a by XCMPLX_1:8
.=1 * a by XCMPLX_1:27
.=a;
then |.((1-r)+ r*l')*w4.|>=a by A52,TOPRNS_1:8;
then |.(1-r)*w4 + r*l'*w4.|>=a by EUCLID:37;
hence |.(1-r)*w4 + r*w3.|>=a by EUCLID:34;
case a<=0;
hence |.(1-r)*w4 + r*w3.|>=a by TOPRNS_1:26;
end;
hence x in Q by A1,A4,A38;
end;
hence thesis by A8,A21,A22;
end;
canceled;
theorem Th52:for f being FinSequence of REAL holds f is Element of REAL (len f)
& f is Point of TOP-REAL (len f)
proof let f be FinSequence of REAL;
f is Element of REAL* by FINSEQ_1:def 11;
then f in { s where s is Element of REAL*: len s = len f };
then f in ((len f)-tuples_on REAL) by FINSEQ_2:def 4;
then f is Element of REAL (len f) by EUCLID:def 1;
hence thesis by EUCLID:25;
end;
theorem Th53:for x being Element of REAL n,f,g being FinSequence of REAL,
r being Real st f=x & g=r*x holds len f=len g &
for i being Nat st 1<=i & i<=len f holds g/.i=r*f/.i
proof let x be Element of REAL n,f,g be FinSequence of REAL,r be Real;
assume A1: f=x & g=r*x;
then A2:len f=n by EUCLID:2;
A3:len g=n by A1,EUCLID:2;
g=(r multreal)*x by A1,RVSUM_1:def 7;
then A4:g=(multreal[;](r,id REAL))*x by RVSUM_1:def 3;
set h1= (dom (id REAL)) --> r;
reconsider h2= (id REAL) as Function;
A5:g= (multreal * (<:h1, h2:>))*x by A4,FUNCOP_1:def 5;
A6: dom (<:h1, h2:>)=dom (h1) /\ dom ((id REAL)) &
for u being set st u in dom (<:h1,h2:>) holds (<:h1, h2:>).u = [h1.u,h2.u]
by FUNCT_3:def 8;
for i being Nat st 1<=i & i<=len f holds g/.i=r*f/.i
proof let i be Nat;assume
A7:1<=i & i<=len f; then i in Seg len f by FINSEQ_1:3;
then i in dom g by A2,A3,FINSEQ_1:def 3;
then A8:g.i=(multreal * (<:h1, h2:>)).(x.i) by A5,FUNCT_1:22;
A9:dom h2=REAL by FUNCT_1:34;
A10:dom (<:h1, h2:>)=dom h1 /\ REAL by A6,FUNCT_1:34;
A11:f.i=f/.i by A7,FINSEQ_4:24;
A12: dom h1=dom (id REAL) by FUNCOP_1:19 .=REAL by FUNCT_1:34;
then A13:(<:h1, h2:>).(x.i)=[h1.(x.i),h2.(x.i)] by A10,FUNCT_3:def 8;
A14:h1.(x.i) = r by A9,FUNCOP_1:13;
A15:h2.(x.i)=x.i by FUNCT_1:34;
(multreal * (<:h1, h2:>)).(x.i)=multreal.((<:h1, h2:>).(x.i))
by A10,A12,FUNCT_1:23;
then g.i=multreal.(r,f.i) by A1,A8,A13,A14,A15,BINOP_1:def 1;
then g.i=r*(f/.i) by A11,VECTSP_1:def 14;
hence g/.i=r*f/.i by A2,A3,A7,FINSEQ_4:24;
end;
hence thesis by A1,A2,EUCLID:2;
end;
theorem Th54: for x being Element of REAL n,f being FinSequence
st x<> 0*n & x=f holds ex i being Nat st 1<=i & i<=n & f.i<>0
proof let x be Element of REAL n,f be FinSequence;
assume A1:x<> 0*n & x=f;
then A2:len f=n by EUCLID:2;
assume A3: not ex i being Nat st 1<=i & i<=n & f.i<>0;
for z being set holds z in f iff
ex x,y st x in Seg n & y in {0} & z = [x,y]
proof let z be set;
hereby assume A4:z in f;
then consider x0,y0 being set such that
A5: z = [x0,y0] by RELAT_1:def 1;
A6:x0 in dom f by A4,A5,RELAT_1:def 4;
then A7:x0 in Seg len f by FINSEQ_1:def 3;
reconsider n1=x0 as Nat by A6;
1<=n1 & n1<=len f by A7,FINSEQ_1:3;
then A8:f.n1=0 by A2,A3;
y0=f.x0 by A4,A5,FUNCT_1:8;
then y0 in {0} by A8,TARSKI:def 1;
hence ex x,y st x in Seg n & y in {0} & z = [x,y] by A2,A5,A7;
end;
given x,y such that
A9: x in Seg n & y in {0} & z = [x,y];
A10:y=0 by A9,TARSKI:def 1;
reconsider n1=x as Nat by A9;
1<=n1 & n1<=n by A9,FINSEQ_1:3;
then x in dom f & y=f.x by A2,A3,A9,A10,FINSEQ_1:def 3;
hence z in f by A9,FUNCT_1:8;
end;
then f=[:Seg n,{0}:] by ZFMISC_1:def 2;
then f=(Seg n -->0) by FUNCOP_1:def 2;
then x=(n |-> (0 qua Real)) by A1,FINSEQ_2:def 2;
hence contradiction by A1,EUCLID:def 4;
end;
theorem Th55: for x being Element of REAL n
st n>=2 & x<> 0*n holds ex y being Element of REAL n st
not ex r being Real st y=r*x or x=r*y
proof let x be Element of REAL n;
assume A1:n>=2 & x<> 0*n;
reconsider f=x as FinSequence of REAL;
consider i2 being Nat such that
A2: 1<=i2 & i2<=n & f.i2<>0 by A1,Th54;
A3:len f=n by EUCLID:2;
then A4:1<=len f by A1,AXIOMS:22;
per cases;
suppose A5:i2>1;
reconsider g=(<*((f/.1)+1)*>)^mid(f,2,len f) as FinSequence of REAL;
A6:len g=len (<*(f/.1+1)*>) + len (mid(f,2,len f)) by FINSEQ_1:35;
A7:len (<*(f/.1+1)*>)=1 by FINSEQ_1:56;
A8:len (mid(f,2,len f))=len f-'2+1 by A1,A3,A4,JORDAN3:27
.=len f-2+1 by A1,A3,SCMFSA_7:3;
then A9:len g=1+(len f-2+1) by A6,FINSEQ_1:56
.=len f-2+(1+1) by XCMPLX_1:1
.=len f by XCMPLX_1:27;
then reconsider y2=g as Element of REAL n by A3,Th52;
now given r being Real such that A10:y2=r*x or x=r*y2;
per cases by A10;
suppose A11:y2=r*x;
A12:g/.i2=g.i2 by A2,A3,A9,FINSEQ_4:24;
A13:f/.i2=f.i2 by A2,A3,FINSEQ_4:24;
A14:1<=len f by A1,A3,AXIOMS:22;
A15:i2-'1=i2-1 by A2,SCMFSA_7:3;
A16:1<=i2-'1 by A5,JORDAN3:12;
i2<=len f-(1+1)+(1+1) by A2,A3,XCMPLX_1:27;
then i2<=len f-(1+1)+1+1 by XCMPLX_1:1;
then i2-1<=len f-(1+1)+1+1-1 by REAL_1:49;
then A17:i2-'1<=len (mid(f,2,len f)) by A8,A15,XCMPLX_1:26;
A18:i2-'1+2-'1=i2-'1+(1+1)-'1
.=i2-'1+1+1-'1 by XCMPLX_1:1
.=i2-'1+1 by BINARITH:39 .=i2-1+1 by A2,SCMFSA_7:3
.=i2 by XCMPLX_1:27;
i2<=len f-2+(1+1) by A2,A3,XCMPLX_1:27;
then 1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A5,A8,NAT_1:38,XCMPLX_1:1
;
then g.i2= (mid(f,2,len f)).(i2-1) by A7,FINSEQ_1:36
.= (mid(f,2,len f)).(i2-'1) by A2,SCMFSA_7:3
.=f.i2 by A1,A3,A14,A16,A17,A18,JORDAN3:27;
then 1 * f/.i2=r*f/.i2 by A2,A3,A11,A12,A13,Th53;
then A19:1=r by A2,A13,XCMPLX_1:5;
A20:g/.1=r*f/.1 by A11,A14,Th53;
g/.1=g.1 by A9,A14,FINSEQ_4:24;
then f/.1+1=1 * f/.1 by A19,A20,FINSEQ_1:58;
then f/.1+1-f/.1=0 by XCMPLX_1:14; hence contradiction by XCMPLX_1:26
;
suppose A21:x=r*y2;
A22:g/.i2=g.i2 by A2,A3,A9,FINSEQ_4:24;
A23:f/.i2=f.i2 by A2,A3,FINSEQ_4:24;
A24:1<=len f by A1,A3,AXIOMS:22;
A25:i2-'1=i2-1 by A2,SCMFSA_7:3;
A26:1<=i2-'1 by A5,JORDAN3:12;
i2<=len f-(1+1)+(1+1) by A2,A3,XCMPLX_1:27;
then i2<=len f-(1+1)+1+1 by XCMPLX_1:1;
then i2-1<=len f-(1+1)+1+1-1 by REAL_1:49;
then A27:i2-'1<=len (mid(f,2,len f)) by A8,A25,XCMPLX_1:26;
A28:i2-'1+2-'1=i2-'1+(1+1)-'1
.=i2-'1+1+1-'1 by XCMPLX_1:1
.=i2-'1+1 by BINARITH:39 .=i2-1+1 by A2,SCMFSA_7:3
.=i2 by XCMPLX_1:27;
i2<=len f-2+(1+1) by A2,A3,XCMPLX_1:27;
then 1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A5,A8,NAT_1:38,XCMPLX_1:1
;
then g.i2= (mid(f,2,len f)).(i2-1) by A7,FINSEQ_1:36
.= (mid(f,2,len f)).(i2-'1) by A2,SCMFSA_7:3
.=f.i2 by A1,A3,A24,A26,A27,A28,JORDAN3:27;
then 1 * f/.i2=r*f/.i2 by A2,A3,A9,A21,A22,A23,Th53;
then A29:1=r by A2,A23,XCMPLX_1:5;
A30:f/.1=r*g/.1 by A9,A21,A24,Th53;
g/.1=g.1 by A9,A24,FINSEQ_4:24;
then f/.1+1=1 * f/.1 by A29,A30,FINSEQ_1:58;
then f/.1+1-f/.1=0 by XCMPLX_1:14; hence contradiction by XCMPLX_1:26
;
end;
hence ex y being Element of REAL n st (not ex r being Real st
y=r*x or x=r*y);
suppose i2<=1;
then A31:i2=1 by A2,AXIOMS:21;
reconsider g=mid(f,1,len f-'1)^<*(f/.len f+1)*> as FinSequence of REAL;
A32:len (<*(f/.len f+1)*>)=1 by FINSEQ_1:56;
A33:len f-'1=len f-1 by A4,SCMFSA_7:3;
A34:len f-'1<=len f by JORDAN3:7;
A35:1+1-1<=len f-1 by A1,A3,REAL_1:49;
then A36:len f-'1-'1+1=len f-1-1+1 by A33,SCMFSA_7:3
.=len f-(1+1)+1 by XCMPLX_1:36;
then A37:len (mid(f,1,len f-'1))=len f-2+1
by A4,A33,A34,A35,JORDAN3:27;
A38:len (mid(f,1,len f-'1)) =len f-(1+1)+1 by A4,A33,A34,A35,A36,JORDAN3:27
.=len f-1-1+1 by XCMPLX_1:36
.=len f-1 by XCMPLX_1:27;
A39:len g=(len f-2+1)+1 by A32,A37,FINSEQ_1:35
.=len f-2+(1+1) by XCMPLX_1:1
.=len f by XCMPLX_1:27;
then reconsider y2=g as Element of REAL n by A3,Th52;
now given r being Real such that A40:y2=r*x or x=r*y2;
per cases by A40;
suppose A41:y2=r*x;
A42:g/.i2=g.i2 by A2,A3,A39,FINSEQ_4:24;
A43:f/.i2=f.i2 by A2,A3,FINSEQ_4:24;
A44:1<=len f by A1,A3,AXIOMS:22;
g.i2= (mid(f,1,len f-'1)).i2 by A31,A35,A38,JORDAN3:17
.=f.i2 by A31,A33,A34,A35,JORDAN3:32;
then 1 * f/.i2=r*f/.i2 by A2,A3,A41,A42,A43,Th53;
then A45:1=r by A2,A43,XCMPLX_1:5;
A46:g/.len f=r*f/.len f by A41,A44,Th53;
A47:g/.len f=g.len f by A39,A44,FINSEQ_4:24;
g.len f= g.(len f -1+1) by XCMPLX_1:27
.=f/.len f+1 by A38,JORDAN3:16;
then f/.len f+1-f/.len f=0 by A45,A46,A47,XCMPLX_1:14;
hence contradiction by XCMPLX_1:26;
suppose A48:x=r*y2;
A49:g/.i2=g.i2 by A2,A3,A39,FINSEQ_4:24;
A50:f/.i2=f.i2 by A2,A3,FINSEQ_4:24;
A51:1<=len f by A1,A3,AXIOMS:22;
g.i2= (mid(f,1,len f-'1)).i2 by A31,A35,A38,JORDAN3:17
.=f.(i2) by A31,A33,A34,A35,JORDAN3:32;
then 1 * f/.i2=r*f/.i2 by A2,A3,A39,A48,A49,A50,Th53;
then A52:1=r by A2,A50,XCMPLX_1:5;
A53:f/.len f=r*g/.len f by A39,A48,A51,Th53;
A54:g/.len f=g.len f by A39,A51,FINSEQ_4:24;
g.len f=g.(len f-1+1) by XCMPLX_1:27
.=f/.len f+1 by A38,JORDAN3:16;
then f/.len f+1-f/.len f=0 by A52,A53,A54,XCMPLX_1:14;
hence contradiction by XCMPLX_1:26;
end;
hence thesis;
end;
theorem Th56: for a being Real,
Q being Subset of TOP-REAL n,
w1,w7 being Point of TOP-REAL n
st n>=2 & Q={q : (|.q.|) > a } & w1 in Q & w7 in Q &
(ex r being Real st w1=r*w7 or w7=r*w1)
holds ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st
w2 in Q & w3 in Q & w4 in Q &
w5 in Q & w6 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q &
LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q
proof let a be Real,
Q be Subset of TOP-REAL n,
w1,w7 be Point of TOP-REAL n;
assume A1: n>=2 & Q={q : (|.q.|) > a } & w1 in Q & w7 in Q &
(ex r being Real st w1=r*w7 or w7=r*w1);
then consider r8 being Real such that
A2: w1=r8*w7 or w7=r8*w1;
reconsider y1=w1 as Element of REAL n by EUCLID:25;
per cases;
suppose A3:a>=0; then A4:a+1>0 by REAL_1:69;
now assume A5:w1=0.REAL n;
ex q st q=w1 & (|.q.|)>a by A1;
hence contradiction by A3,A5,TOPRNS_1:24;
end; then y1<>0*n by EUCLID:def 9;
then consider y being Element of REAL n such that
A6: (not ex r being Real st y=r*y1 or y1=r*y) by A1,Th55;
set y4=((a+1)/|.y.|)*y;
reconsider w4=y4 as Point of TOP-REAL n by EUCLID:25;
A7: |.y.|>=0 by EUCLID:12;
A8: now assume |.y.|=0;
then A9:y=0*n by EUCLID:11;
0 *y1=0 *w1 by EUCLID:def 11 .=0.REAL n by EUCLID:33
.=0*n by EUCLID:def 9;
hence contradiction by A6,A9;
end;
then A10: (a+1)/|.y.|>0 by A4,A7,REAL_2:127;
|.w4.|=|.y4.| by JGRAPH_1:def 5 .=abs((a+1)/|.y.|)*|.y.| by EUCLID:14
.= (a+1)/|.y.|*|.y.| by A10,ABSVALUE:def 1 .=a+1 by A8,XCMPLX_1:88;
then A11: |.w4.|>a by REAL_1:69;
then A12:w4 in Q by A1;
A13:now given r being Real such that
A14: w1=r*w4 or w4=r*w1;
reconsider y'=y,y1'=y1 as Element of n-tuples_on REAL by EUCLID:def 1;
y1=r*(((a+1)/|.y.|)*y) or ((a+1)/|.y.|)*y=r*y1 by A14,EUCLID:def 11;
then y1=(r*((a+1)/|.y.|))*y or
((a+1)/|.y.|)"*((a+1)/|.y.|)*y'=((a+1)/|.y.|)"*(r*y1) by RVSUM_1:71;
then y1=(r*((a+1)/|.y.|))*y or
((a+1)/|.y.|)"*((a+1)/|.y.|)*y=((a+1)/|.y.|)"*r*y1'
by RVSUM_1:71;
then y1=(r*((a+1)/|.y.|))*y' or 1 *y=((a+1)/|.y.|)"*r*y1
by A10,XCMPLX_0:def 7;
then A15: y1=(r*((a+1)/|.y.|))*y or y'=((a+1)/|.y.|)"*r*y1 by RVSUM_1:74;
per cases by A15;
suppose y1=(r*((a+1)/|.y.|))*y; hence contradiction by A6;
suppose y=((a+1)/|.y.|)"*r*y1; hence contradiction by A6;
end;
then consider w2,w3 being Point of TOP-REAL n such that
A16: w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q by A1,A12,Th49;
now given r1 being Real such that
A17: w4=r1*w7 or w7=r1*w4;
A18:now assume r1=0;
then A19:w4=0.REAL n or w7=0.REAL n by A17,EUCLID:33;
ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1;
hence contradiction by A3,A11,A19,TOPRNS_1:24;
end;
per cases by A2;
suppose A20: w1=r8*w7;
now per cases by A17;
case w4=r1*w7;
then r1"*w4=r1"*r1*w7 by EUCLID:34;
then r1"*w4=1 *w7 by A18,XCMPLX_0:def 7;
then r1"*w4=w7 by EUCLID:33;
then w1=r8*r1"*w4 by A20,EUCLID:34;
hence contradiction by A13;
case w7=r1*w4;
then r1"*w7=r1"*r1*w4 by EUCLID:34;
then r1"*w7=1 *w4 by A18,XCMPLX_0:def 7;
then r1"*w7=w4 by EUCLID:33;
then r1""*w4=r1""*r1"*w7 by EUCLID:34;
then r1""*w4=1 *w7 by A18,XCMPLX_0:def 7;
then r1""*w4=w7 by EUCLID:33;
then w1=r8*r1""*w4 by A20,EUCLID:34;
hence contradiction by A13;
end;
hence contradiction;
suppose A21: w7=r8*w1;
then A22:r8"*w7=r8"*r8*w1 by EUCLID:34;
now assume r8=0;
then A23: w7=0.REAL n by A21,EUCLID:33;
ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1;
hence contradiction by A3,A23,TOPRNS_1:24;
end;
then r8"*w7=1 *w1 by A22,XCMPLX_0:def 7;
then A24:r8"*w7=w1 by EUCLID:33;
now per cases by A17;
case w4=r1*w7;
then r1"*w4=r1"*r1*w7 by EUCLID:34;
then r1"*w4=1 *w7 by A18,XCMPLX_0:def 7;
then r1"*w4=w7 by EUCLID:33;
then w1=r8"*r1"*w4 by A24,EUCLID:34;
hence contradiction by A13;
case w7=r1*w4;
then r1"*w7=r1"*r1*w4 by EUCLID:34;
then r1"*w7=1 *w4 by A18,XCMPLX_0:def 7;
then r1"*w7=w4 by EUCLID:33;
then r1""*w4=r1""*r1"*w7 by EUCLID:34;
then r1""*w4=1 *w7 by A18,XCMPLX_0:def 7;
then r1""*w4=w7 by EUCLID:33;
then w1=r8"*r1""*w4 by A24,EUCLID:34;
hence contradiction by A13;
end;
hence contradiction;
end;
then consider w2',w3' being Point of TOP-REAL n such that
A25: w2' in Q & w3' in Q &
LSeg(w4,w2') c=Q & LSeg(w2',w3') c= Q & LSeg(w3',w7) c= Q
by A1,A12,Th49;
thus thesis by A12,A16,A25;
suppose A26:a<0;
A27:the carrier of TOP-REAL n=REAL n by EUCLID:25;
REAL n c= Q
proof let x be set;assume x in REAL n;
then reconsider w=x as Point of TOP-REAL n by EUCLID:25;
|.w.|>=0 by TOPRNS_1:26;
hence x in Q by A1,A26;
end;
then A28:Q=the carrier of TOP-REAL n by A27,XBOOLE_0:def 10;
set w2=0.REAL n;
A29:LSeg(w1,w2) c=Q by A28;
LSeg(w2,w7) c=Q by A28;
hence ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st
w2 in Q & w3 in Q & w4 in Q &
w5 in Q & w6 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q &
LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q by A28,A29;
end;
theorem Th57: for a being Real,
Q being Subset of TOP-REAL n,
w1,w7 being Point of TOP-REAL n
st n>=2 & Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w7 in Q &
(ex r being Real st w1=r*w7 or w7=r*w1)
holds ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st
w2 in Q & w3 in Q & w4 in Q &
w5 in Q & w6 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q &
LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q
proof let a be Real,
Q be Subset of TOP-REAL n,
w1,w7 be Point of TOP-REAL n;
assume A1: n>=2 & Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w7 in Q &
(ex r being Real st w1=r*w7 or w7=r*w1);
then consider r8 being Real such that
A2: w1=r8*w7 or w7=r8*w1;
reconsider y1=w1 as Element of REAL n by EUCLID:25;
per cases;
suppose A3:a>0;
now assume w1=0.REAL n;
then |.w1.|=0 by TOPRNS_1:24;
then w1 in {q : (|.q.|) < a } by A3;
hence contradiction by A1,XBOOLE_0:def 4;
end; then y1<>0*n by EUCLID:def 9;
then consider y being Element of REAL n such that
A4: (not ex r being Real st y=r*y1 or y1=r*y) by A1,Th55;
set y4=(a/|.y.|)*y;
reconsider w4=y4 as Point of TOP-REAL n by EUCLID:25;
A5: |.y.|>=0 by EUCLID:12;
A6: now assume |.y.|=0;
then A7:y=0*n by EUCLID:11;
0 *y1=0 *w1 by EUCLID:def 11 .=0.REAL n by EUCLID:33
.=0*n by EUCLID:def 9;
hence contradiction by A4,A7;
end;
then A8: a/|.y.|>0 by A3,A5,REAL_2:127;
A9: |.w4.|=|.y4.| by JGRAPH_1:def 5 .=abs(a/|.y.|)*|.y.| by EUCLID:14
.= a/|.y.|*|.y.| by A8,ABSVALUE:def 1 .=a by A6,XCMPLX_1:88;
A10:now assume w4 in {q : (|.q.|) < a };
then ex q st q=w4 & (|.q.|) < a;
hence contradiction by A9;
end;
then A11:w4 in Q by A1,XBOOLE_0:def 4;
A12:now given r being Real such that
A13: w1=r*w4 or w4=r*w1;
reconsider y'=y,y1'=y1 as Element of n-tuples_on REAL by EUCLID:def 1;
y1=r*((a/|.y.|)*y) or (a/|.y.|)*y=r*y1 by A13,EUCLID:def 11;
then y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y'=(a/|.y.|)"*(r*y1)
by RVSUM_1:71;
then y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y=(a/|.y.|)"*r*y1'
by RVSUM_1:71;
then y1=(r*(a/|.y.|))*y' or 1 *y=(a/|.y.|)"*r*y1
by A8,XCMPLX_0:def 7;
then A14: y1=(r*(a/|.y.|))*y or y'=(a/|.y.|)"*r*y1 by RVSUM_1:74;
per cases by A14;
suppose y1=(r*(a/|.y.|))*y;
hence contradiction by A4;
suppose y=(a/|.y.|)"*r*y1;
hence contradiction by A4;
end;
then consider w2,w3 being Point of TOP-REAL n such that
A15: w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q
by A1,A11,Th50;
now given r1 being Real such that
A16: w4=r1*w7 or w7=r1*w4;
A17:now assume r1=0;
then w4=0.REAL n or w7=0.REAL n by A16,EUCLID:33;
then |.w4.|=0 or |.w7.|=0 by TOPRNS_1:24;
then w4 in {q : (|.q.|) < a } or
w7 in {q2 where q2 is Point of TOP-REAL n: (|.q2.|) < a } by A3;
hence contradiction by A1,A10,XBOOLE_0:def 4;
end;
now per cases by A2;
case A18: w1=r8*w7;
now per cases by A16;
case w4=r1*w7;
then r1"*w4=r1"*r1*w7 by EUCLID:34;
then r1"*w4=1 *w7 by A17,XCMPLX_0:def 7;
then r1"*w4=w7 by EUCLID:33;
then w1=r8*r1"*w4 by A18,EUCLID:34;
hence contradiction by A12;
case w7=r1*w4;
then r1"*w7=r1"*r1*w4 by EUCLID:34;
then r1"*w7=1 *w4 by A17,XCMPLX_0:def 7;
then r1"*w7=w4 by EUCLID:33;
then r1""*w4=r1""*r1"*w7 by EUCLID:34;
then r1""*w4=1 *w7 by A17,XCMPLX_0:def 7;
then r1""*w4=w7 by EUCLID:33;
then w1=r8*r1""*w4 by A18,EUCLID:34;
hence contradiction by A12;
end;
hence contradiction;
case A19: w7=r8*w1;
then A20:r8"*w7=r8"*r8*w1 by EUCLID:34;
now assume r8=0;
then w7=0.REAL n by A19,EUCLID:33;
then |.w7.|=0 by TOPRNS_1:24;
then w7 in {q : (|.q.|) < a } by A3;
hence contradiction by A1,XBOOLE_0:def 4;
end;
then r8"*w7=1 *w1 by A20,XCMPLX_0:def 7;
then A21:r8"*w7=w1 by EUCLID:33;
now per cases by A16;
case w4=r1*w7;
then r1"*w4=r1"*r1*w7 by EUCLID:34;
then r1"*w4=1 *w7 by A17,XCMPLX_0:def 7;
then r1"*w4=w7 by EUCLID:33;
then w1=r8"*r1"*w4 by A21,EUCLID:34;
hence contradiction by A12;
case w7=r1*w4;
then r1"*w7=r1"*r1*w4 by EUCLID:34;
then r1"*w7=1 *w4 by A17,XCMPLX_0:def 7;
then r1"*w7=w4 by EUCLID:33;
then r1""*w4=r1""*r1"*w7 by EUCLID:34;
then r1""*w4=1 *w7 by A17,XCMPLX_0:def 7;
then r1""*w4=w7 by EUCLID:33;
then w1=r8"*r1""*w4 by A21,EUCLID:34;
hence contradiction by A12;
end;
hence contradiction;
end;
hence contradiction;
end;
then consider w2',w3' being Point of TOP-REAL n such that
A22: w2' in Q & w3' in Q &
LSeg(w4,w2') c=Q & LSeg(w2',w3') c= Q & LSeg(w3',w7) c= Q
by A1,A11,Th50;
thus thesis by A11,A15,A22;
suppose A23:a<=0;
A24:the carrier of TOP-REAL n=REAL n by EUCLID:25;
REAL n c= Q
proof let x be set;assume A25:x in REAL n;
now assume x in {q : (|.q.|) < a };
then consider q being Point of TOP-REAL n such that
A26:q=x & (|.q.|) < a;
thus contradiction by A23,A26,TOPRNS_1:26;
end;
hence x in Q by A1,A25,XBOOLE_0:def 4;
end;
then A27:Q=the carrier of TOP-REAL n by A24,XBOOLE_0:def 10;
set w2=0.REAL n;
A28:LSeg(w1,w2) c=Q by A27;
LSeg(w2,w7) c=Q by A27;
hence thesis by A27,A28;
end;
theorem Th58:for a being Real st n>=1 holds {q: |.q.| >a} <>{}
proof let a be Real;assume A1:n>=1;
now assume not (a+1)*(1.REAL n) in {q : |.q.| > a };
then A2: |.(a+1)*(1.REAL n).|<=a;
A3: |.(a+1)*(1.REAL n).|=abs(a+1)*|.(1.REAL n).| by TOPRNS_1:8
.=abs(a+1)*(sqrt n) by Th37;
A4:abs(a+1)>=0 by ABSVALUE:5;
sqrt 1<=sqrt n by A1,SQUARE_1:94;
then A5: abs(a+1)*1<=abs(a+1)*sqrt n by A4,AXIOMS:25,SQUARE_1:83;
a+1<=abs(a+1) by ABSVALUE:11;
then A6:a+1<= |.(a+1)*(1.REAL n).| by A3,A5,AXIOMS:22;
a<a+1 by REAL_1:69;
hence contradiction by A2,A6,AXIOMS:22;
end;
hence thesis;
end;
theorem Th59: for a being Real,
P being Subset of TOP-REAL n st n>=2 & P={q : |.q.| > a }
holds P is connected
proof let a be Real,
P be Subset of TOP-REAL n;
assume A1:n>=2 & P={q : |.q.| > a };
then n>=1 by AXIOMS:22;
then reconsider Q=P as non empty Subset of TOP-REAL n by A1,Th58;
for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7
ex f being map of I[01],((TOP-REAL n)|Q) st f is continuous &
w1=f.0 & w7=f.1
proof let w1,w7 be Point of TOP-REAL n;
assume A2:w1 in Q & w7 in Q & w1<>w7;
per cases;
suppose not (ex r being Real st w1=r*w7 or w7=r*w1);
then consider w2,w3 being Point of TOP-REAL n such that
A3: w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w7) c= Q
by A1,A2,Th49;
thus ex h being map of I[01],(TOP-REAL n)|Q st h is continuous
& w1=h.0 & w7=h.1 by A2,A3,Th45;
suppose (ex r being Real st w1=r*w7 or w7=r*w1);
then consider w2,w3,w4,w5,w6 being Point of TOP-REAL n such that
A4:w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q
& LSeg(w4,w5) c= Q &
LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q by A1,A2,Th56;
thus thesis by A2,A4,Th46;
end;
hence P is connected by JORDAN1:5;
end;
theorem Th60:for a being Real st n>=1 holds
(REAL n) \ {q: |.q.| < a} <> {}
proof let a be Real;assume A1:n>=1;
A2:{q:(|.q.|)>a} c= (REAL n)\{q2:(|.q2.|)<a}
proof let x be set;assume x in {q:(|.q.|)>a};
then consider q such that A3:q=x & (|.q.|)>a;
not (|.q.|)<a & q in the carrier of TOP-REAL n by A3;
then A4:not (|.q.|)<a & q in REAL n by EUCLID:25;
now assume x in {q2:(|.q2.|)<a};
then ex q2 st q2=x & (|.q2.|)<a;
hence contradiction by A3;
end;
hence thesis by A3,A4,XBOOLE_0:def 4;
end;
{q:(|.q.|)>a} <>{} by A1,Th58;
hence thesis by A2,XBOOLE_1:3;
end;
theorem Th61: for a being Real,P being Subset of TOP-REAL n
st n>=2 & P=(REAL n)\ {q : |.q.| < a }
holds P is connected
proof let a be Real,
P be Subset of TOP-REAL n;
assume A1:n>=2 & P=(REAL n)\ {q : |.q.| < a };
then n>=1 by AXIOMS:22;
then reconsider Q=P as non empty Subset of TOP-REAL n by A1,Th60;
for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7
ex f being map of I[01],((TOP-REAL n)|Q) st f is continuous &
w1=f.0 & w7=f.1
proof let w1,w7 be Point of TOP-REAL n;
assume A2:w1 in Q & w7 in Q & w1<>w7;
per cases;
suppose not (ex r being Real st w1=r*w7 or w7=r*w1);
then consider w2,w3 being Point of TOP-REAL n such that
A3: w2 in Q & w3 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w7) c= Q
by A1,A2,Th50;
thus thesis by A2,A3,Th45;
suppose (ex r being Real st w1=r*w7 or w7=r*w1);
then consider w2,w3,w4,w5,w6 being Point of TOP-REAL n such that
A4:w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q &
LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q
& LSeg(w4,w5) c= Q &
LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q by A1,A2,Th57;
consider f1 being map of I[01],((TOP-REAL n)|Q)
such that A5:f1 is continuous &
w1=f1.0 & w7=f1.1 by A2,A4,Th46;
thus thesis by A5;
end;
hence P is connected by JORDAN1:5;
end;
theorem Th62: for a being Real,n being Nat,
P being Subset of TOP-REAL n
st n>=1 & P=(REAL n)\ {q where q is Point of TOP-REAL n: |.q.| < a }
holds not P is Bounded
proof let a be Real,n be Nat,P be Subset of TOP-REAL n;
assume A1:n>=1 &
P=(REAL n)\ {q where q is Point of TOP-REAL n : |.q.| < a };
per cases;
suppose A2:a>0;
now assume P is Bounded;
then consider r being Real such that
A3: for q being Point of TOP-REAL n st
q in P holds |.q.|<r by Th40;
consider p being Element of P;
A4:P<>{} by A1,Th60;
then p in P;
then reconsider p as Point of TOP-REAL n;
A5: |.p.|<r by A3,A4;
A6: 0 <= (|.p.|) by TOPRNS_1:26;
now assume not (a+r+1)*(1.REAL n) in (REAL n)
\{q where q is Point of TOP-REAL n: (|.q.|) < a };
then A7:not ((a+r+1)*(1.REAL n) in (REAL n) & not
(a+r+1)*(1.REAL n) in
{q where q is Point of TOP-REAL n : (|.q.|) < a }) by XBOOLE_0:def 4;
(a+r+1)*(1.REAL n) in the carrier of TOP-REAL n;
then consider q being Point of TOP-REAL n such that
A8:q= (a+r+1)*(1.REAL n) & (|.q.|) < a by A7,EUCLID:25;
A9: |.(a+r+1)*(1.REAL n).|=abs(a+r+1)*|.(1.REAL n).| by TOPRNS_1:8
.=abs(a+r+1)*(sqrt n) by Th37;
A10:abs(a+r+1)>=0 by ABSVALUE:5;
sqrt 1<=sqrt n by A1,SQUARE_1:94;
then A11: abs(a+r+1)*1<=abs(a+r+1)*sqrt n by A10,AXIOMS:25,SQUARE_1:83;
a+r+1<=abs(a+r+1) by ABSVALUE:11;
then A12:a+r+1<= |.(a+r+1)*(1.REAL n).| by A9,A11,AXIOMS:22;
A13:a+r<a+r+1 by REAL_1:69;
a<a+r by A5,A6,REAL_1:69;
then a<a+r+1 by A13,AXIOMS:22;
hence contradiction by A8,A12,AXIOMS:22;
end;
then A14:(|.((a+r+1)*(1.REAL n)).|)<=r by A1,A3;
A15: |.(a+r+1)*(1.REAL n).|
=abs(a+r+1)*|.(1.REAL n).| by TOPRNS_1:8
.=abs(a+r+1)*(sqrt n) by Th37;
A16:abs(a+r+1)>=0 by ABSVALUE:5;
sqrt 1<=sqrt n by A1,SQUARE_1:94;
then A17: abs(a+r+1)*1<=abs(a+r+1)*sqrt n by A16,AXIOMS:25,SQUARE_1:83;
a+r+1<=abs(a+r+1) by ABSVALUE:11;
then A18: a+r+1<= |.(a+r+1)*(1.REAL n).| by A15,A17,AXIOMS:22;
a+r<a+r+1 by REAL_1:69;
then A19:a+r<|.((a+r+1)*(1.REAL n)).| by A18,AXIOMS:22;
r<r+a by A2,REAL_1:69;
hence contradiction by A14,A19,AXIOMS:22;
end;
hence not P is Bounded;
suppose A20:a<=0;
now assume
A21:{q where q is Point of TOP-REAL n: (|.q.|) < a }<>{};
{q where q is Point of TOP-REAL n: (|.q.|) < a }
c= the carrier of TOP-REAL n
proof let z;assume z in
{q where q is Point of TOP-REAL n: (|.q.|) < a };
then consider q being Point of TOP-REAL n such that
A22:q=z & (|.q.|) < a;
thus z in the carrier of TOP-REAL n by A22;
end;
then reconsider
Q={q where q is Point of TOP-REAL n: (|.q.|) < a }
as Subset of TOP-REAL n;
consider d being Element of Q;
d in {q where q is Point of TOP-REAL n: (|.q.|) < a } by A21;
then consider q being Point of TOP-REAL n such that
A23:q=d & (|.q.|) < a;
thus contradiction by A20,A23,TOPRNS_1:26;
end;
then P=the carrier of TOP-REAL n by A1,EUCLID:25;
then P=[#](TOP-REAL n) by PRE_TOPC:12;
hence not P is Bounded by A1,Th41;
end;
theorem Th63: for a being Real,P being Subset of TOP-REAL 1
st P={q where q is Point of TOP-REAL 1:
ex r st q=<*r*> & r > a } holds P is convex
proof let a be Real,P be Subset of TOP-REAL 1;
assume A1:P={q where q is Point of TOP-REAL 1: ex r st q=<*r*> & r > a };
for w1,w2 being Point of TOP-REAL 1
st w1 in P & w2 in P holds LSeg(w1,w2) c= P
proof let w1,w2 be Point of TOP-REAL 1;
assume A2:w1 in P & w2 in P;
then consider q1 being Point of TOP-REAL 1 such that
A3:q1=w1 & ex r st q1=<*r*> & r > a by A1;
consider r1 such that A4: q1=<*r1*> & r1 > a by A3;
consider q2 being Point of TOP-REAL 1 such that
A5:q2=w2 & ex r st q2=<*r*> & r > a by A1,A2;
consider r2 such that A6: q2=<*r2*> & r2 > a by A5;
thus LSeg(w1,w2) c= P
proof let x be set;assume x in LSeg(w1,w2);
then x in {(1-r)*w1+r*w2 : 0<=r & r<=1} by TOPREAL1:def 4;
then consider r3 being Real such that
A7: x=(1-r3)*w1+r3*w2 & (0<=r3 & r3<=1);
A8:1-r3>=0 by A7,SQUARE_1:12;
per cases;
suppose A9:r3>0;
A10:(1-r3)*r1>=(1-r3)*a by A4,A8,AXIOMS:25;
A11: r3*r2>r3*a by A6,A9,REAL_1:70;
(1-r3)*a+r3*a=((1-r3)+r3)*a by XCMPLX_1:8 .=1 *a by XCMPLX_1:27 .=a;
then A12:(1-r3)*r1+r3*r2>a by A10,A11,REAL_1:67;
A13:<*(1-r3)*r1+r3*r2*>=|[(1-r3)*r1+r3*r2]| by JORDAN2B:def 2
.=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:27
.=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:26
.=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:26;
A14: |[r1]|=w1 by A3,A4,JORDAN2B:def 2;
|[r2]|=w2 by A5,A6,JORDAN2B:def 2;
hence x in P by A1,A7,A12,A13,A14;
suppose r3<=0; then r3=0 by A7;
then x=w1+0 *w2 by A7,EUCLID:33
.=w1+0.REAL 1 by EUCLID:33 .=w1 by EUCLID:31;
hence x in P by A2;
end;
end;
hence P is convex by JORDAN1:def 1;
end;
theorem Th64: for a being Real,P being Subset of TOP-REAL 1
st P={q where q is Point of TOP-REAL 1 :
ex r st q=<*r*> & r < -a } holds P is convex
proof let a be Real,P be Subset of TOP-REAL 1;
assume A1:P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a };
for w1,w2 being Point of TOP-REAL 1
st w1 in P & w2 in P holds LSeg(w1,w2) c= P
proof let w1,w2 be Point of TOP-REAL 1;
assume A2:w1 in P & w2 in P;
then consider q1 being Point of TOP-REAL 1 such that
A3:q1=w1 & ex r st q1=<*r*> & r < -a by A1;
consider r1 such that A4: q1=<*r1*> & r1 < -a by A3;
consider q2 being Point of TOP-REAL 1 such that
A5:q2=w2 & ex r st q2=<*r*> & r < -a by A1,A2;
consider r2 such that A6: q2=<*r2*> & r2 < -a by A5;
thus LSeg(w1,w2) c= P
proof let x be set;assume x in LSeg(w1,w2);
then x in {(1-r)*w1+r*w2 : 0<=r & r<=1} by TOPREAL1:def 4;
then consider r3 being Real such that
A7: x=(1-r3)*w1+r3*w2 & (0<=r3 & r3<=1);
A8:1-r3>=0 by A7,SQUARE_1:12;
per cases;
suppose A9:r3>0;
A10:(1-r3)*r1<=(1-r3)*(-a) by A4,A8,AXIOMS:25;
A11: r3*r2<r3*(-a) by A6,A9,REAL_1:70;
(1-r3)*(-a)+r3*(-a)=((1-r3)+r3)*(-a) by XCMPLX_1:8
.=1 *(-a) by XCMPLX_1:27 .=-a;
then A12:(1-r3)*r1+r3*r2< -a by A10,A11,REAL_1:67;
A13:<*(1-r3)*r1+r3*r2*>=|[(1-r3)*r1+r3*r2]| by JORDAN2B:def 2
.=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:27
.=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:26
.=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:26;
A14: |[r1]|=w1 by A3,A4,JORDAN2B:def 2;
|[r2]|=w2 by A5,A6,JORDAN2B:def 2;
hence x in P by A1,A7,A12,A13,A14;
suppose r3<=0; then r3=0 by A7;
then x=w1+0 *w2 by A7,EUCLID:33
.=w1+0.REAL 1 by EUCLID:33 .=w1 by EUCLID:31;
hence x in P by A2;
end;
end;
hence P is convex by JORDAN1:def 1;
end;
theorem Th65: for a being Real,P being Subset of TOP-REAL 1
st P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }
holds P is connected
proof let a be Real,P be Subset of TOP-REAL 1;
assume P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a };
then P is convex by Th63;
hence thesis by Th14;
end;
theorem Th66: for a being Real,P being Subset of TOP-REAL 1
st P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }
holds P is connected
proof let a be Real,P be Subset of TOP-REAL 1;
assume P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a };
then P is convex by Th64;
hence P is connected by Th14;
end;
theorem Th67: for W being Subset of Euclid 1,a being Real,
P being Subset of TOP-REAL 1
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }
& P=W holds P is connected & W is not bounded
proof let W be Subset of Euclid 1,a be Real,
P be Subset of TOP-REAL 1;
assume
A1:W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a } & P=W;
hence P is connected by Th65;
now assume W is bounded;
then consider r such that
A2: 0<r & for x,y being Point of Euclid 1 st
x in W & y in W holds dist(x,y)<=r by TBSP_1:def 9;
A3:a<=abs(a) by ABSVALUE:11;
A4:abs(a)>=0 by ABSVALUE:5;
then abs(a)+abs(a)>=0+abs(a) by AXIOMS:24;
then abs(a)+abs(a)+abs(a)>=0+abs(a) by A4,AXIOMS:24;
then A5:3*abs(a)>=abs(a) by XCMPLX_1:12;
3*r>0 by A2,REAL_2:122;
then 0+abs(a)<3*r+3*abs(a) by A5,REAL_1:67;
then abs(a)<3*(r+abs(a)) by XCMPLX_1:8;
then A6:a<3*(r+abs(a)) by A3,AXIOMS:22;
reconsider p3=<*1 qua Real*> as Element of 1-tuples_on REAL;
reconsider p4=p3 as Element of REAL 1 by EUCLID:def 1;
(3*(r+abs(a)))*(1.REAL 1)=(3*(r+abs(a)))*p4 by Th36,EUCLID:def 11
.=<*((3*(r+abs(a)))*1)*> by RVSUM_1:69;
then A7: (3*(r+abs(a)))*(1.REAL 1) in W by A1,A6;
then reconsider z1=(3*(r+abs(a)))*(1.REAL 1) as Point of Euclid 1;
A8:a<=abs(a) by ABSVALUE:11;
0+abs(a)<r+abs(a) by A2,REAL_1:53;
then A9:a<r+abs(a) by A8,AXIOMS:22;
(r+abs(a))*(1.REAL 1)=(r+abs(a))*p4 by Th36,EUCLID:def 11
.=<*((r+abs(a))*1)*> by RVSUM_1:69;
then A10: (r+abs(a))*(1.REAL 1) in W by A1,A9;
then reconsider z2=(r+abs(a))*(1.REAL 1) as Point of Euclid 1;
0<=abs(a) by ABSVALUE:5;
then A11: r+0<=r+abs(a) by AXIOMS:24;
then A12: 0<r+abs(a) by A2;
dist(z1,z2)=|.(3*(r+abs(a)))*(1.REAL 1)-((r+abs(a))*(1.REAL 1)).|
by JGRAPH_1:45
.=|.(3*(r+abs(a))-(r+abs(a)))*(1.REAL 1).| by EUCLID:54
.=|.((r+abs(a))+(r+abs(a))+(r+abs(a))-(r+abs(a)))*(1.REAL 1).|
by XCMPLX_1:12
.=|.((r+abs(a))+(r+abs(a)))*(1.REAL 1).|
by XCMPLX_1:26
.=abs((r+abs(a))+(r+abs(a)))*|.(1.REAL 1).| by TOPRNS_1:8
.=abs((r+abs(a))+(r+abs(a)))*(sqrt 1) by Th37;
then A13: (r+abs(a))+(r+abs(a))<= dist(z1,z2) by ABSVALUE:11,SQUARE_1:83;
(r+abs(a))+0<(r+abs(a))+(r+abs(a)) by A12,REAL_1:53;
then (r+abs(a))<dist(z1,z2) by A13,AXIOMS:22;
then r<dist(z1,z2) by A11,AXIOMS:22;
hence contradiction by A2,A7,A10;
end;
hence W is not bounded;
end;
theorem Th68: for W being Subset of Euclid 1,a being Real,
P being Subset of TOP-REAL 1
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }
& P=W holds P is connected & W is not bounded
proof let W be Subset of Euclid 1,a be Real,
P be Subset of TOP-REAL 1; assume
A1:W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } & P=W;
hence P is connected by Th66;
assume W is bounded;
then consider r such that
A2: 0<r & for x,y being Point of Euclid 1 st
x in W & y in W holds dist(x,y)<=r by TBSP_1:def 9;
A3:a<=abs(a) by ABSVALUE:11;
A4:abs(a)>=0 by ABSVALUE:5;
then abs(a)+abs(a)>=0+abs(a) by AXIOMS:24;
then abs(a)+abs(a)+abs(a)>=0+abs(a) by A4,AXIOMS:24;
then A5:3*abs(a)>=abs(a) by XCMPLX_1:12;
3*r>0 by A2,REAL_2:122;
then 0+abs(a)<3*r+3*abs(a) by A5,REAL_1:67;
then abs(a)<3*(r+abs(a)) by XCMPLX_1:8;
then a<3*(r+abs(a)) by A3,AXIOMS:22;
then A6: -a> -(3*(r+abs(a))) by REAL_1:50;
reconsider p3=<*1 qua Real*> as Element of 1-tuples_on REAL;
reconsider p4=p3 as Element of REAL 1 by EUCLID:def 1;
(-3*(r+abs(a)))*(1.REAL 1)=(-3*(r+abs(a)))*p4 by Th36,EUCLID:def 11
.=<*((-3*(r+abs(a)))*1)*> by RVSUM_1:69;
then A7: (-3*(r+abs(a)))*(1.REAL 1) in {q where q is Point of TOP-REAL 1:
ex r st q=<*r*> & r< -a } by A6;
then reconsider z1=(-3*(r+abs(a)))*(1.REAL 1) as Point of Euclid 1 by A1;
A8:a<=abs(a) by ABSVALUE:11;
0+abs(a)<r+abs(a) by A2,REAL_1:53;
then a<r+abs(a) by A8,AXIOMS:22;
then A9: -a> -(r+abs(a)) by REAL_1:50;
(-(r+abs(a)))*(1.REAL 1)=(-(r+abs(a)))*p4 by Th36,EUCLID:def 11
.=<* (-(r+abs(a)))*1 *> by RVSUM_1:69;
then A10: (-(r+abs(a)))*(1.REAL 1) in W by A1,A9;
then reconsider z2=(-(r+abs(a)))*(1.REAL 1) as Point of Euclid 1;
0<=abs(a) by ABSVALUE:5;
then A11: r+0<=r+abs(a) by AXIOMS:24;
then A12: 0<r+abs(a) by A2;
dist(z1,z2)=|.(-3*(r+abs(a)))*(1.REAL 1)-(-(r+abs(a)))*(1.REAL 1).|
by JGRAPH_1:45
.=|.(-3*(r+abs(a))--(r+abs(a)))*(1.REAL 1).| by EUCLID:54
.=|.-((-3*(r+abs(a))--(r+abs(a)))*(1.REAL 1)).| by TOPRNS_1:27
.=|.(-(-3*(r+abs(a))--(r+abs(a))))*(1.REAL 1).| by EUCLID:44
.=|.(-(-3*(r+abs(a))+--(r+abs(a))))*(1.REAL 1).| by XCMPLX_0:def 8
.=|.(-(-3*(r+abs(a)))-(r+abs(a)))*(1.REAL 1).| by XCMPLX_1:161
.=|.((r+abs(a))+(r+abs(a))+(r+abs(a))-(r+abs(a)))*(1.REAL 1).|
by XCMPLX_1:12
.=|.((r+abs(a))+(r+abs(a)))*(1.REAL 1).| by XCMPLX_1:26
.=abs((r+abs(a))+(r+abs(a)))*|.(1.REAL 1).| by TOPRNS_1:8
.=abs((r+abs(a))+(r+abs(a)))*(sqrt 1) by Th37;
then A13: (r+abs(a))+(r+abs(a))<= dist(z1,z2) by ABSVALUE:11,SQUARE_1:83;
(r+abs(a))+0<(r+abs(a))+(r+abs(a)) by A12,REAL_1:53;
then (r+abs(a))<dist(z1,z2) by A13,AXIOMS:22;
then r<dist(z1,z2) by A11,AXIOMS:22;
hence contradiction by A1,A2,A7,A10;
end;
theorem Th69: for W being Subset of Euclid n,a being Real,
P being Subset of TOP-REAL n st n>=2 & W={q : |.q.| > a }
& P=W holds P is connected & W is not bounded
proof let W be Subset of Euclid n,a be Real,
P be Subset of TOP-REAL n;
assume A1:n>=2 & W={q : |.q.| > a } & P=W;
hence P is connected by Th59;
assume W is bounded;
then consider r such that
A2: 0<r & for x,y being Point of Euclid n st
x in W & y in W holds dist(x,y)<=r by TBSP_1:def 9;
A3: |.(r+abs(a))*(1.REAL n).|=abs(r+abs(a))*|.(1.REAL n).| by TOPRNS_1:8
.=abs(r+abs(a))*(sqrt n) by Th37;
A4:abs(r+abs(a))>=0 by ABSVALUE:5;
A5: 1<=n by A1,AXIOMS:22;
then A6: 1<=sqrt n by SQUARE_1:83,94;
then A7: abs(r+abs(a))*1<=abs(r+abs(a))*sqrt n by A4,AXIOMS:25;
(r+abs(a))<=abs(r+abs(a)) by ABSVALUE:11;
then A8:(r+abs(a))<= |.(r+abs(a))*(1.REAL n).| by A3,A7,AXIOMS:22;
A9:a<=abs(a) by ABSVALUE:11;
abs(a)<r+abs(a) by A2,REAL_1:69;
then A10: a<r+abs(a) by A9,AXIOMS:22;