:: Bounded Domains and Unbounded Domains
:: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski
::
:: Received January 7, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, XXREAL_0, CARD_1, COMPLEX1, ARYTM_1,
ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC, EUCLID, RVSUM_1,
SQUARE_1, XBOOLE_0, RELAT_2, TARSKI, STRUCT_0, NAT_1, XXREAL_2, CONNSP_1,
METRIC_1, CONVEX1, CONNSP_3, ZFMISC_1, SETFAM_1, RLTOPSP1, FINSEQ_2,
SUPINF_2, BORSUK_1, XXREAL_1, BORSUK_2, GRAPH_1, TOPMETR, TREAL_1,
VALUED_1, FUNCT_4, RCOMP_1, TOPREAL1, TOPS_2, PCOMPS_1, WEIERSTR, SEQ_4,
PARTFUN1, FUNCOP_1, BINOP_2, ORDINAL4, JORDAN3, TBSP_1, CONNSP_2,
RUSUB_4, SPPOL_1, GOBOARD2, SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1,
MCART_1, MATRIX_1, GOBOARD9, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2,
JORDAN2C;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RVSUM_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_2, COMPLEX1, SEQM_3, PRE_TOPC, TOPS_1, TOPS_2,
COMPTS_1, METRIC_1, BINOP_2, PCOMPS_1, CONNSP_1, CONNSP_2, TBSP_1,
CONNSP_3, TOPMETR, RCOMP_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, STRUCT_0,
SQUARE_1, BORSUK_2, XXREAL_0, SEQ_4, FINSEQ_6, FUNCOP_1, FUNCT_3,
TREAL_1, FUNCT_4, RLVECT_1, RUSUB_4, RLTOPSP1, CONVEX1, EUCLID, SPPOL_1,
PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1, MATRIX_0, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD9, JORDAN2B, REAL_1, NAT_1, NAT_D, WEIERSTR, FINSOP_1;
constructors REAL_1, SQUARE_1, FINSEQOP, RCOMP_1, FINSOP_1, TOPS_1, CONNSP_1,
TOPS_2, COMPTS_1, TBSP_1, MONOID_0, TREAL_1, GOBOARD2, SPPOL_1, JORDAN1,
PSCOMP_1, WEIERSTR, BORSUK_2, GOBOARD9, CONNSP_3, JORDAN2B, SPRECT_1,
SPRECT_2, BINOP_2, GOBOARD1, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, RUSUB_4,
SETWISEO, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1,
NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC,
TOPS_1, METRIC_1, BORSUK_1, TBSP_1, EUCLID, TOPMETR, GOBOARD2, JORDAN1,
BORSUK_2, SPRECT_1, SPRECT_3, VALUED_0, RLTOPSP1, JORDAN2B, MONOID_0,
SEQ_4, SPPOL_1, CARD_1, NAT_1, SQUARE_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, TOPS_2, TBSP_1, RLTOPSP1, XXREAL_2;
equalities EUCLID, BINOP_1, SQUARE_1, SUBSET_1, PSCOMP_1, FINSEQ_2, CONNSP_3,
RVSUM_1, STRUCT_0, VALUED_1, ALGSTR_0, RLTOPSP1, METRIC_1, CONVEX1;
expansions TARSKI, XBOOLE_0, TOPS_2, TBSP_1, RLTOPSP1, XXREAL_2, METRIC_1;
theorems PRE_TOPC, CONNSP_1, EUCLID, TBSP_1, TOPREAL3, NAT_1, JGRAPH_1,
JORDAN1, TOPS_2, FUNCT_2, BORSUK_1, TOPMETR, TOPREAL1, FINSEQ_2,
ABSVALUE, RVSUM_1, SQUARE_1, BORSUK_2, TOPREAL5, WEIERSTR, TARSKI, SEQ_4,
FUNCT_1, METRIC_1, SUBSET_1, FUNCOP_1, ZFMISC_1, FINSEQ_1, FINSEQ_4,
RELAT_1, FUNCT_3, RCOMP_1, FUNCT_4, HEINE, TREAL_1, CONNSP_3, JORDAN6,
COMPTS_1, TSEP_1, CONNSP_2, TOPS_1, JORDAN5D, JORDAN2B, GOBOARD1,
GOBOARD2, GOBOARD5, GOBOARD6, UNIFORM1, FINSEQ_6, MATRIX_0, GOBOARD9,
GOBRD12, SPRECT_1, CARD_1, CARD_2, ENUMSET1, SPRECT_2, SPRECT_3, SEQ_2,
RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_0, XCMPLX_1,
BINOP_2, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, XXREAL_1, SEQM_3, NAT_D,
VALUED_1, RLTOPSP1, RLVECT_1, FINSEQ_3, SPPOL_1, RUSUB_4, CONVEX1,
METRIC_6, XTUPLE_0, RLVECT_4;
schemes NAT_1, CLASSES1;
begin :: from, RLAFFIN2, 2011.08.01, A.T.
registration
let n be Nat;
cluster TOP-REAL n -> add-continuous Mult-continuous;
coherence
proof
set T=TOP-REAL n,E=Euclid n,TE=TopSpaceMetr E;
A1: the TopStruct of T=TE by EUCLID:def 8;
thus T is add-continuous
proof
let x1,x2 be Point of T,V be Subset of T such that
A2: V is open and
A3: x1+x2 in V;
reconsider X1=x1,X2=x2,X12=x1+x2 as Point of E by A1,TOPMETR:12;
reconsider v=V as Subset of TE by A1;
V in the topology of T by A2,PRE_TOPC:def 2;
then v is open by A1,PRE_TOPC:def 2;
then consider r be Real such that
A4: r>0 and
A5: Ball(X12,r)c=v by A3,TOPMETR:15;
set r2=r/2;
reconsider B1=Ball(X1,r2),B2=Ball(X2,r2) as Subset of T by A1,TOPMETR:12;
take B1,B2;
thus B1 is open & B2 is open & x1 in B1 & x2 in B2
by A4,GOBOARD6:1,3,XREAL_1:215;
let x be object;
assume x in B1+B2;
then x in {b1+b2 where b1,b2 is Element of T:b1 in B1 & b2 in B2}
by RUSUB_4:def 9;
then consider b1,b2 be Element of T such that
A6: x=b1+b2 and
A7: b1 in B1 and
A8: b2 in B2;
reconsider e1=b1,e2=b2,e12=b1+b2 as Point of E by A1,TOPMETR:12;
reconsider y1=x1,y2=x2,c1=b1,c2=b2 as Element of REAL n by EUCLID:22;
dist(X2,e2)0 and
A16: Ball(AX,r)c=v by A14,TOPMETR:15;
set r2=r/2;
A17: r2>0 by A15,XREAL_1:215;
then A18: r2/2>0 by XREAL_1:215;
ex m be positive Real st |.a.|*m0;
then reconsider m=r2/2/|.a.| as positive Real
by A18,XREAL_1:139;
take m;
r2/20) by RVSUM_1:32
.=C-(Y-Y) by RVSUM_1:37
.=C-Y+Y by RVSUM_1:41;
then A24: |.c.|<=|.c-y.|+|.y.| by EUCLID:12;
A25: dist(X,e)=0 & |.y-c.|=dist(X,e) by COMPLEX1:46,SPPOL_1:5;
then |.a*y+-a*c.|<=|.a.|*m by A25,A27,XREAL_1:64;
then A28: |.a*y+-a*c.|0)-s*C by RVSUM_1:32
.=a*y-(a*C-a*C)-s*c by RVSUM_1:37
.=a*y-a*C+a*C-s*c by RVSUM_1:41
.=a*y-a*C+a*C+-s*c
.=a*y-a*C+(a*c+-s*c) by RVSUM_1:15
.=a*y+-a*c+(a*c+-s*c);
then dist(AX,se)=|.a*y+-a*c+(a*c+-s*c).| by SPPOL_1:5;
then dist(AX,se)=|.q2.|;
then |.q1.|- |.q2.|>=0 by XREAL_1:48;
then |.q1.|- |.q2.|=|.|.q1.|- |.q2.|.| by ABSVALUE:def 1;
hence thesis by TOPRNS_1:32;
end;
suppose
A1: |.q1.|<|.q2.|;
A2: |.q2.|- |.q1.|<= |.q2-q1.| by TOPRNS_1:32;
|.q2.|- |.q1.|>0 by A1,XREAL_1:50;
then |.|.q2.|- |.q1.|.|<= |.q2-q1.| by A2,ABSVALUE:def 1;
then |.|.q2.|- |.q1.|.|<= |.q1-q2.| by TOPRNS_1:27;
hence thesis by UNIFORM1:11;
end;
end;
theorem Th4:
|.|[r]|.|=|.r.|
proof
set p=|[r]|;
reconsider w=|[r]| as Element of REAL 1 by EUCLID:22;
reconsider r2=r^2 as Element of REAL by XREAL_0:def 1;
sqr w=<*r2*> by RVSUM_1:55;
then |.p.| =sqrt r2 by FINSOP_1:11
.=|.r.| by COMPLEX1:72;
hence thesis;
end;
Lm1:
for n being Nat, r being Real st r > 0
for x,y,z being Element of Euclid n st x = 0*n
for p being Element of TOP-REAL n st p = y & r*p = z
holds r*dist(x,y) = dist(x,z)
proof let n be Nat, r be Real such that
A1: r > 0;
let x,y,z be Element of Euclid n such that
A2: x = 0*n;
let p be Element of TOP-REAL n such that
A3: p = y and
A4: r*p = z;
reconsider x1=x, y1 = y as Element of REAL n;
A5: dist(x,z) = (Pitag_dist n).(x,z)
.= |.x1-r*y1.| by A3,A4,EUCLID:def 6;
A6: r*x1 = n |-> (0 *r) by A2,RVSUM_1:48
.= x1 by A2;
dist(x,y) = (Pitag_dist n).(x,y)
.= |.x1-y1.| by EUCLID:def 6;
hence r*dist(x,y) = |.r.|*|.x1-y1.| by A1,ABSVALUE:def 1
.= |.r*(x1-y1).| by EUCLID:11
.= |.r*x1 + r*(-y1).| by RVSUM_1:51
.= |.r*x1 + (-1)*r*y1.| by RVSUM_1:49
.= dist(x,z) by A5,A6,RVSUM_1:49;
end;
Lm2:
for n being Nat, r,s being Real st r > 0
for x being Element of Euclid n st x = 0*n
for A being Subset of TOP-REAL n st A = Ball(x,s)
holds r*A = Ball(x,r*s)
proof let n be Nat, r,s be Real such that
A1: r > 0;
let x be Element of Euclid n such that
A2: x = 0*n;
let A be Subset of TOP-REAL n such that
A3: A = Ball(x,s);
thus r*A c= Ball(x,r*s)
proof let y be object;
assume y in r*A;
then consider v being Element of TOP-REAL n such that
A4: y = r * v and
A5: v in A;
v in {q where q is Element of Euclid n : dist(x,q) < s}
by A5,A3,METRIC_1:def 14;
then consider q being Element of Euclid n such that
A6: v = q and
A7: dist(x,q) < s;
reconsider p = y as Element of Euclid n by A4,EUCLID:67;
r*dist(x,q) = dist(x,p) by A1,A2,A6,A4,Lm1;
then dist(x,p) < r*s by A7,A1,XREAL_1:68;
then y in {e where e is Element of Euclid n : dist(x,e) < r*s};
hence y in Ball(x,r*s) by METRIC_1:def 14;
end;
let y be object;
assume y in Ball(x,r*s);
then y in {q where q is Element of Euclid n : dist(x,q) < r*s}
by METRIC_1:def 14;
then consider z being Element of Euclid n such that
A8: y = z and
A9: dist(x,z) < r*s;
reconsider q = z as Element of TOP-REAL n by EUCLID:67;
set p = r"*q;
A10: y = 1 *q by A8,RVSUM_1:52
.= (r"*r)*q by A1,XCMPLX_0:def 7
.= r * p by RVSUM_1:49;
reconsider f = p as Element of Euclid n by EUCLID:67;
A11: dist(x,f) = r"*dist(x,z) by A1,A2,Lm1;
s = 1 *s
.= r"*r""*s by A1,XCMPLX_0:def 7
.= r"*(r*s);
then dist(x,f) < s by A9,A11,A1,XREAL_1:68;
then p in {e where e is Element of Euclid n : dist(x,e) < s};
then p in A by A3,METRIC_1:def 14;
hence y in r*A by A10;
end;
Lm3: for n being Nat, r,s,t be Real st 0 < s & s <= t
for x being Element of Euclid n st x = 0*n
for BA being Subset of TOP-REAL n st BA = Ball(x,r)
holds s*BA c= t*BA
proof let n be Nat, r,s,t be Real such that
A1: 0 < s and
A2: s <= t;
let x be Element of Euclid n such that
A3: x = 0*n;
let BA be Subset of TOP-REAL n such that
A4: BA = Ball(x,r);
let e be object;
assume e in s*BA;
then consider w being Element of TOP-REAL n such that
A5: e = s * w and
A6: w in BA;
w in {q where q is Element of Euclid n : dist(x,q) < r}
by A6,A4,METRIC_1:def 14;
then consider q being Element of Euclid n such that
A7: w = q and
A8: dist(x,q) < r;
set p = (s/t)*w;
A9: e = s * w by A5
.= t*(s/t)*w by A1,A2,XCMPLX_1:87
.= t*((s/t)*w) by RVSUM_1:49
.= t*p;
reconsider y = p as Element of Euclid n by EUCLID:67;
A10: dist(x,y) = (s/t)*dist(x,q) by A3,A7,Lm1,A1,A2,XREAL_1:139;
s/t <= 1 by A1,A2,XREAL_1:183;
then dist(x,y) <= dist(x,q) by A10,METRIC_1:5,XREAL_1:153;
then dist(x,y) < r by A8,XXREAL_0:2;
then p in {f where f is Element of Euclid n : dist(x,f) < r};
then p in BA by A4,METRIC_1:def 14;
hence e in t*BA by A9;
end;
theorem Th5:
for n being Nat, A be Subset of TOP-REAL n
holds A is bounded iff A is bounded Subset of Euclid n
proof let n be Nat, A be Subset of TOP-REAL n;
reconsider z = 0*n as Element of Euclid n;
thus A is bounded implies A is bounded Subset of Euclid n
proof assume
A1: A is bounded;
reconsider B = A as Subset of Euclid n by EUCLID:67;
z = 0.TOP-REAL n by EUCLID:70;
then reconsider V = Ball(z,1) as a_neighborhood of 0.TOP-REAL n
by GOBOARD6:2;
consider s being Real such that
A2: s > 0 and
A3: for t being Real
st t > s holds A c= t*V by A1;
set r = s+1;
0 < r by A2;
then r*V = Ball(z,r*1) by Lm2;
then B c= Ball(z,r) by A3,XREAL_1:29;
hence A is bounded Subset of Euclid n by A2,METRIC_6:def 3;
end;
assume
A4: A is bounded Subset of Euclid n;
then reconsider B = A as Subset of Euclid n;
consider r1 being Real such that
A5: 0 < r1 and
A6: B c= Ball(z,r1) by A4,METRIC_6:29;
let V be a_neighborhood of 0.TOP-REAL n;
0.TOP-REAL n = 0*n by EUCLID:70;
then z in Int V by CONNSP_2:def 1;
then consider r2 being Real such that
A7: r2 > 0 and
A8: Ball(z,r2) c= V by GOBOARD6:5;
reconsider r2 as Real;
take s = r1/r2;
thus
A9: s > 0 by A5,A7,XREAL_1:139;
let t;
reconsider BA = Ball(z,r2) as Subset of TOP-REAL n by EUCLID:67;
s*r2 = r1 by A7,XCMPLX_1:87;
then
A10: A c= s*BA by A6,A9,Lm2;
assume t > s;
then s*BA c= t*BA by A9,Lm3;
then
A11: A c= t*BA by A10;
t*BA c= t*V by A8,CONVEX1:39;
hence A c= t*V by A11;
end;
theorem
for A,B being Subset of TOP-REAL n st B is bounded & A c= B
holds A is bounded by RLTOPSP1:42;
definition
::$CD
let n be Nat;
let A, B be Subset of TOP-REAL n;
pred B is_inside_component_of A means
B is_a_component_of A` & B is bounded;
end;
registration
let M be non empty MetrStruct;
cluster bounded for Subset of M;
existence
proof
take {}M, 1;
thus thesis;
end;
end;
theorem Th7:
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 & 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 by CONNSP_1:def 6;
thus B is_inside_component_of A implies ex C being Subset of ((TOP-REAL n) |
(A`)) st C=B & C is a_component & C is bounded Subset of Euclid n
by Th5,A1;
given C being Subset of ((TOP-REAL n) | (A`)) such that
A2: C=B & C is a_component & C is bounded Subset
of Euclid n;
B is bounded & B is_a_component_of A` by A2,Th5,CONNSP_1:def 6;
hence thesis;
end;
definition
let n be Nat;
let A, B be Subset of TOP-REAL n;
pred B is_outside_component_of A means
B is_a_component_of A` & B is not bounded;
end;
theorem Th8:
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 &
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 by CONNSP_1:def 6;
thus B is_outside_component_of A implies ex C being Subset of ((TOP-REAL n) |
(A`)) st C=B & C is a_component & C is not bounded
Subset of Euclid n
proof
reconsider D2=B as Subset of Euclid n by TOPREAL3:8;
assume
A2: B is_outside_component_of A;
then consider C being Subset of (TOP-REAL n) | (A`) such that
A3: C=B and
A4: C is a_component by A1;
now
assume for D being Subset of Euclid n st D=C holds D is bounded;
then D2 is bounded by A3;
hence contradiction by A2,Th5;
end;
hence thesis by A3,A4;
end;
given C being Subset of ((TOP-REAL n) | (A`)) such that
A5: C=B & C is a_component & C is not bounded
Subset of Euclid n;
( not B is bounded)& B is_a_component_of A` by A5,Th5,CONNSP_1:def 6;
hence thesis;
end;
theorem
for A,B being Subset of TOP-REAL n st B is_inside_component_of A holds
B c= A`
by SPRECT_1:5;
theorem
for A,B being Subset of TOP-REAL n st B is_outside_component_of A
holds B c= A`
by SPRECT_1:5;
definition
let n be Nat;
let A be Subset of TOP-REAL n;
func BDD A -> Subset of TOP-REAL n equals
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 be object;
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 and
A2: y in {B where B is Subset of TOP-REAL n: B
is_inside_component_of A} by TARSKI:def 4;
ex B being Subset of TOP-REAL n st y=B & B is_inside_component_of A
by A2;
hence thesis by A1;
end;
hence thesis;
end;
end;
definition
let n be Nat;
let A be Subset of TOP-REAL n;
func UBD A -> Subset of TOP-REAL n equals
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 be object;
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 and
A2: y in {B where B is Subset of TOP-REAL n: B
is_outside_component_of A } by TARSKI:def 4;
ex B being Subset of TOP-REAL n st y=B & B is_outside_component_of A
by A2;
hence thesis by A1;
end;
hence thesis;
end;
end;
registration
let n be Nat;
cluster [#](TOP-REAL n) -> convex;
coherence;
end;
registration
let n;
cluster [#](TOP-REAL n) -> a_component;
coherence
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;
hence thesis by CONNSP_1:def 5;
end;
end;
::$CT 3
theorem Th11:
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 be object;
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 and
A2: B is_inside_component_of A;
ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component &
C is bounded Subset of Euclid n by A2,Th7;
hence thesis by A1;
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`);
reconsider F0 as Subset-Family of (TOP-REAL n) | A`;
A3: for B0 being Subset of ((TOP-REAL n) | A`) st B0 in F0 holds B0
is a_component
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 and
A5: B is_inside_component_of A;
ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component
& C is bounded Subset of Euclid n by A5,Th7;
hence thesis by A4;
end;
BDD A=union F0;
hence thesis by A3,CONNSP_3:def 2;
end;
theorem Th12:
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 be object;
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 and
A2: B is_outside_component_of A;
ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component
& C is not bounded Subset of Euclid n by A2,Th8;
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`);
reconsider F0 as Subset-Family of ((TOP-REAL n) | A`);
A3: for B0 being Subset of ((TOP-REAL n) | A`) st B0 in F0 holds B0
is a_component
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 and
A5: B is_outside_component_of A;
ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component
& C is not bounded Subset of Euclid n by A5,Th8;
hence thesis by A4;
end;
UBD A=union F0;
hence thesis by A3,CONNSP_3:def 2;
end;
theorem Th13:
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 B is_inside_component_of A;
then
A1: B in {B2 where B2 is Subset of TOP-REAL n: B2 is_inside_component_of A};
let x be object;
assume x in B;
hence thesis by A1,TARSKI:def 4;
end;
theorem Th14:
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 B is_outside_component_of A;
then
A1: B in {B2 where B2 is Subset of TOP-REAL n: B2 is_outside_component_of A};
let x be object;
assume x in B;
hence thesis by A1,TARSKI:def 4;
end;
theorem Th15:
for A being Subset of TOP-REAL n holds BDD A misses UBD A
proof
let A be Subset of TOP-REAL n;
set x = the Element of (BDD A) /\ (UBD A);
assume
A1: (BDD A) /\ (UBD A) <>{};
then
x in union{B where B is Subset of TOP-REAL n: B is_inside_component_of A
} by XBOOLE_0:def 4;
then consider y being set such that
A2: x in y and
A3: y in {B where B is Subset of TOP-REAL n: B is_inside_component_of A}
by TARSKI:def 4;
x in union{B2 where B2 is Subset of TOP-REAL n: B2
is_outside_component_of A} by A1,XBOOLE_0:def 4;
then consider y2 being set such that
A4: x in y2 and
A5: y2 in {B2 where B2 is Subset of TOP-REAL n: B2
is_outside_component_of A} by TARSKI:def 4;
consider B being Subset of TOP-REAL n such that
A6: y=B and
A7: B is_inside_component_of A by A3;
consider B2 being Subset of TOP-REAL n such that
A8: y2=B2 and
A9: B2 is_outside_component_of A by A5;
consider C being Subset of ((TOP-REAL n) | (A`)) such that
A10: C=B and
A11: C is a_component & C is bounded Subset of
Euclid n by A7,Th7;
consider C2 being Subset of ((TOP-REAL n) | (A`)) such that
A12: C2=B2 and
A13: C2 is a_component & C2 is not bounded Subset
of Euclid n by A9,Th8;
C /\ C2<>{}((TOP-REAL n) | (A`)) by A2,A6,A10,A4,A8,A12,XBOOLE_0:def 4;
then C meets C2;
hence contradiction by A11,A13,CONNSP_1:35;
end;
theorem Th16:
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 Th11;
D c= the carrier of ((TOP-REAL n) | A`);
hence thesis by PRE_TOPC:8;
end;
theorem Th17:
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 Th12;
D c= the carrier of ((TOP-REAL n) | A`);
hence thesis by PRE_TOPC:8;
end;
theorem Th18:
for A being Subset of TOP-REAL n holds (BDD A) \/ (UBD A) = A`
proof
let A be Subset of TOP-REAL n;
A1: A` c= (BDD A) \/ (UBD A)
proof
let z be object;
assume
A2: z in A`;
then reconsider p=z as Element of A`;
reconsider B=A` as non empty Subset of TOP-REAL n by A2;
reconsider q=p as Point of (TOP-REAL n) | A` by PRE_TOPC:8;
Component_of q is Subset of [#]((TOP-REAL n) | A`);
then Component_of q is Subset of A` by PRE_TOPC:def 5;
then reconsider G=Component_of q as Subset of TOP-REAL n by XBOOLE_1:1;
A3: (TOP-REAL n) | B is non empty;
then
A4: q in G by CONNSP_1:38;
Component_of q is a_component by A3,CONNSP_1:40;
then
A5: G is_a_component_of A` by CONNSP_1:def 6;
per cases;
suppose
G is bounded;
then G is_inside_component_of A by A5;
then G c= BDD A by Th13;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose
not G is bounded;
then G is_outside_component_of A by A5;
then G c= UBD A by Th14;
hence thesis by A4,XBOOLE_0:def 3;
end;
end;
(BDD A) c= A` & (UBD A) c= A` by Th16,Th17;
then (BDD A) \/ (UBD A) c= A` by XBOOLE_1:8;
hence thesis by A1;
end;
reserve u for Point of Euclid n;
theorem Th19:
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 that
p1 in P and
p2 in P;
the carrier of TOP-REAL n=REAL n by EUCLID:22;
hence thesis by A1;
end;
then P is convex by JORDAN1:def 1;
hence thesis;
end;
::$CT 4
theorem Th20:
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 that
A1: n>=1 and
A2: W=(REAL n);
reconsider y0=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
assume W is bounded;
then consider r being Real such that
A3: 0{};
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
set x0 = the Element of C;
x0 in C by A1;
then reconsider x0 as Point of Euclid n;
consider r being Real such that
0{};
set x0 = the Element of C;
x0 in C by A6;
then reconsider x0 as Point of Euclid n;
reconsider q0=x0 as Point of TOP-REAL n by TOPREAL3:8;
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
set R0=r+r;
A7: 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 that
A8: x in C and
A9: y in C;
reconsider q2=y as Point of TOP-REAL n by A9;
dist(o,y)=|.q2-(0.TOP-REAL n) .| by JGRAPH_1:28
.=|.q2.| by RLVECT_1:13;
then
A10: dist(o,y) =1 implies not [#](TOP-REAL n) is bounded
proof
assume
A1: n>=1;
assume [#](TOP-REAL n) is bounded;
then reconsider C=[#](TOP-REAL n) as bounded Subset of Euclid n by Th5;
C=REAL n by EUCLID:22;
hence contradiction by A1,Th20;
end;
theorem Th23:
n>=1 implies UBD {}(TOP-REAL n)=REAL n
proof
set A={}(TOP-REAL n);
A1: (TOP-REAL n) | [#](TOP-REAL n)=the TopStruct of TOP-REAL n by TSEP_1:93;
assume
A2: n>=1;
A3: now
reconsider D1=[#]((TOP-REAL n) | A`) as Subset of Euclid n
by A1,TOPREAL3:8;
assume for D being Subset of Euclid n st D=[#]((TOP-REAL n) | A`) holds D
is bounded;
then D1 is bounded;
then [#](TOP-REAL n) is bounded by A1,Th5;
hence contradiction by A2,Th22;
end;
[#]((TOP-REAL n) | A`) is a_component by A1,CONNSP_1:45;
then [#](TOP-REAL n) is_outside_component_of {}(TOP-REAL n) by A1,A3,Th8;
then
A4: [#](TOP-REAL n) in {B2 where B2 is Subset of TOP-REAL n: B2
is_outside_component_of {}(TOP-REAL n)};
UBD {}(TOP-REAL n) c= the carrier of TOP-REAL n;
hence UBD {}(TOP-REAL n) c= REAL n by EUCLID:22;
let x be object;
assume x in REAL n;
then x in [#](TOP-REAL n) by EUCLID:22;
hence thesis by A4,TARSKI:def 4;
end;
theorem Th24:
for w1,w2,w3 being Point of TOP-REAL n, P being non empty Subset
of TOP-REAL n, h1,h2 being Function 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
Function 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 Function of I[01],(TOP-REAL n) |P;
assume that
A1: h1 is continuous and
A2: w1=h1.0 and
A3: w2=h1.1 and
A4: h2 is continuous and
A5: w2=h2.0 and
A6: w3=h2.1;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
then reconsider p1=w1,p2=w2,p3=w3 as Point of (TOP-REAL n) |P by A2,A3,A6,
BORSUK_1:40,FUNCT_2:5;
p2,p3 are_connected by A4,A5,A6,BORSUK_2:def 1;
then reconsider P2=h2 as Path of p2,p3 by A4,A5,A6,BORSUK_2:def 2;
p1,p2 are_connected by A1,A2,A3,BORSUK_2:def 1;
then reconsider P1=h1 as Path of p1,p2 by A1,A2,A3,BORSUK_2:def 2;
ex P0 being Path of p1,p3 st P0 is continuous & P0.0=p1 & P0.1=p3 & for
t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 & t9 <= 1/2
implies P0.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies P0.t = P2.(2*t9-1) )
proof
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:40,RCOMP_1:def 1;
reconsider T1 = Closed-Interval-TSpace (0, 1/2), T2 =
Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01] by TOPMETR:20,TREAL_1:3;
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set E1 = P1 * e1;
set E2 = P2 * e2;
set f = E1 +* E2;
A7: dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:18;
A8: dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1.] by TOPMETR:18;
reconsider gg = E2 as Function of T2, ((TOP-REAL n) |P) by TOPMETR:20;
reconsider ff = E1 as Function of T1, ((TOP-REAL n) |P) by TOPMETR:20;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
A9: for t9 being Real st 1/2 <= t9 & t9 <= 1 holds E2.t9 = P2.(2*t9-1)
proof
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then
A10: dom e2 = [.1/2,1.] by TOPMETR:18
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
let t9 be Real;
assume 1/2 <= t9 & t9 <= 1;
then
A11: t9 in dom e2 by A10;
then reconsider s = t9 as Point of Closed-Interval-TSpace (1/2,1);
e2.s = ((r2 - r1)/(1 - 1/2))*t9 + (1 * r1 - (1/2)*r2)/(1 - 1/2) by
TREAL_1:11
.= 2*t9 - 1 by BORSUK_1:def 14,def 15,TREAL_1:5;
hence thesis by A11,FUNCT_1:13;
end;
A12: for t9 being Real st 0 <= t9 & t9 <= 1/2 holds E1.t9 = P1.(2*t9)
proof
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then
A13: dom e1 = [.0, 1/2.] by TOPMETR:18
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
let t9 be Real;
assume 0 <= t9 & t9 <= 1/2;
then
A14: t9 in dom e1 by A13;
then reconsider s = t9 as Point of Closed-Interval-TSpace (0, 1/2);
e1.s = ((r2 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 * r2)/(1/2 - 0) by
TREAL_1:11
.= 2*t9 by BORSUK_1:def 14,def 15,TREAL_1:5;
hence thesis by A14,FUNCT_1:13;
end;
then
A15: ff.(1/2) = P2.(2*(1/2)-1) by A3,A5
.= gg.pol by A9;
[#] T1 = [.0,1/2.] & [#] T2 = [.1/2,1.] by TOPMETR:18;
then
A16: ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} by
BORSUK_1:40,XXREAL_1:174,418;
rng f c= rng E1 \/ rng E2 by FUNCT_4:17;
then
A17: rng f c= the carrier of ((TOP-REAL n) |P) by XBOOLE_1:1;
A18: T1 is compact & T2 is compact by HEINE:4;
dom P1 = the carrier of I[01] by FUNCT_2:def 1;
then
A19: rng e1 c= dom P1 by TOPMETR:20;
dom P2 = the carrier of I[01] &
rng e2 c= the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:def 1;
then
A20: dom E2 = dom e2 by RELAT_1:27,TOPMETR:20;
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 A8,A20,RCOMP_1:def 1;
then
A21: f.0 = E1.0 by FUNCT_4:11
.= P1.(2*0) by A12
.= p1 by A2;
dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1.] by A7,A8,A19,A20,RELAT_1:27
.= the carrier of I[01] by BORSUK_1:40,XXREAL_1:174;
then reconsider f as Function of I[01], ((TOP-REAL n) |P) by A17,
FUNCT_2:def 1,RELSET_1:4;
e1 is continuous & e2 is continuous by TREAL_1:12;
then reconsider
f as continuous Function of I[01], ((TOP-REAL n) |P) by A1,A4,A15,A16,A18,
COMPTS_1:20,TOPMETR:20;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A8,A20,RCOMP_1:def 1;
then
A22: f.1 = E2.1 by FUNCT_4:13
.= P2.(2*1-1) by A9
.= p3 by A6;
then p1,p3 are_connected by A21,BORSUK_2:def 1;
then reconsider f as Path of p1, p3 by A21,A22,BORSUK_2:def 2;
for t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 &
t9 <= 1/2 implies f.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2
*t9-1) )
proof
let t be Point of I[01], t9 be Real;
assume
A23: t = t9;
thus 0 <= t9 & t9 <= 1/2 implies f.t = P1.(2*t9)
proof
assume
A24: 0 <= t9 & t9 <= 1/2;
then t9 in { r : 0 <= r & r <= 1/2 };
then
A25: t9 in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose
A26: t9 <> 1/2;
not t9 in dom E2
proof
assume t9 in dom E2;
then t9 in [.0,1/2.] /\ [.1/2,1.] by A8,A20,A25,XBOOLE_0:def 4;
then t9 in {1/2} by XXREAL_1:418;
hence thesis by A26,TARSKI:def 1;
end;
then f.t = E1.t by A23,FUNCT_4:11
.= P1.(2*t9) by A12,A23,A24;
hence thesis;
end;
suppose
A27: t9 = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by
TOPMETR:18;
then t in dom E2 by A23,A27,FUNCT_2:def 1,TOPMETR:20;
then f.t = E2.(1/2) by A23,A27,FUNCT_4:13
.= P1.(2*t9) by A12,A15,A27;
hence thesis;
end;
end;
thus 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2*t9-1)
proof
assume
A28: 1/2 <= t9 & t9 <= 1;
then t9 in { r : 1/2 <= r & r <= 1 };
then t9 in [.1/2,1.] by RCOMP_1:def 1;
then f.t = E2.t by A8,A20,A23,FUNCT_4:13
.= P2.(2*t9-1) by A9,A23,A28;
hence thesis;
end;
end;
hence thesis by A21,A22;
end;
hence thesis;
end;
theorem Th25:
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 Function 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 that
A1: w1 in P and
A2: w2 in P and
A3: w3 in P and
A4: LSeg(w1,w2) c= P and
A5: LSeg(w2,w3) c= P;
reconsider Y = P as non empty Subset of TOP-REAL n by A1;
per cases;
suppose
A6: w1<>w2;
then LSeg(w1,w2) is_an_arc_of w1,w2 by TOPREAL1:9;
then consider
f being Function of I[01], (TOP-REAL n) | LSeg(w1,w2) such that
A7: f is being_homeomorphism and
A8: f.0 = w1 and
A9: f.1 = w2 by TOPREAL1:def 1;
A10: rng f = [#]((TOP-REAL n) | LSeg(w1,w2)) by A7;
then
A11: rng f c= P by A4,PRE_TOPC:def 5;
then [#]((TOP-REAL n) | LSeg(w1,w2)) c= [#]((TOP-REAL n) |P) by A10,
PRE_TOPC:def 5;
then
A12: (TOP-REAL n) | LSeg(w1,w2) is SubSpace of (TOP-REAL n) |P by TOPMETR:3;
dom f= ([.0 ,1.]) by BORSUK_1:40,FUNCT_2:def 1;
then reconsider g=f as Function of ([.0,1.]),P by A11,FUNCT_2:2;
reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40
,PRE_TOPC:8;
A13: f is continuous by A7;
now
per cases;
suppose
w2<>w3;
then LSeg(w2,w3) is_an_arc_of w2,w3 by TOPREAL1:9;
then consider
f2 being Function of I[01], (TOP-REAL n) | LSeg(w2,w3) such
that
A14: f2 is being_homeomorphism and
A15: f2.0 = w2 & f2.1 = w3 by TOPREAL1:def 1;
A16: rng f2 = [#]((TOP-REAL n) | LSeg(w2,w3)) by A14;
then
A17: rng f2 c= P by A5,PRE_TOPC:def 5;
then [#]((TOP-REAL n) | LSeg(w2,w3)) c= [#]((TOP-REAL n) |P) by A16,
PRE_TOPC:def 5;
then
A18: (TOP-REAL n) | LSeg(w2,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3;
[#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5;
then reconsider
w19=w1,w29=w2,w39=w3 as Point of (TOP-REAL n) |P by A1,A2,A3;
A19: gt is continuous & w29=gt.1 by A9,A13,A12,PRE_TOPC:26;
dom f2=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider
g2=f2 as Function of ([.0,1.]),P by A17,FUNCT_2:2;
reconsider gt2=g2 as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40
,PRE_TOPC:8;
f2 is continuous by A14;
then gt2 is continuous by A18,PRE_TOPC:26;
then ex h being Function of I[01],(TOP-REAL n) | Y st h is continuous &
w19=h.0 & w39=h.1 & rng h c= (rng gt) \/ (rng gt2) by A8,A15,A19,BORSUK_2:13;
hence thesis;
end;
suppose
A20: w2=w3;
then LSeg(w1,w3) is_an_arc_of w1,w3 by A6,TOPREAL1:9;
then consider
f being Function of I[01], (TOP-REAL n) | LSeg(w1,w3) such that
A21: f is being_homeomorphism and
A22: f.0 = w1 & f.1 = w3 by TOPREAL1:def 1;
A23: rng f = [#]((TOP-REAL n) | LSeg(w1,w3)) by A21;
then
A24: rng f c= P by A4,A20,PRE_TOPC:def 5;
then [#]((TOP-REAL n) | LSeg(w1,w3)) c= [#]((TOP-REAL n) |P) by A23,
PRE_TOPC:def 5;
then
A25: (TOP-REAL n) | LSeg(w1,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3;
dom f=[.0 ,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider
g=f as Function of ([.0,1.]),P by A24,FUNCT_2:2;
reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40
,PRE_TOPC:8;
f is continuous by A21;
then gt is continuous by A25,PRE_TOPC:26;
hence thesis by A22;
end;
end;
hence thesis;
end;
suppose
A26: w1=w2;
now
per cases;
case
w2<>w3;
then LSeg(w1,w3) is_an_arc_of w1,w3 by A26,TOPREAL1:9;
then consider
f being Function of I[01], (TOP-REAL n) | LSeg(w1,w3) such that
A27: f is being_homeomorphism and
A28: f.0 = w1 & f.1 = w3 by TOPREAL1:def 1;
A29: rng f = [#]((TOP-REAL n) | LSeg(w1,w3)) by A27;
then
A30: rng f c= P by A5,A26,PRE_TOPC:def 5;
then [#]((TOP-REAL n) | LSeg(w1,w3)) c= [#]((TOP-REAL n) |P) by A29,
PRE_TOPC:def 5;
then
A31: (TOP-REAL n) | LSeg(w1,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3;
dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider g=f as Function of [.0,1.],P by A30,FUNCT_2:2;
reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40
,PRE_TOPC:8;
f is continuous by A27;
then gt is continuous by A31,PRE_TOPC:26;
hence thesis by A28;
end;
case
A32: w2=w3;
[#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5;
then reconsider w19=w1,w39=w3 as Point of (TOP-REAL n) |P by A1,A3;
ex f be Function of I[01], (TOP-REAL n) | Y st f is continuous & f.
0 = w19 & f.1 = w39 by A26,A32,BORSUK_2:3;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem Th26:
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 Function 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 that
A1: w1 in P and
A2: w2 in P and
A3: w3 in P and
A4: w4 in P and
A5: LSeg(w1,w2) c= P & LSeg(w2,w3) c= P and
A6: LSeg(w3,w4) c= P;
reconsider Y = P as non empty Subset of TOP-REAL n by A1;
consider h2 being Function of I[01],(TOP-REAL n) |P such that
A7: h2 is continuous & w1=h2.0 and
A8: w3=h2.1 by A1,A2,A3,A5,Th25;
per cases;
suppose
w3<>w4;
then LSeg(w3,w4) is_an_arc_of w3,w4 by TOPREAL1:9;
then consider
f being Function of I[01], (TOP-REAL n) | LSeg(w3,w4) such that
A9: f is being_homeomorphism and
A10: f.0 = w3 & f.1 = w4 by TOPREAL1:def 1;
A11: rng f = [#]((TOP-REAL n) | LSeg(w3,w4)) by A9;
then
A12: rng f c= P by A6,PRE_TOPC:def 5;
then [#]((TOP-REAL n) | LSeg(w3,w4)) c= [#]((TOP-REAL n) |P) by A11,
PRE_TOPC:def 5;
then
A13: (TOP-REAL n) | LSeg(w3,w4) is SubSpace of (TOP-REAL n) |P by TOPMETR:3;
[#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5;
then reconsider
w19=w1,w39=w3,w49=w4 as Point of (TOP-REAL n) |P by A1,A3,A4;
A14: w39=h2.1 by A8;
dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider g=f as Function of [.0,1.],P by A12,FUNCT_2:2;
reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40
,PRE_TOPC:8;
f is continuous by A9;
then gt is continuous by A13,PRE_TOPC:26;
then
ex h being Function of I[01],(TOP-REAL n) | Y st h is continuous & w19=
h.0 & w49=h.1 & rng h c= (rng h2) \/ (rng gt) by A7,A10,A14,BORSUK_2:13;
hence thesis;
end;
suppose
w3=w4;
hence thesis by A7,A8;
end;
end;
theorem Th27:
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 Function 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 that
A1: w1 in P and
A2: 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 h2 being Function of I[01],(TOP-REAL n) |P st h2 is continuous & w1=
h2.0 & w4=h2.1)& ex h4 being Function of I[01],(TOP-REAL n) |P st h4 is
continuous & w4=h4.0 & w7=h4.1 by A1,A2,Th26;
hence thesis by A1,Th24;
end;
theorem Th28:
for w1,w2 being Point of TOP-REAL n,P being Subset of
TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)& not (0.TOP-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.TOP-REAL n)
proof
let w1,w2 be Point of TOP-REAL n,P be Subset of TopSpaceMetr(Euclid n);
assume that
A1: P=LSeg(w1,w2) and
A2: not 0.TOP-REAL n in LSeg(w1,w2);
set M=Euclid n;
reconsider P0=P as Subset of TopSpaceMetr(M);
A3: the TopStruct of TOP-REAL n = TopSpaceMetr M by EUCLID:def 8;
then reconsider Q={0.TOP-REAL n} as Subset of TopSpaceMetr(M);
P0 is compact by A1,A3,COMPTS_1:23;
then consider x1,x2 being Point of M such that
A4: x1 in P0 and
A5: x2 in Q and
A6: dist(x1,x2) = min_dist_min(P0,Q) by A1,A3,WEIERSTR:30;
reconsider w01=x1 as Point of TOP-REAL n by EUCLID:67;
A7: x2=0.TOP-REAL n by A5,TARSKI:def 1;
reconsider o=0.TOP-REAL n as Point of M by EUCLID:67;
reconsider o2=0.TOP-REAL n as Point of TopSpaceMetr(M) by A3;
for x being object holds x in (dist_min(P0)).:(Q) iff x=(dist_min(P0)).o
proof
let x be object;
hereby
assume x in (dist_min(P0)).:(Q);
then
ex y being object st y in dom(dist_min(P0)) & y in Q & x=( dist_min(P0)
).y by FUNCT_1:def 6;
hence x=(dist_min(P0)).o by TARSKI:def 1;
end;
o2 in the carrier of TopSpaceMetr(M) by A3;
then
A8: o in Q & o in dom (dist_min(P0)) by FUNCT_2:def 1,TARSKI:def 1;
assume x=(dist_min(P0)).o;
hence thesis by A8,FUNCT_1:def 6;
end;
then
A9: (dist_min(P0)).:(Q)={(dist_min(P0)).o} by TARSKI:def 1;
[#] ((dist_min(P0)).:(Q))=(dist_min(P0)).:(Q) & lower_bound([#] ((
dist_min( P0)).:(Q)))=lower_bound((dist_min(P0)).:(Q)) by WEIERSTR:def 1,def 3;
then
A10: lower_bound((dist_min(P0)).:(Q))=(dist_min(P0)).o by A9,SEQ_4:9;
A11: |.w01.|=|.w01-0.TOP-REAL n.| by RLVECT_1:13
.=dist(x1,x2) by A7,JGRAPH_1:28;
|.w01.| <> 0 by A1,A2,A4,TOPRNS_1:24;
hence thesis by A1,A4,A6,A10,A11,WEIERSTR:def 7;
end;
theorem Th29:
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;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid 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 not (0.TOP-REAL n) in LSeg(w1,w4) by RLTOPSP1:71;
then consider w0 being Point of TOP-REAL n such that
w0 in LSeg(w1,w4) and
A2: |.w0.|>0 and
A3: |.w0.|=(dist_min(P)).(0.TOP-REAL n) by Th28;
set l9=(a+1)/|.w0.|;
set w2= l9*w1,w3=l9*w4;
A4: LSeg(w2,w3)c=Q
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
let x be object;
A5: |.l9.| = |.a+1.|/|.|.w0.|.| by COMPLEX1:67
.=|.a+1.|/|.w0.| by ABSVALUE:def 1;
(dist(o)).:(P) c= REAL
by XREAL_0:def 1;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
assume x in LSeg(w2,w3);
then consider r such that
A6: x=(1-r)*w2 + r*w3 and
A7: 0 <= r & r <= 1;
reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
A8: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A9: x in P and
A10: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A9,TOPREAL3:8;
r=dist(w0,o) by A10,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A11: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A12: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in LSeg(w1,w4) by A7;
then dist(w59,o) in ((dist(o)).:(P)) by A12,A8,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A11,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then |.w5.| >=|.w0.| by RLVECT_1:13;
then |.a+1.|>=0 & |.w5.|/|.w0.|>=1 by A2,COMPLEX1:46,XREAL_1:181;
then |.a+1.|*(|.w5.|/|.w0.|)>=|.a+1.|*1 by XREAL_1:66;
then |.a+1.|*(|.w0.|"*|.w5.|)>=|.a+1.| by XCMPLX_0:def 9;
then |.a+1.|*|.w0.|"*|.w5.|>=|.a+1.|;
then
A13: |.a+1.|/|.w0.|*|.w5.|>=|.a+1.| by XCMPLX_0:def 9;
a+1>a & |.a+1.|>=a+1 by ABSVALUE:4,XREAL_1:29;
then |.a+1.|>a by XXREAL_0:2;
then |.a+1.|/|.w0.|*|.w5.|>a by A13,XXREAL_0:2;
then |.l9*((1-r)*w1 + r*w4).|>a by A5,TOPRNS_1:7;
then |.l9*((1-r)*w1) + l9*(r*w4).|>a by RLVECT_1:def 5;
then |.l9*((1-r)*w1) + (l9*r)*w4.|>a by RLVECT_1:def 7;
then |.(l9*(1-r))*w1 + (l9*r)*w4.|>a by RLVECT_1:def 7;
then |.((1-r)*l9)*w1 + r*(l9*w4).|>a by RLVECT_1:def 7;
then |.(1-r)*w2 + r*w3.|>a by RLVECT_1:def 7;
hence thesis by A1,A6;
end;
A14: w3 in LSeg(w2,w3) by RLTOPSP1:68;
then
A15: w3 in Q by A4;
A16: LSeg(w4,w3) c=Q
proof
let x be object;
assume x in LSeg(w4,w3);
then consider r such that
A17: x=(1-r)*w4 + r*w3 and
A18: 0 <= r and
A19: r <= 1;
now
per cases;
case
A20: a>=0;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n;
A21: (1-0)*w4+0 * w1=(1-0)*w4+0.TOP-REAL n by RLVECT_1:10
.=(1-0)*w4 by RLVECT_1:4
.=w4 by RLVECT_1:def 8;
(dist(o)).:(P) c= REAL
by XREAL_0:def 1;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
A22: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A23: x in P and
A24: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A23,TOPREAL3:8;
r=dist(w0,o) by A24,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A25: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A26: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1};
then dist(w59,o) in ((dist(o)).:(P)) by A26,A22,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A25,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then
A27: |.w5.| >=|.w0.| by RLVECT_1:13;
r*l9*|.w0.| =r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:74
.=r*(a+1) by A2,XCMPLX_1:87;
then
A28: r*l9*|.w4.|>= r*(a+1) by A18,A20,A21,A27,XREAL_1:64;
A29: 1-r>=0 by A19,XREAL_1:48;
A30: a+r>=a+0 by A18,XREAL_1:6;
A31: ex q1 being Point of TOP-REAL n st q1=w4 & |.q1.| > a by A1;
now
per cases;
case
1-r>0;
then
A32: (1-r)*|.w4.|>(1-r)*a by A31,XREAL_1:68;
|.(1-r)+ r*l9.|*|.w4.|=((1-r)+ r*l9)*|.w4.| by A18,A20,A29,
ABSVALUE:def 1
.= (1-r)*|.w4.|+r*l9*|.w4.|;
then |.(1-r)+r*l9.|*|.w4.|>r*(a+1)+(1-r)*a by A28,A32,XREAL_1:8;
then |.(1-r)+r*l9.|*|.w4.|>a by A30,XXREAL_0:2;
then |.((1-r)+ r*l9)*w4.|>a by TOPRNS_1:7;
then |.(1-r)*w4 + r*l9*w4.|>a by RLVECT_1:def 6;
hence |.(1-r)*w4 + r*w3.|>a by RLVECT_1:def 7;
end;
case
1-r<=0;
then 1-r+r<=0+r by XREAL_1:6;
then r=1 by A19,XXREAL_0:1;
then
A33: (1-r)*w4+r*w3=0.TOP-REAL n +1 * w3 by RLVECT_1:10
.=0.TOP-REAL n +w3 by RLVECT_1:def 8
.=w3 by RLVECT_1:4;
ex q3 being Point of TOP-REAL n st q3=w3 & |.q3.| > a by A1,A15;
hence |.(1-r)*w4 + r*w3.|>a by A33;
end;
end;
hence |.(1-r)*w4 + r*w3.|>a;
end;
case
a<0;
hence |.(1-r)*w4 + r*w3.|>a;
end;
end;
hence thesis by A1,A17;
end;
A34: w2 in LSeg(w2,w3) by RLTOPSP1:68;
then
A35: w2 in Q by A4;
LSeg(w1,w2) c=Q
proof
let x be object;
assume x in LSeg(w1,w2);
then consider r such that
A36: x=(1-r)*w1 + r*w2 and
A37: 0 <= r and
A38: r <= 1;
now
per cases;
case
A39: a>=0;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n;
A40: (1-0)*w1+0 * w4=(1-0)*w1+0.TOP-REAL n by RLVECT_1:10
.=(1-0)*w1 by RLVECT_1:4
.=w1 by RLVECT_1:def 8;
((dist(o)).:(P)) c= REAL
by XREAL_0:def 1;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A41: x in P and
A42: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A41,TOPREAL3:8;
r=dist(w0,o) by A42,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A43: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A44: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in LSeg(w1,w4) & dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
then dist(w59,o) in ((dist(o)).:(P)) by A44,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A43,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then
A45: |.w5.| >=|.w0.| by RLVECT_1:13;
r*l9*|.w0.| =r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:74
.=r*(a+1) by A2,XCMPLX_1:87;
then
A46: r*l9*|.w1.|>= r*(a+1) by A37,A39,A40,A45,XREAL_1:64;
A47: ex q1 being Point of TOP-REAL n st q1=w1 & |.q1.| > a by A1;
A48: a+r>=a+0 by A37,XREAL_1:6;
A49: 1-r>=0 by A38,XREAL_1:48;
A50: ex q2 being Point of TOP-REAL n st q2=w2 & |.q2.| > a by A1,A35;
now
per cases;
case
1-r>0;
then
A51: (1-r)*|.w1.|>(1-r)*a by A47,XREAL_1:68;
|.(1-r)+ r*l9.|*|.w1.|=((1-r)+ r*l9)*|.w1.| by A37,A39,A49,
ABSVALUE:def 1
.= (1-r)*|.w1.|+r*l9*|.w1.|;
then |.(1-r)+ r*l9.|*|.w1.|>r*(a+1)+(1-r)*a by A46,A51,XREAL_1:8;
then |.(1-r)+ r*l9.|*|.w1.|>a by A48,XXREAL_0:2;
then |.((1-r)+ r*l9)*w1.|>a by TOPRNS_1:7;
then |.(1-r)*w1 + r*l9*w1.|>a by RLVECT_1:def 6;
hence |.(1-r)*w1 + r*w2.|>a by RLVECT_1:def 7;
end;
case
1-r<=0;
then 1-r+r<=0+r by XREAL_1:6;
then r=1 by A38,XXREAL_0:1;
then (1-r)*w1+r*w2=0.TOP-REAL n +1 * w2 by RLVECT_1:10
.=0.TOP-REAL n +w2 by RLVECT_1:def 8
.=w2 by RLVECT_1:4;
hence |.(1-r)*w1 + r*w2.|>a by A50;
end;
end;
hence |.(1-r)*w1 + r*w2.|>a;
end;
case
a<0;
hence |.(1-r)*w1 + r*w2.|>a;
end;
end;
hence thesis by A1,A36;
end;
hence thesis by A4,A34,A14,A16;
end;
theorem Th30:
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;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid 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 not (0.TOP-REAL n) in LSeg(w1,w4) by RLTOPSP1:71;
then consider w0 being Point of TOP-REAL n such that
w0 in LSeg(w1,w4) and
A2: |.w0.|>0 and
A3: |.w0.|=(dist_min(P)).(0.TOP-REAL n) by Th28;
set l9=a/|.w0.|;
set w2= l9*w1,w3=l9*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 object;
assume
A5: z in (REAL n)\ {q : (|.q.|) < a };
then reconsider q2=z as Point of TOP-REAL n by EUCLID:22;
not z in {q : (|.q.|) < a } by A5,XBOOLE_0:def 5;
then |.q2.| >= a;
hence thesis;
end;
let z be object;
assume z in {q1 : (|.q1.|) >= a };
then consider q1 such that
A6: z=q1 and
A7: (|.q1.|) >= a;
q1 in the carrier of TOP-REAL n;
then
A8: z in REAL n by A6,EUCLID:22;
for q st q=z holds (|.q.|) >= a by A6,A7;
then not z in {q : (|.q.|) < a };
hence thesis by A8,XBOOLE_0:def 5;
end;
A9: LSeg(w1,w2) c=Q
proof
let x be object;
assume x in LSeg(w1,w2);
then consider r such that
A10: x=(1-r)*w1 + r*w2 and
A11: 0 <= r and
A12: r <= 1;
now
per cases;
case
A13: a>0;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n;
A14: (1-0)*w1+0 * w4=(1-0)*w1+0.TOP-REAL n by RLVECT_1:10
.=(1-0)*w1 by RLVECT_1:4
.=w1 by RLVECT_1:def 8;
((dist(o)).:(P)) c= REAL
by XREAL_0:def 1;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A15: x in P and
A16: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A15,TOPREAL3:8;
r=dist(w0,o) by A16,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A17: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A18: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in LSeg(w1,w4) & dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
then dist(w59,o) in ((dist(o)).:(P)) by A18,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A17,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then
A19: |.w5.| >=|.w0.| by RLVECT_1:13;
A20: 1-r>=0 by A12,XREAL_1:48;
then
A21: |.(1-r)+r*l9.|*|.w1.|=((1-r)+ r*l9)*|.w1.| by A11,A13,ABSVALUE:def 1
.= (1-r)*|.w1.|+r*l9*|.w1.|;
ex q1 being Point of TOP-REAL n st q1=w1 & |.q1.| >= a by A1,A4;
then
A22: (1-r)*|.w1.|>=(1-r)*a by A20,XREAL_1:64;
r*l9*|.w0.| =r*a/|.w0.|*|.w0.| by XCMPLX_1:74
.=r*a by A2,XCMPLX_1:87;
then r*l9*|.w1.|>= r*a by A11,A13,A14,A19,XREAL_1:64;
then |.(1-r)+r*l9.|*|.w1.|>=r*a+(1-r)*a by A22,A21,XREAL_1:7;
then |.((1-r)+ r*l9)*w1.|>=a by TOPRNS_1:7;
then |.(1-r)*w1 + r*l9*w1.|>=a by RLVECT_1:def 6;
hence |.(1-r)*w1 + r*w2.|>=a by RLVECT_1:def 7;
end;
case
a<=0;
hence |.(1-r)*w1 + r*w2.|>=a;
end;
end;
hence thesis by A1,A4,A10;
end;
A23: LSeg(w4,w3) c=Q
proof
let x be object;
assume x in LSeg(w4,w3);
then consider r such that
A24: x=(1-r)*w4 + r*w3 and
A25: 0 <= r and
A26: r <= 1;
now
per cases;
case
A27: a>0;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n;
A28: (1-0)*w4+0 * w1=(1-0)*w4+0.TOP-REAL n by RLVECT_1:10
.=(1-0)*w4 by RLVECT_1:4
.=w4 by RLVECT_1:def 8;
((dist(o)).:(P)) c= REAL
by XREAL_0:def 1;
then reconsider F=((dist(o)).:(P)) as Subset of REAL;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
A29: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A30: x in P and
A31: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A30,TOPREAL3:8;
r=dist(w0,o) by A31,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A32: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A33: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1};
then dist(w59,o) in ((dist(o)).:(P)) by A33,A29,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A32,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then
A34: |.w5.| >=|.w0.| by RLVECT_1:13;
A35: 1-r>=0 by A26,XREAL_1:48;
then
A36: |.(1-r)+r*l9.|*|.w4.|=((1-r)+ r*l9)*|.w4.| by A25,A27,ABSVALUE:def 1
.= (1-r)*|.w4.|+r*l9*|.w4.|;
ex q1 being Point of TOP-REAL n st q1=w4 & |.q1.| >= a by A1,A4;
then
A37: (1-r)*|.w4.|>=(1-r)*a by A35,XREAL_1:64;
r*l9*|.w0.| =r*a/|.w0.|*|.w0.| by XCMPLX_1:74
.=r*a by A2,XCMPLX_1:87;
then r*l9*|.w4.|>= r*a by A25,A27,A28,A34,XREAL_1:64;
then |.(1-r)+r*l9.|*|.w4.|>=r*a+(1-r)*a by A37,A36,XREAL_1:7;
then |.((1-r)+ r*l9)*w4.|>=a by TOPRNS_1:7;
then |.(1-r)*w4 + r*l9*w4.|>=a by RLVECT_1:def 6;
hence |.(1-r)*w4 + r*w3.|>=a by RLVECT_1:def 7;
end;
case
a<=0;
hence |.(1-r)*w4 + r*w3.|>=a;
end;
end;
hence thesis by A1,A4,A24;
end;
A38: LSeg(w2,w3)c=Q
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n);
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
let x be object;
A39: |.l9.|=|.a.|/|.|.w0.|.| by COMPLEX1:67
.=|.a.|/|.w0.| by ABSVALUE:def 1;
((dist(o)).:(P)) c= REAL
by XREAL_0:def 1;
then reconsider F=(dist(o)).:(P) as Subset of REAL;
assume x in LSeg(w2,w3);
then consider r such that
A40: x=(1-r)*w2 + r*w3 and
A41: 0 <= r & r <= 1;
reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n;
reconsider w59=w5 as Point of Euclid n by TOPREAL3:8;
A42: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o).:P
proof
let r be ExtReal;
assume r in ((dist(o)).:(P));
then consider x being object such that
x in dom (dist(o)) and
A43: x in P and
A44: r=(dist(o)).x by FUNCT_1:def 6;
reconsider w0=x as Point of Euclid n by A43,TOPREAL3:8;
r=dist(w0,o) by A44,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
then
A45: F is bounded_below;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then w59 in the carrier of TopSpaceMetr(Euclid n);
then
A46: w59 in dom (dist(o)) by FUNCT_2:def 1;
w5 in LSeg(w1,w4) by A41;
then dist(w59,o) in ((dist(o)).:(P)) by A46,A42,FUNCT_1:def 6;
then lower_bound F <=dist(w59,o) by A45,SEQ_4:def 2;
then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1;
then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3;
then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6;
then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28;
then |.w5.| >=|.w0.| by RLVECT_1:13;
then |.a.|>=0 & |.w5.|/|.w0.|>=1 by A2,COMPLEX1:46,XREAL_1:181;
then |.a.|*(|.w5.|/|.w0.|)>=|.a.|*1 by XREAL_1:66;
then |.a.|*(|.w5.|*|.w0.|")>=|.a.| by XCMPLX_0:def 9;
then |.a.|*|.w0.|"*|.w5.|>=|.a.|;
then
A47: |.a.|/|.w0.|*|.w5.|>=|.a.| by XCMPLX_0:def 9;
|.a.|>=a by ABSVALUE:4;
then |.a.|/|.w0.|*|.w5.|>=a by A47,XXREAL_0:2;
then |.l9*((1-r)*w1 + r*w4).|>=a by A39,TOPRNS_1:7;
then |.l9*((1-r)*w1) + l9*(r*w4).|>=a by RLVECT_1:def 5;
then |.l9*((1-r)*w1) + (l9*r)*w4.|>=a by RLVECT_1:def 7;
then |.(l9*(1-r))*w1 + (l9*r)*w4.|>=a by RLVECT_1:def 7;
then |.((1-r)*l9)*w1 + r*(l9*w4).|>=a by RLVECT_1:def 7;
then |.(1-r)*w2 + r*w3.|>=a by RLVECT_1:def 7;
hence thesis by A1,A4,A40;
end;
w2 in LSeg(w2,w3) & w3 in LSeg(w2,w3) by RLTOPSP1:68;
hence thesis by A38,A9,A23;
end;
theorem
for f being FinSequence of REAL holds f is Element of REAL (len
f) & f is Point of TOP-REAL (len f) by EUCLID:76;
theorem Th32:
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 Element of NAT st 1<=
i & i<=len f holds g/.i=r*f/.i
proof
reconsider h2= (id REAL) as Function;
let x be Element of REAL n,f,g be FinSequence of REAL,
r be Real;
assume that
A1: f=x and
A2: g=r*x;
A3: len f=n by A1,CARD_1:def 7;
set h1= (dom (id REAL)) --> r;
A4: dom (<:h1, h2:>)=dom (h1) /\ dom ((id REAL)) by FUNCT_3:def 7;
A5: len g=n by A2,CARD_1:def 7;
A6: g= (multreal * (<:h1, h2:>))*x by A2,FUNCOP_1:def 5;
for i being Element of NAT st 1<=i & i<=len f holds g/.i=r*f/.i
proof
let i be Element of NAT;
A7: dom h1=dom (id REAL) by FUNCOP_1:13
.=REAL by FUNCT_1:17;
reconsider xi = x.i as Element of REAL by XREAL_0:def 1;
dom h2=REAL by FUNCT_1:17;
then
A8: h1.(xi) = r by FUNCOP_1:7;
assume
A9: 1<=i & i<=len f;
then
A10: f.i=f/.i by FINSEQ_4:15;
i in Seg len f by A9,FINSEQ_1:1;
then i in dom g by A3,A5,FINSEQ_1:def 3;
then
A11: g.i=(multreal * (<:h1, h2:>)).(x.i) by A6,FUNCT_1:12;
A12: dom (<:h1, h2:>)=dom h1 /\ REAL by A4,FUNCT_1:17;
then (<:h1, h2:>).(x.i)=[h1.(xi),h2.(xi)] by A7,FUNCT_3:def 7;
then g.i=multreal.(r,f.i) by A1,A11,A12,A7,A8,FUNCT_1:13;
then g.i=r*(f/.i) by A10,BINOP_2:def 11;
hence thesis by A3,A5,A9,FINSEQ_4:15;
end;
hence thesis by A2,A3,CARD_1:def 7;
end;
theorem Th33:
for x being Element of REAL n,f being FinSequence st x<> 0*n & x
=f holds ex i being Element of NAT st 1<=i & i<=n & f.i<>0
proof
let x be Element of REAL n,f be FinSequence;
assume that
A1: x<> 0*n and
A2: x=f;
A3: len f=n by A2,CARD_1:def 7;
assume
A4: not ex i being Element of NAT st 1<=i & i<=n & f.i<>0;
for z being object holds z in f iff
ex x,y being object st x in Seg n & y in {0} & z = [ x,y]
proof
let z be object;
hereby
assume
A5: z in f;
then consider x0,y0 being object such that
A6: z = [x0,y0] by RELAT_1:def 1;
A7: y0=f.x0 by A5,A6,FUNCT_1:1;
A8: x0 in dom f by A5,A6,XTUPLE_0:def 12;
then reconsider n1=x0 as Element of NAT;
A9: x0 in Seg len f by A8,FINSEQ_1:def 3;
then 1<=n1 & n1<=len f by FINSEQ_1:1;
then f.n1=0 by A3,A4;
then y0 in {0} by A7,TARSKI:def 1;
hence ex x,y being object
st x in Seg n & y in {0} & z = [x,y] by A3,A6,A9;
end;
given x,y being object such that
A10: x in Seg n and
A11: y in {0} and
A12: z = [x,y];
reconsider n1=x as Element of NAT by A10;
A13: n1<=n by A10,FINSEQ_1:1;
A14: x in dom f by A3,A10,FINSEQ_1:def 3;
y=0 & 1<=n1 by A10,A11,FINSEQ_1:1,TARSKI:def 1;
then y=f.x by A4,A13;
hence thesis by A12,A14,FUNCT_1:1;
end;
then f=[:Seg n,{0}:] by ZFMISC_1:def 2;
hence contradiction by A1,A2,FUNCOP_1:def 2;
end;
theorem Th34:
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 that
A1: n>=2 and
A2: x<> 0*n;
reconsider f=x as FinSequence of REAL;
consider i2 being Element of NAT such that
A3: 1<=i2 and
A4: i2<=n and
A5: f.i2<>0 by A2,Th33;
A6: len f=n by CARD_1:def 7;
then
A7: 1<=len f by A1,XXREAL_0:2;
per cases;
suppose
A8: i2>1;
reconsider f11 = (f/.1)+1 as Element of REAL by XREAL_0:def 1;
reconsider g=(<*f11*>)^mid(f,2,len f) as FinSequence of REAL;
A9: len (mid(f,2,len f))=len f-'2+1 by A1,A6,A7,FINSEQ_6:118
.=len f-2+1 by A1,A6,XREAL_1:233;
len g=len (<*(f/.1+1)*>) + len (mid(f,2,len f)) by FINSEQ_1:22;
then
A10: len g=1+(len f-2+1) by A9,FINSEQ_1:39
.=len f;
then reconsider y2=g as Element of REAL n by A6,EUCLID:76;
A11: len (<*(f/.1+1)*>)=1 by FINSEQ_1:39;
now
given r being Real such that
A12: y2=r*x or x=r*y2;
per cases by A12;
suppose
A13: y2=r*x;
i2<=len f-(1+1)+(1+1) by A4,CARD_1:def 7;
then
A14: i2-1<=len f-(1+1)+1+1-1 by XREAL_1:9;
A15: i2-'1=i2-1 & 1<=i2-'1 by A8,NAT_D:49,XREAL_1:233;
A16: 1<=len f by A1,A6,XXREAL_0:2;
then
A17: g/.1=g.1 by A10,FINSEQ_4:15;
A18: g/.i2=g.i2 by A3,A4,A6,A10,FINSEQ_4:15;
A19: i2-'1+2-'1=i2-'1+1+1-'1 .=i2-'1+1 by NAT_D:34
.=i2-1+1 by A3,XREAL_1:233
.=i2;
A20: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15;
1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A4,A8,A9,CARD_1:def 7,NAT_1:13;
then g.i2= (mid(f,2,len f)).(i2-1) by A11,FINSEQ_1:23
.=f.i2 by A1,A6,A9,A16,A15,A14,A19,FINSEQ_6:118;
then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A13,A18,A20,Th32;
then
A21: 1=r by A5,A20,XCMPLX_1:5;
g/.1=r*f/.1 by A13,A16,Th32;
then f/.1+1=1 * f/.1 by A21,A17,FINSEQ_1:41;
hence contradiction;
end;
suppose
A22: x=r*y2;
i2<=len f-(1+1)+(1+1) by A4,CARD_1:def 7;
then
A23: i2-1<=len f-(1+1)+1+1-1 by XREAL_1:9;
A24: i2-'1=i2-1 & 1<=i2-'1 by A8,NAT_D:49,XREAL_1:233;
A25: 1<=len f by A1,A6,XXREAL_0:2;
then
A26: g/.1=g.1 by A10,FINSEQ_4:15;
A27: g/.i2=g.i2 by A3,A4,A6,A10,FINSEQ_4:15;
A28: i2-'1+2-'1=i2-'1+1+1-'1 .=i2-'1+1 by NAT_D:34
.=i2-1+1 by A3,XREAL_1:233
.=i2;
A29: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15;
1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A4,A8,A9,CARD_1:def 7,NAT_1:13;
then g.i2= (mid(f,2,len f)).(i2-1) by A11,FINSEQ_1:23
.=f.i2 by A1,A6,A9,A25,A24,A23,A28,FINSEQ_6:118;
then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A10,A22,A27,A29,Th32;
then
A30: 1=r by A5,A29,XCMPLX_1:5;
f/.1=r*g/.1 by A10,A22,A25,Th32;
then f/.1+1=1 * f/.1 by A30,A26,FINSEQ_1:41;
hence contradiction;
end;
end;
hence thesis;
end;
suppose
A31: i2<=1;
reconsider ff1 = f/.len f+1 as Element of REAL by XREAL_0:def 1;
reconsider g=mid(f,1,len f-'1)^<*ff1*> as FinSequence of REAL;
A32: len f-'1<=len f by NAT_D:44;
A33: 1+1-1<=len f-1 by A1,A6,XREAL_1:9;
A34: len f-'1=len f-1 by A1,A6,XREAL_1:233,XXREAL_0:2;
then
A35: len f-'1-'1+1=len f-1-1+1 by A33,XREAL_1:233
.=len f-(1+1)+1;
then
A36: len (mid(f,1,len f-'1)) =len f-1 by A7,A34,A32,A33,FINSEQ_6:118;
len (<*(f/.len f+1)*>)=1 & len (mid(f,1,len f-'1))=len f-2+1 by A7,A34,A32
,A33,A35,FINSEQ_1:39,FINSEQ_6:118;
then
A37: len g=(len f-2+1)+1 by FINSEQ_1:22
.=len f;
then reconsider y2=g as Element of REAL n by A6,EUCLID:76;
A38: i2=1 by A3,A31,XXREAL_0:1;
now
given r being Real such that
A39: y2=r*x or x=r*y2;
per cases by A39;
suppose
A40: y2=r*x;
A41: g/.i2=g.i2 by A3,A4,A6,A37,FINSEQ_4:15;
A42: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15;
g.i2= (mid(f,1,len f-'1)).i2 by A38,A33,A36,FINSEQ_6:109
.=f.i2 by A38,A34,A32,A33,FINSEQ_6:123;
then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A40,A41,A42,Th32;
then
A43: 1=r by A5,A42,XCMPLX_1:5;
A44: g.len f= g.(len f -1+1) .=f/.len f+1 by A36,FINSEQ_1:42;
A45: 1<=len f by A1,A6,XXREAL_0:2;
then
A46: g/.len f=g.len f by A37,FINSEQ_4:15;
g/.len f=r*f/.len f by A40,A45,Th32;
hence contradiction by A43,A46,A44;
end;
suppose
A47: x=r*y2;
A48: g/.i2=g.i2 by A3,A4,A6,A37,FINSEQ_4:15;
A49: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15;
g.i2= (mid(f,1,len f-'1)).i2 by A38,A33,A36,FINSEQ_6:109
.=f.(i2) by A38,A34,A32,A33,FINSEQ_6:123;
then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A37,A47,A48,A49,Th32;
then
A50: 1=r by A5,A49,XCMPLX_1:5;
A51: g.len f=g.(len f-1+1) .=f/.len f+1 by A36,FINSEQ_1:42;
A52: 1<=len f by A1,A6,XXREAL_0:2;
then
A53: g/.len f=g.len f by A37,FINSEQ_4:15;
f/.len f=r*g/.len f by A37,A47,A52,Th32;
hence contradiction by A50,A53,A51;
end;
end;
hence thesis;
end;
end;
theorem Th35:
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;
reconsider y1=w1 as Element of REAL n by EUCLID:22;
given r8 being Real such that
A2: w1=r8*w7 or w7=r8*w1;
per cases;
suppose
A3: a>=0;
now
assume
A4: w1=0.TOP-REAL n;
ex q st q=w1 & (|.q.|)>a by A1;
hence contradiction by A3,A4,TOPRNS_1:23;
end;
then w1 <> 0*n by EUCLID:70;
then consider y being Element of REAL n such that
A5: not ex r being Real st y=r*y1 or y1=r*y by A1,Th34;
set y4=((a+1)/|.y.|)*y;
reconsider w4=y4 as Point of TOP-REAL n by EUCLID:22;
A6: now
A7: 0 *y1 = 0 * w1
.= 0.TOP-REAL n by RLVECT_1:10
.=0*n by EUCLID:70;
assume |.y.|=0;
hence contradiction by A5,A7,EUCLID:8;
end;
then
A8: (a+1)/|.y.|>0 by A3,XREAL_1:139;
A9: now
reconsider y9=y,y19=y1 as Element of n-tuples_on REAL;
given r being Real such that
A10: w1=r*w4 or w4=r*w1;
per cases by A10;
suppose
w1=r*w4;
then y1=(r*((a+1)/|.y.|))*y by RVSUM_1:49;
hence contradiction by A5;
end;
suppose
w4=r*w1;
then ((a+1)/|.y.|)"*((a+1)/|.y.|)*y9=((a+1)/|.y.|)"*(r*y1) by
RVSUM_1:49;
then ((a+1)/|.y.|)"*((a+1)/|.y.|)*y=((a+1)/|.y.|)"*r*y19 by RVSUM_1:49;
then 1 *y=((a+1)/|.y.|)"*r*y1 by A8,XCMPLX_0:def 7;
then y=((a+1)/|.y.|)"*r*y1 by RVSUM_1:52;
hence contradiction by A5;
end;
end;
A11: |.w4.|=|.(a+1)/|.y.|.|*|.y.| by EUCLID:11
.= (a+1)/|.y.|*|.y.| by A3,ABSVALUE:def 1
.=a+1 by A6,XCMPLX_1:87;
then |.w4.|>a by XREAL_1:29;
then
A12: w4 in Q by A1;
now
given r1 being Real such that
A13: w4=r1*w7 or w7=r1*w4;
A14: now
assume r1=0;
then
A15: w4=0.TOP-REAL n or w7=0.TOP-REAL n by A13,RLVECT_1:10;
ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1;
hence contradiction by A3,A11,A15,TOPRNS_1:23;
end;
per cases by A2;
suppose
A16: w1=r8*w7;
now
per cases by A13;
case
w4=r1*w7;
then r1"*w4=r1"*r1*w7 by RLVECT_1:def 7;
then r1"*w4=1 *w7 by A14,XCMPLX_0:def 7;
then r1"*w4=w7 by RLVECT_1:def 8;
then w1=r8*r1"*w4 by A16,RLVECT_1:def 7;
hence contradiction by A9;
end;
case
w7=r1*w4;
then r1"*w7=r1"*r1*w4 by RLVECT_1:def 7;
then r1"*w7=1 *w4 by A14,XCMPLX_0:def 7;
then r1"*w7=w4 by RLVECT_1:def 8;
then r1""*w4=r1""*r1"*w7 by RLVECT_1:def 7;
then r1""*w4=1 *w7 by A14,XCMPLX_0:def 7;
then r1""*w4=w7 by RLVECT_1:def 8;
then w1=r8*r1""*w4 by A16,RLVECT_1:def 7;
hence contradiction by A9;
end;
end;
hence contradiction;
end;
suppose
A17: w7=r8*w1;
A18: now
assume r8=0;
then
A19: w7=0.TOP-REAL n by A17,RLVECT_1:10;
ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1;
hence contradiction by A3,A19,TOPRNS_1:23;
end;
r8"*w7=r8"*r8*w1 by A17,RLVECT_1:def 7;
then r8"*w7=1 *w1 by A18,XCMPLX_0:def 7;
then
A20: r8"*w7=w1 by RLVECT_1:def 8;
now
per cases by A13;
case
w4=r1*w7;
then r1"*w4=r1"*r1*w7 by RLVECT_1:def 7;
then r1"*w4=1 *w7 by A14,XCMPLX_0:def 7;
then r1"*w4=w7 by RLVECT_1:def 8;
then w1=r8"*r1"*w4 by A20,RLVECT_1:def 7;
hence contradiction by A9;
end;
case
w7=r1*w4;
then r1"*w7=r1"*r1*w4 by RLVECT_1:def 7;
then r1"*w7=1 *w4 by A14,XCMPLX_0:def 7;
then r1"*w7=w4 by RLVECT_1:def 8;
then r1""*w4=r1""*r1"*w7 by RLVECT_1:def 7;
then r1""*w4=1 *w7 by A14,XCMPLX_0:def 7;
then r1""*w4=w7 by RLVECT_1:def 8;
then w1=r8"*r1""*w4 by A20,RLVECT_1:def 7;
hence contradiction by A9;
end;
end;
hence contradiction;
end;
end;
then
A21: ex w29,w39 being Point of TOP-REAL n st w29 in Q & w39 in Q & LSeg(w4,
w29) c=Q & LSeg(w29,w39) c= Q & LSeg(w39,w7) c= Q by A1,A12,Th29;
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 by A1,A12,A9,Th29;
hence thesis by A12,A21;
end;
suppose
A22: a<0;
set w2=0.TOP-REAL n;
A23: REAL n c= Q
proof
let x be object;
assume x in REAL n;
then reconsider w=x as Point of TOP-REAL n by EUCLID:22;
|.w.|>=0;
hence thesis by A1,A22;
end;
the carrier of TOP-REAL n=REAL n by EUCLID:22;
then
A24: Q=the carrier of TOP-REAL n by A23;
then LSeg(w1,w2) c=Q & LSeg(w2,w7) c=Q;
hence thesis by A24;
end;
end;
theorem Th36:
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;
reconsider y1=w1 as Element of REAL n by EUCLID:22;
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;
per cases;
suppose
A3: a>0;
now
assume w1=0.TOP-REAL n;
then |.w1.|=0 by TOPRNS_1:23;
then w1 in {q : (|.q.|) < a } by A3;
hence contradiction by A1,XBOOLE_0:def 5;
end;
then w1 <> 0*n by EUCLID:70;
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,Th34;
set y4=(a/|.y.|)*y;
reconsider w4=y4 as Point of TOP-REAL n by EUCLID:22;
A5: now
A6: 0 *y1 = 0 * w1
.= 0.TOP-REAL n by RLVECT_1:10
.=0*n by EUCLID:70;
assume |.y.|=0;
hence contradiction by A4,A6,EUCLID:8;
end;
then
A7: a/|.y.|>0 by A3,XREAL_1:139;
A8: now
reconsider y9=y,y19=y1 as Element of n-tuples_on REAL;
given r being Real such that
A9: w1=r*w4 or w4=r*w1;
y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y9=(a/|.y.|)"*(r*y1)
by A9,RVSUM_1:49;
then y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y=(a/|.y.|)"*r*y19 by
RVSUM_1:49;
then
A10: y1=(r*(a/|.y.|))*y9 or 1 *y=(a/|.y.|)"*r*y1 by A7,XCMPLX_0:def 7;
per cases by A10,RVSUM_1:52;
suppose
y1=(r*(a/|.y.|))*y;
hence contradiction by A4;
end;
suppose
y=(a/|.y.|)"*r*y1;
hence contradiction by A4;
end;
end;
A11: |.w4.|=|.a/|.y.|.|*|.y.| by EUCLID:11
.= a/|.y.|*|.y.| by A3,ABSVALUE:def 1
.=a by A5,XCMPLX_1:87;
A12: now
assume w4 in {q : (|.q.|) < a };
then ex q st q=w4 & (|.q.|) < a;
hence contradiction by A11;
end;
then
A13: w4 in Q by A1,XBOOLE_0:def 5;
now
given r1 being Real such that
A14: w4=r1*w7 or w7=r1*w4;
A15: now
assume r1=0;
then w4=0.TOP-REAL n or w7=0.TOP-REAL n by A14,RLVECT_1:10;
then |.w4.|=0 or |.w7.|=0 by TOPRNS_1:23;
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,A12,XBOOLE_0:def 5;
end;
now
per cases by A2;
case
A16: w1=r8*w7;
now
per cases by A14;
case
w4=r1*w7;
then r1"*w4=r1"*r1*w7 by RLVECT_1:def 7;
then r1"*w4=1 *w7 by A15,XCMPLX_0:def 7;
then r1"*w4=w7 by RLVECT_1:def 8;
then w1=r8*r1"*w4 by A16,RLVECT_1:def 7;
hence contradiction by A8;
end;
case
w7=r1*w4;
then r1"*w7=r1"*r1*w4 by RLVECT_1:def 7;
then r1"*w7=1 *w4 by A15,XCMPLX_0:def 7;
then r1"*w7=w4 by RLVECT_1:def 8;
then r1""*w4=r1""*r1"*w7 by RLVECT_1:def 7;
then r1""*w4=1 *w7 by A15,XCMPLX_0:def 7;
then r1""*w4=w7 by RLVECT_1:def 8;
then w1=r8*r1""*w4 by A16,RLVECT_1:def 7;
hence contradiction by A8;
end;
end;
hence contradiction;
end;
case
A17: w7=r8*w1;
A18: now
assume r8=0;
then w7=0.TOP-REAL n by A17,RLVECT_1:10;
then |.w7.|=0 by TOPRNS_1:23;
then w7 in {q : (|.q.|) < a } by A3;
hence contradiction by A1,XBOOLE_0:def 5;
end;
r8"*w7=r8"*r8*w1 by A17,RLVECT_1:def 7;
then r8"*w7=1 *w1 by A18,XCMPLX_0:def 7;
then
A19: r8"*w7=w1 by RLVECT_1:def 8;
now
per cases by A14;
case
w4=r1*w7;
then r1"*w4=r1"*r1*w7 by RLVECT_1:def 7;
then r1"*w4=1 *w7 by A15,XCMPLX_0:def 7;
then r1"*w4=w7 by RLVECT_1:def 8;
then w1=r8"*r1"*w4 by A19,RLVECT_1:def 7;
hence contradiction by A8;
end;
case
w7=r1*w4;
then r1"*w7=r1"*r1*w4 by RLVECT_1:def 7;
then r1"*w7=1 *w4 by A15,XCMPLX_0:def 7;
then r1"*w7=w4 by RLVECT_1:def 8;
then r1""*w4=r1""*r1"*w7 by RLVECT_1:def 7;
then r1""*w4=1 *w7 by A15,XCMPLX_0:def 7;
then r1""*w4=w7 by RLVECT_1:def 8;
then w1=r8"*r1""*w4 by A19,RLVECT_1:def 7;
hence contradiction by A8;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
then
A20: ex w29,w39 being Point of TOP-REAL n st w29 in Q & w39 in Q & LSeg(w4,
w29) c=Q & LSeg(w29,w39) c= Q & LSeg(w39,w7) c= Q by A1,A13,Th30;
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 by A1,A13,A8,Th30;
hence thesis by A13,A20;
end;
suppose
A21: a<=0;
set w2=0.TOP-REAL n;
A22: REAL n c= Q
proof
let x be object;
A23: now
assume x in {q : (|.q.|) < a };
then ex q being Point of TOP-REAL n st q=x & (|.q.|) < a;
hence contradiction by A21;
end;
assume x in REAL n;
hence thesis by A1,A23,XBOOLE_0:def 5;
end;
the carrier of TOP-REAL n=REAL n by EUCLID:22;
then
A24: Q=the carrier of TOP-REAL n by A22;
then LSeg(w1,w2) c=Q & LSeg(w2,w7) c=Q;
hence thesis by A24;
end;
end;
theorem Th37:
for a being Real st n>=1 holds {q: |.q.| >a} <>{}
proof
let a be Real;
assume
A1: n>=1;
now
|.a+1.|>=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26;
then
A2: |.a+1.|*1<=|.a+1.|*sqrt n by SQUARE_1:18,XREAL_1:64;
A3: a+1<=|.a+1.| by ABSVALUE:4;
assume not (a+1)*(1.REAL n) in {q : |.q.| > a };
then
A4: |.(a+1)*(1.REAL n).|<=a;
A5: a=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 reconsider Q=P as non empty Subset of TOP-REAL n by Th37,XXREAL_0:2;
for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7 ex f
being Function 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 that
A2: w1 in Q & w7 in Q and
w1<>w7;
per cases;
suppose
not (ex r being Real st w1=r*w7 or w7=r*w1);
then
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,w7) c= Q by A1,A2,Th29;
hence thesis by A2,Th26;
end;
suppose
ex r being Real st w1=r*w7 or w7=r*w1;
then
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 A1,A2,Th35;
hence thesis by A2,Th27;
end;
end;
hence thesis by JORDAN1:2;
end;
theorem Th39:
for a being Real st n>=1 holds (REAL n) \ {q: |.q.| < a} <> {}
proof
let a be Real;
A1: {q:(|.q.|)>a} c= (REAL n)\{q2:(|.q2.|)a};
then consider q such that
A2: q=x and
A3: (|.q.|)>a;
A4: now
assume x in {q2:(|.q2.|)=1;
hence thesis by A1,Th37,XBOOLE_1:3;
end;
theorem Th40:
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 reconsider Q=P as non empty Subset of TOP-REAL n by Th39,XXREAL_0:2;
for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7 ex f
being Function 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 that
A2: w1 in Q & w7 in Q and
w1<>w7;
per cases;
suppose
not (ex r being Real st w1=r*w7 or w7=r*w1);
then
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,w7) c= Q by A1,A2,Th30;
hence thesis by A2,Th26;
end;
suppose
ex r being Real st w1=r*w7 or w7=r*w1;
then
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 A1,A2,Th36;
hence thesis by A2,Th27;
end;
end;
hence thesis by JORDAN1:2;
end;
theorem Th41:
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 that
A1: n>=1 and
A2: P=(REAL n)\ {q where q is Point of TOP-REAL n : |.q.| < a };
per cases;
suppose
A3: a>0;
now
set p = the Element of P;
assume P is bounded;
then consider r being Real such that
A4: for q being Point of TOP-REAL n st q in P holds |.q.|{} by A1,A2,Th39;
then p in P;
then reconsider p as Point of TOP-REAL n;
A6: |.p.|=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26;
then
A12: |.a+r+1.|*1<=|.a+r+1.|*sqrt n by SQUARE_1:18,XREAL_1:64;
|.(a+r+1)*(1.REAL n).|=|.a+r+1.|*|.(1.REAL n).| by TOPRNS_1:7
.=|.a+r+1.|*(sqrt n) by EUCLID:73;
then a+r+1<= |.(a+r+1)*(1.REAL n).| by A12,A10,XXREAL_0:2;
hence contradiction by A9,A11,XXREAL_0:2;
end;
A13: a+r+1<=|.a+r+1.| by ABSVALUE:4;
|.a+r+1.|>=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26;
then
A14: |.a+r+1.|*1<=|.a+r+1.|*sqrt n by SQUARE_1:18,XREAL_1:64;
A15: a+r{};
then d in {q where q is Point of TOP-REAL n: (|.q.|) < a };
then ex q being Point of TOP-REAL n st q=d & (|.q.|) < a;
hence contradiction by A17;
end;
then P=[#](TOP-REAL n) by A2,EUCLID:22;
hence thesis by A1,Th22;
end;
end;
theorem Th42:
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 that
A2: w1 in P and
A3: w2 in P;
consider q2 being Point of TOP-REAL 1 such that
A4: q2=w2 and
A5: ex r st q2=<*r*> & r > a by A1,A3;
consider q1 being Point of TOP-REAL 1 such that
A6: q1=w1 and
A7: ex r st q1=<*r*> & r > a by A1,A2;
consider r2 such that
A8: q2=<*r2*> and
A9: r2 > a by A5;
consider r1 such that
A10: q1=<*r1*> and
A11: r1 > a by A7;
thus LSeg(w1,w2) c= P
proof
let x be object;
assume x in LSeg(w1,w2);
then consider r3 being Real such that
A12: x=(1-r3)*w1+r3*w2 and
A13: 0<=r3 and
A14: r3<=1;
A15: 1-r3>=0 by A14,XREAL_1:48;
per cases;
suppose
A16: r3>0;
A17: (1-r3)*r1>=(1-r3)*a & (1-r3)*a+r3*a=a by A11,A15,XREAL_1:64;
r3*r2>r3*a by A9,A16,XREAL_1:68;
then
A18: (1-r3)*r1+r3*r2>a by A17,XREAL_1:8;
<*(1-r3)*r1+r3*r2*>=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:22
.=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:21
.=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:21;
hence thesis by A1,A6,A10,A4,A8,A12,A18;
end;
suppose
r3<=0;
then r3=0 by A13;
then x=w1+0 *w2 by A12,RLVECT_1:def 8
.=w1+0.TOP-REAL 1 by RLVECT_1:10
.=w1 by RLVECT_1:4;
hence thesis by A2;
end;
end;
end;
hence thesis by JORDAN1:def 1;
end;
theorem Th43:
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 that
A2: w1 in P and
A3: w2 in P;
consider q2 being Point of TOP-REAL 1 such that
A4: q2=w2 and
A5: ex r st q2=<*r*> & r < -a by A1,A3;
consider q1 being Point of TOP-REAL 1 such that
A6: q1=w1 and
A7: ex r st q1=<*r*> & r < -a by A1,A2;
consider r2 such that
A8: q2=<*r2*> and
A9: r2 < -a by A5;
consider r1 such that
A10: q1=<*r1*> and
A11: r1 < -a by A7;
thus LSeg(w1,w2) c= P
proof
let x be object;
assume x in LSeg(w1,w2);
then consider r3 being Real such that
A12: x=(1-r3)*w1+r3*w2 and
A13: 0<=r3 and
A14: r3<=1;
A15: 1-r3>=0 by A14,XREAL_1:48;
per cases;
suppose
A16: r3>0;
A17: (1-r3)*r1<=(1-r3)*(-a) & (1-r3)*(-a)+r3*(-a)=-a by A11,A15,XREAL_1:64;
r3*r2=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:22
.=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:21
.=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:21;
hence thesis by A1,A6,A10,A4,A8,A12,A18;
end;
suppose
r3<=0;
then r3=0 by A13;
then x=w1+0 *w2 by A12,RLVECT_1:def 8
.=w1+0.TOP-REAL 1 by RLVECT_1:10
.=w1 by RLVECT_1:4;
hence thesis by A2;
end;
end;
end;
hence thesis by JORDAN1:def 1;
end;
::$CT 2
theorem Th44:
for W being Subset of Euclid 1,a being Real
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }
holds W is not bounded
proof
let W be Subset of Euclid 1,a be Real;
assume
A1: W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a };
|.a.|>=0 by COMPLEX1:46;
then
A2: |.a.|+|.a.|+|.a.|>=0+|.a.| by XREAL_1:6;
assume W is bounded;
then consider r such that
A3: 0 by FINSEQ_2:59
.=<*((r+|.a.|)*1)*> by RVSUM_1:47;
reconsider z2=(r+|.a.|)*(1.REAL 1) as Point of Euclid 1
by FINSEQ_2:131;
a<=|.a.| & 0+|.a.| by FINSEQ_2:59
.=<*((3*(r+|.a.|))*1)*> by RVSUM_1:47;
reconsider z1=(3*(r+|.a.|))*(1.REAL 1) as Point of Euclid 1
by FINSEQ_2:131;
dist(z1,z2)=|.(3*(r+|.a.|))*(1.REAL 1)-((r+|.a.|)*(1.REAL 1)).| by
JGRAPH_1:28
.=|.((r+|.a.|)+(r+|.a.|)+(r+|.a.|)-(r+|.a.|))*(1.REAL 1).| by RLVECT_1:35
.=|.(r+|.a.|)+(r+|.a.|).|*|.(1.REAL 1).| by TOPRNS_1:7
.=|.(r+|.a.|)+(r+|.a.|).|*(sqrt 1) by EUCLID:73;
then
A8: (r+|.a.|)+(r+|.a.|)<= dist(z1,z2) by ABSVALUE:4,SQUARE_1:18;
A9: 0<=|.a.| by COMPLEX1:46;
then (r+|.a.|)+0<(r+|.a.|)+(r+|.a.|) by A3,XREAL_1:6;
then
A10: (r+|.a.|)0 by A3,XREAL_1:129;
then a<=|.a.| & 0+|.a.|<3*r+3*|.a.| by A2,ABSVALUE:4,XREAL_1:8;
then a<3*(r+|.a.|) by XXREAL_0:2;
then (3*(r+|.a.|))*(1.REAL 1) in W by A1,A7;
hence contradiction by A4,A6,A11;
end;
theorem Th45:
for W being Subset of Euclid 1,a being Real
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }
holds W is not bounded
proof
let W be Subset of Euclid 1,a be Real;
|.a.|>=0 by COMPLEX1:46;
then
A1: |.a.|+|.a.|+|.a.|>=0+|.a.| by XREAL_1:6;
assume
A2: W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a };
assume W is bounded;
then consider r such that
A3: 0 by FINSEQ_2:59
.=<*((-3*(r+|.a.|))*1)*> by RVSUM_1:47;
reconsider z1=(-3*(r+|.a.|))*(1.REAL 1) as Point of Euclid 1
by FINSEQ_2:131;
3*r>0 by A3,XREAL_1:129;
then a<=|.a.| & 0+|.a.|<3*r+3*|.a.| by A1,ABSVALUE:4,XREAL_1:8;
then a<3*(r+|.a.|) by XXREAL_0:2;
then -a> -(3*(r+|.a.|)) by XREAL_1:24;
then
A6: (-3*(r+|.a.|))*(1.REAL 1) in {q where q is Point of TOP-REAL 1: ex r
st q=<*r*> & r< -a } by A5;
A7: (-(r+|.a.|))*(1.REAL 1) = (-(r+|.a.|))*<* 1 *> by FINSEQ_2:59
.=<* (-(r+|.a.|))*1 *> by RVSUM_1:47;
reconsider z2=(-(r+|.a.|))*(1.REAL 1) as Point of Euclid 1
by FINSEQ_2:131;
dist(z1,z2)=|.(-3*(r+|.a.|))*(1.REAL 1)-(-(r+|.a.|))*(1.REAL 1).| by
JGRAPH_1:28
.=|.(-3*(r+|.a.|)--(r+|.a.|))*(1.REAL 1).| by RLVECT_1:35
.=|.-((-3*(r+|.a.|)--(r+|.a.|))*(1.REAL 1)).| by TOPRNS_1:26
.=|.(-(-3*(r+|.a.|)+--(r+|.a.|)))*(1.REAL 1).| by RLVECT_1:79
.=|.(r+|.a.|)+(r+|.a.|).|*|.(1.REAL 1).| by TOPRNS_1:7
.=|.(r+|.a.|)+(r+|.a.|).|*(sqrt 1) by EUCLID:73;
then
A8: (r+|.a.|)+(r+|.a.|)<= dist(z1,z2) by ABSVALUE:4,SQUARE_1:18;
A9: 0<=|.a.| by COMPLEX1:46;
then (r+|.a.|)+0<(r+|.a.|)+(r+|.a.|) by A3,XREAL_1:6;
then
A10: (r+|.a.|) -(r+|.a.|) by XREAL_1:24;
then (-(r+|.a.|))*(1.REAL 1) in W by A2,A7;
hence contradiction by A2,A4,A6,A11;
end;
theorem Th46:
for W being Subset of Euclid n,a being Real
st n>=2 & W={q : |.q.| > a } holds W is not bounded
proof
let W be Subset of Euclid n,a be Real;
assume
A1: n>=2 & W={q : |.q.| > a };
A2: 1<=n by A1,XXREAL_0:2;
then
A3: 1<=sqrt n by SQUARE_1:18,26;
assume W is bounded;
then consider r such that
A4: 0=0 & 1<=sqrt n by A2,COMPLEX1:46,SQUARE_1:18,26;
then
A7: |.r+|.a.|.|*1<=|.r+|.a.|.|*sqrt n by XREAL_1:64;
a<=|.a.| & |.a.|=0 by COMPLEX1:46;
then
A11: |.r+|.a.|.|*1<=|.r+|.a.|.|*sqrt n by A3,XREAL_1:64;
|.(r+|.a.|)*(1.REAL n).|=|.r+|.a.|.|*|.(1.REAL n).| by TOPRNS_1:7
.=|.r+|.a.|.|*sqrt n by EUCLID:73;
then (r+|.a.|)<= |.(r+|.a.|)*(1.REAL n).| by A11,A10,XXREAL_0:2;
then a<|.(r+|.a.|)*(1.REAL n).| by A8,XXREAL_0:2;
then
A12: (r+|.a.|)*(1.REAL n) in W by A1;
then reconsider z1=(r+|.a.|)*(1.REAL n) as Point of Euclid n;
A13: (r+|.a.|)+(r+|.a.|)<=|.(r+|.a.|)+(r+|.a.|).| by ABSVALUE:4;
|.(r+|.a.|)+(r+|.a.|).|>=0 by COMPLEX1:46;
then
A14: |.(r+|.a.|)+(r+|.a.|).|*1<=|.(r+|.a.|)+(r+|.a.|).|*sqrt n by A3,XREAL_1:64
;
A15: 0<=|.a.| by COMPLEX1:46;
then
A16: r+0<=r+|.a.| by XREAL_1:6;
A17: (r+|.a.|)+0<(r+|.a.|)+(r+|.a.|) by A4,A15,XREAL_1:6;
dist(z1,z2)=|.(r+|.a.|)*(1.REAL n)--((r+|.a.|)*(1.REAL n)).| by JGRAPH_1:28
.=|.(r+|.a.|)*(1.REAL n)+((r+|.a.|)*(1.REAL n)).|
.=|.((r+|.a.|)+(r+|.a.|))*(1.REAL n).| by RLVECT_1:def 6
.=|.((r+|.a.|)+(r+|.a.|)).|*|.(1.REAL n).| by TOPRNS_1:7
.=|.(r+|.a.|)+(r+|.a.|).|*(sqrt n) by EUCLID:73;
then (r+|.a.|)+(r+|.a.|)<= dist(z1,z2) by A14,A13,XXREAL_0:2;
then (r+|.a.|)=2 & W=(REAL n)\ {q : (|.q.|) < a } holds W is not bounded
proof
let W be Subset of Euclid n,a be Real;
reconsider 1R = 1.REAL n as Point of TOP-REAL n;
assume
A1: n>=2 & W=(REAL n)\ {q : (|.q.|) < a };
assume W is bounded;
then consider r such that
A2: 0=1 by A1,XXREAL_0:2;
then
A6: 1<=sqrt n by SQUARE_1:18,26;
A7: now
a<=|.a.| & |.a.|=0 by COMPLEX1:46;
then
A10: |.r+|.a.|.|*1<=|.r+|.a.|.|*sqrt n by A6,XREAL_1:64;
A11: (r+|.a.|)<=|.r+|.a.|.| by ABSVALUE:4;
|.-((r+|.a.|)*(1.REAL n)).| = |.((r+|.a.|)*(1.REAL n)).| by TOPRNS_1:26
.=|.r+|.a.|.|*|.(1.REAL n).| by TOPRNS_1:7
.=|.r+|.a.|.|*(sqrt n) by EUCLID:73;
then (r+|.a.|)<= |.-((r+|.a.|)*(1.REAL n)).| by A10,A11,XXREAL_0:2;
hence contradiction by A9,A8,XXREAL_0:2;
end;
A12: now
a<=|.a.| & |.a.|=0 by COMPLEX1:46;
then
A15: |.r+|.a.|.|*1<=|.r+|.a.|.|*sqrt n by A6,XREAL_1:64;
A16: (r+|.a.|)<=|.r+|.a.|.| by ABSVALUE:4;
|.(r+|.a.|)*(1.REAL n).|=|.r+|.a.|.|*|.(1.REAL n).| by TOPRNS_1:7
.=|.r+|.a.|.|*(sqrt n) by EUCLID:73;
then (r+|.a.|)<= |.(r+|.a.|)*(1.REAL n).| by A15,A16,XXREAL_0:2;
hence contradiction by A14,A13,XXREAL_0:2;
end;
reconsider z2=-((r+|.a.|)*(1.REAL n)) as Point of Euclid n by EUCLID:22;
reconsider z1=(r+|.a.|)*(1.REAL n) as Point of Euclid n by EUCLID:22;
A17: (r+|.a.|)+(r+|.a.|)<=|.(r+|.a.|)+(r+|.a.|).| by ABSVALUE:4;
|.((r+|.a.|)+(r+|.a.|)).|>=0 by COMPLEX1:46;
then
A18: |.(r+|.a.|)+(r+|.a.|).|*1<=|.(r+|.a.|)+(r+|.a.|).|*sqrt n by A6,XREAL_1:64
;
dist(z1,z2)=|.(r+|.a.|)*(1.REAL n)--((r+|.a.|)*(1.REAL n)).| by JGRAPH_1:28
.=|.(r+|.a.|)*1R + --((r+|.a.|)*1R).|
.=|.(r+|.a.|)*1R+((r+|.a.|)*1R).|
.=|.((r+|.a.|)+(r+|.a.|))*1R .| by RLVECT_1:def 6
.=|.((r+|.a.|)+(r+|.a.|))*(1.REAL n).|
.=|.((r+|.a.|)+(r+|.a.|)).|*|.(1.REAL n).| by TOPRNS_1:7
.=|.((r+|.a.|)+(r+|.a.|)).|*(sqrt n) by EUCLID:73;
then (r+|.a.|)+(r+|.a.|)<= dist(z1,z2) by A18,A17,XXREAL_0:2;
then
A19: (r+|.a.|) {}Euclid n by A3;
A11: W /\ Q = {} by A5;
now
assume Q`={};
then Q=({}(the carrier of TOP-REAL n))`;
hence contradiction by A1,A10,A11,XBOOLE_1:28;
end;
then reconsider Q1=Q` as non empty Subset of TOP-REAL n;
(TOP-REAL n) | Q1 is non empty;
then Component_of P0 is a_component by A1,A10,A8,CONNSP_3:9;
hence thesis by A4,A7,A9,Th8;
end;
theorem Th49:
for A being Subset of Euclid n, B being non empty Subset of
Euclid n, C being Subset of (Euclid n) | B st A=C & C is bounded holds A is
bounded
proof
let A be Subset of Euclid n, B be non empty Subset of Euclid n, C be Subset
of (Euclid n) | B;
assume that
A1: A=C and
A2: C is bounded;
consider r0 being Real such that
A3: 0{};
then reconsider A1=A as non empty Subset of Euclid n by TOPREAL3:8;
[#]((TOP-REAL n) | A)=A2 by PRE_TOPC:def 5;
then [#]((TOP-REAL n) | A) is compact by A1,COMPTS_1:2;
then
A2: (TOP-REAL n) | A is compact by COMPTS_1:1;
TopSpaceMetr((Euclid n) | A1)=(TOP-REAL n) | A by EUCLID:63;
then (Euclid n) | A1 is totally_bounded by A2,TBSP_1:9;
then
A3: (Euclid n) | A1 is bounded by TBSP_1:19;
[#]((Euclid n) | A1) =A1 by TOPMETR:def 2;
then A1 is bounded by A3,Th49;
hence thesis by Th5;
end;
suppose
A={};
hence thesis;
end;
end;
registration
let n be Element of NAT;
cluster compact -> bounded for Subset of TOP-REAL n;
coherence by Th50;
end;
theorem Th51:
for A being Subset of TOP-REAL n st 1<=n & A is bounded holds A` <> {}
proof
let A be Subset of TOP-REAL n;
assume that
A1: 1<=n and
A2: A is bounded;
consider r being Real such that
A3: for q being Point of TOP-REAL n st q in A holds |.q.|=0 by COMPLEX1:46;
then
A4: |.r.|*|.1.REAL n.|>=|.r.|*1 by A1,EUCLID:75,XREAL_1:64;
|.r*(1.REAL n).|=|.r.|*|.1.REAL n.| & r<=|.r.| by ABSVALUE:4,TOPRNS_1:7;
then not r*(1.REAL n) in A by A3,A4,XXREAL_0:2;
hence thesis by XBOOLE_0:def 5;
end;
theorem Th52:
for r being Real holds (ex B being Subset of Euclid n st B={q :
(|.q.|) < r }) & for A being Subset of Euclid n st A={q1 : (|.q1.|) < r } holds
A is bounded
proof
let r be Real;
A1: {q : (|.q.|) < r } c= the carrier of Euclid n
proof
let x be object;
assume x in {q : (|.q.|) < r };
then ex q being Point of TOP-REAL n st q=x & (|.q.|) < r;
then x in the carrier of TOP-REAL n;
hence thesis by TOPREAL3:8;
end;
hence ex B being Subset of Euclid n st B={q : (|.q.|) < r };
reconsider C={q1 : (|.q1.|) < r } as Subset of TOP-REAL n by A1,TOPREAL3:8;
let A be Subset of Euclid n;
for q being Point of TOP-REAL n st q in C holds |.q.|=2 & A is bounded holds
UBD A is_outside_component_of A
proof
let A be Subset of TOP-REAL n;
assume that
A1: n>=2 and
A2: A is bounded;
reconsider C=A as bounded Subset of Euclid n by A2,Th5;
per cases;
suppose
A3: C<>{};
set x0 = the Element of C;
A4: x0 in C by A3;
then reconsider q1=x0 as Point of TOP-REAL n;
reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67;
reconsider x0 as Point of Euclid n by A4;
consider r being Real such that
0= r+dist(o,x0)+1 by A9;
then dist(o,z)>=r+dist(o,x0)+1 by A11,RLVECT_1:13;
then r+(dist(o,x0)+1)<=r+dist(o,x0) by A10,XXREAL_0:2;
then dist(o,x0)+1<=dist(o,x0)+0 by XREAL_1:6;
hence contradiction by XREAL_1:6;
end;
reconsider P=W as Subset of TOP-REAL n by TOPREAL3:8;
reconsider P as Subset of TOP-REAL n;
the carrier of (TOP-REAL n) | A`=A` by PRE_TOPC:8;
then reconsider P1=Component_of (Down(P,A`)) as Subset of TOP-REAL n by
XBOOLE_1:1;
A12: P is connected by A1,Th40;
A13: UBD A c= P1
proof
A14: (TOP-REAL n) |P is connected by A12,CONNSP_1:def 3;
A15: P c= A` by A6,SUBSET_1:23;
then Down(P,A`)=P by XBOOLE_1:28;
then ((TOP-REAL n) | A`) | Down(P,A`) is connected by A15,A14,PRE_TOPC:7;
then
A16: Down(P,A`) is connected by CONNSP_1:def 3;
reconsider G=A` as non empty Subset of TOP-REAL n by A1,A2,Th51,
XXREAL_0:2;
let z be object;
assume z in UBD A;
then consider y being set such that
A17: z in y and
A18: 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
A19: y=B and
A20: B is_outside_component_of A by A18;
consider C2 being Subset of ((TOP-REAL n) | (A`)) such that
A21: C2=B and
A22: C2 is a_component and
A23: C2 is not bounded Subset of Euclid n by A20,Th8;
consider D2 being Subset of Euclid n such that
A24: D2={q : |.q.| < R0 } by Th52;
reconsider D2 as Subset of Euclid n;
A25: A c= D2
proof
let z be object;
A26: |.q1.|=|.q1-0.TOP-REAL n.| by RLVECT_1:13
.=dist(x0,o) by JGRAPH_1:28;
assume
A27: z in A;
then reconsider q2=z as Point of TOP-REAL n;
reconsider x1=q2 as Point of Euclid n by TOPREAL3:8;
|.q2-q1.|=dist(x1,x0) & dist(x1,x0)<=r by A5,A27,JGRAPH_1:28;
then
A28: |.q2-q1.|+|.q1.|<=r+dist(o,x0) by A26,XREAL_1:6;
A29: r+dist(o,x0){} by A24,A30,XBOOLE_1:3,26;
then
A34: Down(P,A`) meets C2;
C2 is connected by A22,CONNSP_1:def 5;
then C2 c= Component_of (Down(P,A`)) by A16,A34,CONNSP_3:16;
hence thesis by A17,A19,A21;
end;
W is not bounded by A1,Th47;
then P1 is_outside_component_of A & P1 c= UBD A by A12,A6,Th14,Th48;
hence thesis by A13,XBOOLE_0:def 10;
end;
suppose
A35: C={};
REAL n c= the carrier of Euclid n;
then reconsider W=REAL n as Subset of Euclid n;
W /\ A={} by A35;
then
A36: W misses A;
reconsider P=W as Subset of TOP-REAL n by TOPREAL3:8;
reconsider P as Subset of TOP-REAL n;
the carrier of (TOP-REAL n) | A`=A` by PRE_TOPC:8;
then reconsider P1=Component_of Down(P,A`) as Subset of TOP-REAL n by
XBOOLE_1:1;
[#](TOP-REAL n) is a_component;
then
A37: [#](the TopStruct of TOP-REAL n) is a_component by CONNSP_1:45;
W is not bounded by A1,Th20,XXREAL_0:2;
then
A38: P1 is_outside_component_of A by A36,Th19,Th48;
A={}(TOP-REAL n) by A35;
then
A39: UBD A=REAL n by A1,Th23,XXREAL_0:2;
[#](TOP-REAL n)=REAL n & (TOP-REAL n) | [#](TOP-REAL n)=the TopStruct
of TOP-REAL n by EUCLID:22,TSEP_1:93;
hence UBD A is_outside_component_of A by A35,A38,A39,A37,CONNSP_3:7;
end;
end;
theorem Th54:
for a being Real, P being Subset of TOP-REAL n st P={q : (|.q.|)
< a } holds P is convex
proof
let a be Real, P be Subset of TOP-REAL n;
assume
A1: P={q : (|.q.|) < a };
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 that
A2: p1 in P and
A3: p2 in P;
A4: ex q2 st q2=p2 & (|.q2.|) < a by A1,A3;
A5: ex q1 st q1=p1 & (|.q1.|) < a by A1,A2;
LSeg(p1,p2) c= P
proof
let x be object;
assume
A6: x in LSeg(p1,p2);
then consider r such that
A7: x=(1-r)*p1+r*p2 and
A8: 0<=r and
A9: r<=1;
A10: |.(1-r)*p1.|=|.1-r.|*|.p1.| by TOPRNS_1:7;
reconsider q=x as Point of TOP-REAL n by A6;
A11: |.(1-r)*p1+r*p2.|<=|.(1-r)*p1.|+|.r*p2.| by TOPRNS_1:29;
A12: 1-r>=0 by A9,XREAL_1:48;
then
A13: |.1-r.|=1-r by ABSVALUE:def 1;
per cases;
suppose
A14: 1-r>0;
A15: |.r*p2.|=|.r.|*|.p2.| & r=|.r.| by A8,ABSVALUE:def 1,TOPRNS_1:7;
0<=|.r.| by COMPLEX1:46;
then
A16: |.r.|*|.p2.|<=|.r.|*a by A4,XREAL_1:64;
|.1-r.|*|.p1.|<|.1-r.|*a by A5,A13,A14,XREAL_1:68;
then |.(1-r)*p1.|+|.r*p2.|<(1-r)*a+r*a by A10,A13,A16,A15,XREAL_1:8;
then (|.q.|)=0 by A11,XREAL_1:48;
then
A15: |.1-r.|=1-r by ABSVALUE:def 1;
per cases;
suppose
A16: 1-r>0;
A17: |.r*(p-p2).|=|.r.|*|.p-p2.| & r=|.r.| by A10,ABSVALUE:def 1,TOPRNS_1:7;
0<=|.r.| by COMPLEX1:46;
then
A18: |.r.|*|.p-p2.|<=|.r.|*a by A5,XREAL_1:64;
|.1-r.|*|.p-p1.|<|.1-r.|*a by A7,A15,A16,XREAL_1:68;
then |.(1-r)*(p-p1).|+|.r*(p-p2).|<(1-r)*a+r*a by A12,A15,A18,A17,
XREAL_1:8;
then (|.p-q.|) q & p in Ball(u,r) & q in Ball(u,r) implies ex h being
Function of I[01],TOP-REAL n st h is continuous & h.0=p & h.1=q & rng h c= Ball
(u,r)
proof
assume that
A1: p<>q and
A2: p in Ball(u,r) & q in Ball(u,r);
reconsider Q=Ball(u,r) as Subset of TOP-REAL n by TOPREAL3:8;
Q is convex by Th55;
then
A3: LSeg(p,q) c= Ball(u,r) by A2,JORDAN1:def 1;
reconsider P=LSeg(p,q) as Subset of TOP-REAL n;
LSeg(p,q) is_an_arc_of p,q by A1,TOPREAL1:9;
then consider f being Function of I[01], (TOP-REAL n) |P such that
A4: f is being_homeomorphism and
A5: f.0 = p & f.1 = q by TOPREAL1:def 1;
reconsider h=f as Function of I[01],TOP-REAL n by JORDAN6:3;
take h;
rng f = [#]((TOP-REAL n) |P) & f is continuous by A4;
hence thesis by A3,A5,JORDAN6:3,PRE_TOPC:def 5;
end;
theorem Th57:
for f being Function of I[01],TOP-REAL n st f is continuous & f.
0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) ex h being Function of I[01],
TOP-REAL n st h is continuous & h.0=p1 & h.1=p & rng h c= rng f \/ Ball(u,r)
proof
let f be Function of I[01],TOP-REAL n;
assume that
A1: f is continuous & f.0=p1 & f.1=p2 and
A2: p in Ball(u,r) & p2 in Ball(u,r);
per cases;
suppose
p2<>p;
then LSeg(p2,p) is_an_arc_of p2,p by TOPREAL1:9;
then consider
f1 being Function of I[01], (TOP-REAL n) | LSeg(p2,p) such that
A3: f1 is being_homeomorphism and
A4: f1.0 = p2 & f1.1 = p by TOPREAL1:def 1;
reconsider f2=f1 as Function of I[01],TOP-REAL n by JORDAN6:3;
rng f1 = [#]((TOP-REAL n) | LSeg(p2,p)) by A3;
then rng f2=LSeg(p2,p) by PRE_TOPC:def 5;
then
A5: rng f \/ rng f2 c= rng f \/ Ball(u,r) by A2,TOPREAL3:21,XBOOLE_1:9;
f1 is continuous by A3;
then f2 is continuous by JORDAN6:3;
then
ex h3 being Function of I[01],(TOP-REAL n) st h3 is continuous & p1=h3
.0 & p=h3.1 & rng h3 c= rng f \/ rng f2 by A1,A4,BORSUK_2:13;
hence thesis by A5,XBOOLE_1:1;
end;
suppose
p2=p;
hence thesis by A1,XBOOLE_1:7;
end;
end;
theorem Th58:
for f being Function of I[01],TOP-REAL n st f is continuous &
rng f c=P & f.0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) & Ball(u,r) c= P
ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= P & f1
.0=p1 & f1.1=p
proof
let f be Function of I[01],TOP-REAL n;
assume f is continuous & rng f c= P & f.0=p1 & f.1=p2 & p in Ball(u,r) & p2
in Ball(u,r) & Ball(u,r) c= P;
then
(ex f3 being Function of I[01],TOP-REAL n st f3 is continuous & f3.0=p1
& f3.1=p & rng f3 c= rng f \/ Ball(u,r) )& rng f \/ Ball(u,r) c= P by Th57,
XBOOLE_1:8;
hence thesis by XBOOLE_1:1;
end;
theorem Th59:
for p for P being Subset of TOP-REAL n st R is connected & R is
open & P = {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f
is continuous & rng f c= R & f.0=p & f.1=q} holds P is open
proof
let p;
let P be Subset of TOP-REAL n;
assume that
A1: R is connected & R is open and
A2: P = {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n
st f is continuous & rng f c= R & f.0=p & f.1=q};
A3: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider P9=P as Subset of TopSpaceMetr(Euclid n);
A4: P c= R
proof
let x be object;
assume x in P;
then
ex q st q=x & q<>p & q in R & not ex f being Function of I[01],TOP-REAL
n st f is continuous & rng f c= R & f.0=p & f.1=q by A2;
hence thesis;
end;
now
A5: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider R9=R as Subset of TopSpaceMetr(Euclid n);
let u;
reconsider p2=u as Point of TOP-REAL n by TOPREAL3:8;
assume
A6: u in P;
R9 is open by A1,A5,PRE_TOPC:30;
then consider r be Real such that
A7: r>0 and
A8: Ball(u,r) c= R9 by A4,A6,TOPMETR:15;
take r;
thus r>0 by A7;
reconsider r9=r as Real;
A9: p2 in Ball(u,r9) by A7,TBSP_1:11;
Ball(u,r) c= P9
proof
assume not thesis;
then consider x being object such that
A10: x in Ball(u,r) and
A11: not x in P;
x in R by A8,A10;
then reconsider q=x as Point of TOP-REAL n;
per cases by A2,A8,A10,A11;
suppose
A12: q=p;
A13: now
assume
A14: q=p2;
ex p3 st p3=p2 & p3<>p & p3 in R & not ex f1 being Function of
I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=p3 by A2,A6;
hence contradiction by A12,A14;
end;
u in Ball(u,r9) by A7,TBSP_1:11;
then
A15: ex f2 being Function of I[01],TOP-REAL n st f2 is continuous & f2.
0=q & f2.1=p2 & rng f2 c= Ball(u,r9) by A10,A13,Th56;
not p2 in P
proof
assume p2 in P;
then ex q4 st q4=p2 & q4<>p & q4 in R & not ex f1 being Function of
I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=q4 by A2;
hence contradiction by A8,A12,A15,XBOOLE_1:1;
end;
hence contradiction by A6;
end;
suppose
A16: ex f1 being Function of I[01],TOP-REAL n st f1 is continuous
& rng f1 c= R & f1.0=p & f1.1=q;
not p2 in P
proof
assume p2 in P;
then ex q4 st q4=p2 & q4<>p & q4 in R & not ex f1 being Function of
I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=q4 by A2;
hence contradiction by A8,A9,A10,A16,Th58;
end;
hence contradiction by A6;
end;
end;
hence Ball(u,r) c= P9;
end;
then P9 is open by TOPMETR:15;
hence thesis by A3,PRE_TOPC:30;
end;
theorem Th60:
for P being Subset of TOP-REAL n st R is connected & R is open &
p in R & P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q} holds P is open
proof
let P be Subset of TOP-REAL n;
assume that
A1: R is connected & R is open and
A2: p in R and
A3: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q};
A4: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider P9=P as Subset of TopSpaceMetr(Euclid n);
reconsider RR=R as Subset of TopSpaceMetr(Euclid n) by A4;
now
let u;
reconsider p2=u as Point of TOP-REAL n by TOPREAL3:8;
assume u in P9;
then consider q1 such that
A5: q1=u and
A6: q1=p or ex f being Function of I[01],TOP-REAL n st f is continuous
& rng f c= R & f.0=p & f.1=q1 by A3;
A7: now
per cases by A6;
suppose
q1=p;
hence p2 in R by A2,A5;
end;
suppose
q1<>p & ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q1;
then consider f2 being Function of I[01],TOP-REAL n such that
f2 is continuous and
A8: rng f2 c= R and
f2.0=p and
A9: f2.1=q1;
dom f2=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then 1 in dom f2 by XXREAL_1:1;
then u in rng f2 by A5,A9,FUNCT_1:def 3;
hence p2 in R by A8;
end;
end;
RR is open by A1,A4,PRE_TOPC:30;
then consider r be Real such that
A10: r>0 and
A11: Ball(u,r) c= R by A7,TOPMETR:15;
take r;
thus r>0 by A10;
reconsider r9=r as Real;
A12: p2 in Ball(u,r9) by A10,TBSP_1:11;
thus Ball(u,r) c= P
proof
let x be object;
assume
A13: x in Ball(u,r);
then reconsider q=x as Point of TOP-REAL n by A11,TARSKI:def 3;
per cases;
suppose
q=p;
hence thesis by A3;
end;
suppose
A14: q<>p;
A15: now
assume q1=p;
then p in Ball(u,r9) by A5,A10,TBSP_1:11;
then consider f2 being Function of I[01],TOP-REAL n such that
A16: f2 is continuous & f2.0=p & f2.1=q and
A17: rng f2 c= Ball(u,r9) by A13,A14,Th56;
rng f2 c= R by A11,A17;
hence thesis by A3,A16;
end;
now
assume q1<>p;
then ex f being Function of I[01],TOP-REAL n st f is continuous &
rng f c= R & f.0=p & f.1=q by A5,A6,A11,A12,A13,Th58;
hence thesis by A3;
end;
hence thesis by A15;
end;
end;
end;
then P9 is open by TOPMETR:15;
hence thesis by A4,PRE_TOPC:30;
end;
theorem Th61:
for R being Subset of TOP-REAL n holds p in R & P={q: q=p or ex
f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p &
f.1=q} implies P c= R
proof
let R be Subset of TOP-REAL n;
assume that
A1: p in R and
A2: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q};
let x be object;
assume x in P;
then consider q such that
A3: q=x and
A4: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous &
rng f c= R & f.0=p & f.1=q by A2;
per cases by A4;
suppose
q=p;
hence thesis by A1,A3;
end;
suppose
ex f being Function of I[01],TOP-REAL n st f is continuous & rng f
c= R & f.0=p & f.1=q;
then consider f1 being Function of I[01],TOP-REAL n such that
f1 is continuous and
A5: rng f1 c= R and
f1.0=p and
A6: f1.1=q;
reconsider P1=rng f1 as Subset of TOP-REAL n;
dom f1=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then 1 in dom f1 by XXREAL_1:1;
then q in P1 by A6,FUNCT_1:def 3;
hence thesis by A3,A5;
end;
end;
theorem Th62:
for R being Subset of TOP-REAL n, p being Point of TOP-REAL n st
R is connected & R is open & p in R & P={q: q=p or ex f being Function of I[01]
,TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds R c= P
proof
let R be Subset of TOP-REAL n, p be Point of TOP-REAL n;
assume that
A1: R is connected & R is open and
A2: p in R and
A3: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q};
reconsider R9 = R as non empty Subset of TOP-REAL n by A2;
A4: p in P by A3;
set P2 = R \ P;
reconsider P22=P2 as Subset of TOP-REAL n;
A5: [#]((TOP-REAL n) | R) = R by PRE_TOPC:def 5;
then reconsider P11 = P, P12 = P22 as Subset of (TOP-REAL n) | R by A2,A3
,Th61,XBOOLE_1:36;
reconsider P11, P12 as Subset of (TOP-REAL n) | R;
P \/ (R \ P) = P \/ R by XBOOLE_1:39;
then
A6: P11 misses P12 & [#]((TOP-REAL n) | R) = P11 \/ P12 by A5,XBOOLE_1:12,79;
now
let x be object;
A7: now
assume
A8: x in P2;
then reconsider q2=x as Point of TOP-REAL n;
not x in P by A8,XBOOLE_0:def 5;
then
A9: q2<>p & not ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q2 by A3;
q2 in R by A8,XBOOLE_0:def 5;
hence x in {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL
n st f is continuous & rng f c= R & f.0=p & f.1=q} by A9;
end;
now
assume x in {q: q<>p & q in R & not ex f being Function of I[01],
TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q};
then
A10: ex q3 st q3=x & q3<>p & q3 in R & not ex f being Function of I[01],
TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q3;
then not ex q st q=x & (q=p or ex f being Function of I[01],TOP-REAL n
st f is continuous & rng f c= R & f.0=p & f.1=q);
then not x in P by A3;
hence x in P2 by A10,XBOOLE_0:def 5;
end;
hence
x in P2 iff x in {q: q<>p & q in R & not ex f being Function of I[01]
,TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} by A7;
end;
then
P2={q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f
is continuous & rng f c= R & f.0=p & f.1=q} by TARSKI:2;
then P22 is open by A1,Th59;
then
A11: P22 in the topology of TOP-REAL n by PRE_TOPC:def 2;
reconsider PPP=P as Subset of TOP-REAL n;
PPP is open by A1,A2,A3,Th60;
then
A12: P in the topology of TOP-REAL n by PRE_TOPC:def 2;
P11 = P /\ [#]((TOP-REAL n) | R) by XBOOLE_1:28;
then P11 in the topology of (TOP-REAL n) | R by A12,PRE_TOPC:def 4;
then
A13: P11 is open by PRE_TOPC:def 2;
P12 = P22 /\ [#]((TOP-REAL n) | R) by XBOOLE_1:28;
then P12 in the topology of ( TOP-REAL n) | R by A11,PRE_TOPC:def 4;
then
A14: P12 is open by PRE_TOPC:def 2;
(TOP-REAL n) | R9 is connected by A1,CONNSP_1:def 3;
then P11 = {}((TOP-REAL n) | R) or P12 = {}((TOP-REAL n) | R) by A6,A13,A14,
CONNSP_1:11;
hence thesis by A4,XBOOLE_1:37;
end;
theorem Th63:
for R being Subset of TOP-REAL n, p,q being Point of TOP-REAL n
st R is connected & R is open & p in R & q in R & p<>q holds ex f being
Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q
proof
let R be Subset of TOP-REAL n, p,q be Point of TOP-REAL n;
assume that
A1: R is connected & R is open & p in R and
A2: q in R and
A3: p<>q;
set RR={q2: q2=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q2};
RR c= the carrier of TOP-REAL n
proof
let x be object;
assume x in RR;
then
ex q2 st q2=x & (q2=p or ex f being Function of I[01],TOP-REAL n st f
is continuous & rng f c= R & f.0=p & f.1=q2);
hence thesis;
end;
then R c= RR by A1,Th62;
then q in RR by A2;
then
ex q2 st q=q2 &(q2=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q2);
hence thesis by A3;
end;
theorem Th64:
for A being Subset of TOP-REAL n, a being Real st A={q:
|.q.|=a} holds A` is open & A is closed
proof
let A be Subset of TOP-REAL n, a be Real;
assume
A1: A={q: |.q.|=a};
reconsider a as Real;
A2: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider P1=A` as Subset of TopSpaceMetr(Euclid n);
for p being Point of Euclid n st p in P1 ex r be Real st r>0 &
Ball(p,r) c= P1
proof
let p be Point of Euclid n;
reconsider q1=p as Point of TOP-REAL n by TOPREAL3:8;
assume p in P1;
then not p in A by XBOOLE_0:def 5;
then
A3: |.q1.|<>a by A1;
now
per cases;
case
A4: |.q1.|<=a;
set r1=(a- |.q1.|)/2;
|.q1.|0 by XREAL_1:50;
Ball(p,r1) c= P1
proof
let x be object;
assume
A6: x in Ball(p,r1);
then reconsider p2=x as Point of Euclid n;
reconsider q2=p2 as Point of TOP-REAL n by TOPREAL3:8;
dist(p,p2)=|.q2.|- |.q1.| by TOPRNS_1:32;
then r1>r1+r1 by A7,A8,XXREAL_0:2;
then r1-r1>r1 by XREAL_1:20;
hence contradiction by A5;
end;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by A5,XREAL_1:139;
end;
case
A9: |.q1.|>a;
set r1=(|.q1.|-a)/2;
A10: |.q1.|-a>0 by A9,XREAL_1:50;
Ball(p,r1) c= P1
proof
let x be object;
assume
A11: x in Ball(p,r1);
then reconsider p2=x as Point of Euclid n;
reconsider q2=p2 as Point of TOP-REAL n by TOPREAL3:8;
dist(p,p2)=|.q1.|- |.q2.| by TOPRNS_1:32;
then r1>r1+r1 by A12,A13,XXREAL_0:2;
then r1-r1>r1 by XREAL_1:20;
hence contradiction by A10;
end;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by A10,XREAL_1:139;
end;
end;
hence thesis;
end;
then P1 is open by TOPMETR:15;
hence A` is open by A2,PRE_TOPC:30;
hence thesis by TOPS_1:3;
end;
theorem Th65:
for B being non empty Subset of TOP-REAL n st B is open holds
(TOP-REAL n) | B is locally_connected
proof
let B be non empty Subset of TOP-REAL n;
A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
assume
A2: B is open;
for A being non empty Subset of ((TOP-REAL n) | B), C being Subset of ((
TOP-REAL n) | B) st A is open & C is_a_component_of A holds C is open
proof
let A be non empty Subset of (TOP-REAL n) | B,
C be Subset of (TOP-REAL n) | B;
assume that
A3: A is open and
A4: C is_a_component_of A;
consider C1 being Subset of ((TOP-REAL n) | B) | A such that
A5: C1 = C and
A6: C1 is a_component by A4,CONNSP_1:def 6;
C1 c= [#](((TOP-REAL n) | B) |A);
then
A7: C1 c= A by PRE_TOPC:def 5;
A c= the carrier of (TOP-REAL n) | B;
then A c= B by PRE_TOPC:8;
then C c= B by A5,A7;
then reconsider C0=C as Subset of TOP-REAL n by XBOOLE_1:1;
reconsider CC = C0 as Subset of TopSpaceMetr Euclid n by A1;
for p being Point of Euclid n st p in C0 ex r be Real st r>0 &
Ball(p,r) c= C0
proof
consider A0 being Subset of TOP-REAL n such that
A8: A0 is open and
A9: A0 /\ [#]((TOP-REAL n) | B) = A by A3,TOPS_2:24;
A10: A0 /\ B=A by A9,PRE_TOPC:def 5;
A11: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider AA=A0 /\ B as Subset of TopSpaceMetr Euclid n;
let p be Point of Euclid n;
assume
A12: p in C0;
AA is open by A2,A8,A11,PRE_TOPC:30;
then consider r1 being Real such that
A13: r1>0 and
A14: Ball(p,r1) c= AA by A5,A7,A12,A10,TOPMETR:15;
reconsider r1 as Real;
A15: Ball(p,r1) c= A by A9,A14,PRE_TOPC:def 5;
then reconsider BL2=Ball(p,r1) as Subset of (TOP-REAL n) | B by
XBOOLE_1:1;
Ball(p,r1) c= [#](((TOP-REAL n) | B) |A) by A15,PRE_TOPC:def 5;
then reconsider BL=Ball(p,r1) as Subset of ((TOP-REAL n) | B) |A;
reconsider BL as Subset of ((TOP-REAL n) | B) |A;
reconsider BL2 as Subset of (TOP-REAL n) | B;
reconsider BL1=Ball(p,r1) as Subset of TOP-REAL n by TOPREAL3:8;
reconsider BL1 as Subset of TOP-REAL n;
now
p in BL by A13,GOBOARD6:1;
then BL /\ C <>{}(((TOP-REAL n) | B) |A) by A12,XBOOLE_0:def 4;
then
A16: BL meets C;
BL1 is convex by Th55;
then
A17: BL2 is connected by CONNSP_1:46;
assume not Ball(p,r1) c= C0;
hence contradiction by A5,A6,A17,A16,CONNSP_1:36,46;
end;
hence thesis by A13;
end;
then CC is open by TOPMETR:15;
then
A18: [#]((TOP-REAL n) | B)=B & C0 is open by A1,PRE_TOPC:30,def 5;
C c= the carrier of ((TOP-REAL n) | B);
then C c= B by PRE_TOPC:8;
then C0 /\ B=C by XBOOLE_1:28;
hence thesis by A18,TOPS_2:24;
end;
hence thesis by CONNSP_2:18;
end;
theorem Th66:
for B being non empty Subset of TOP-REAL n, A being Subset of
TOP-REAL n,a being Real st A={q: |.q.|=a} & A`=B holds
(TOP-REAL n) | B is locally_connected
proof
let B be non empty Subset of TOP-REAL n, A be Subset of TOP-REAL n,a be Real;
assume
A1: A={q: |.q.|=a} & A`=B;
then A` is open by Th64;
hence thesis by A1,Th65;
end;
theorem Th67:
for f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.|
) holds f is continuous
proof
let f be Function of TOP-REAL n,R^1;
A1: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider
f1=f as Function of TopSpaceMetr(Euclid n),TopSpaceMetr(RealSpace
) by TOPMETR:def 6;
assume
A2: for q holds f.q=|.q.|;
now
let r be Real,u be Element of Euclid n,u1 be Element
of RealSpace;
assume that
A3: r>0 and
A4: u1=f1.u;
set s1=r;
for w being Element of Euclid n, w1 being Element of RealSpace st w1=
f1.w & dist(u,w)0 & for w being Element of Euclid n, w1
being Element of RealSpace st w1=f1.w & dist(u,w)~~ implies |.q.|=|.r.|
proof
assume
A1: q=<*r*>;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
reconsider xr=<*rr*> as Element of REAL 1;
reconsider qk = (q/.1)^2 as Element of REAL by XREAL_0:def 1;
len xr=1 by FINSEQ_1:39;
then
A2: q/.1=xr.1 by A1,FINSEQ_4:15;
then len (sqr xr) =1 & (sqr xr).1=(q/.1)^2 by CARD_1:def 7,VALUED_1:11;
then
A3: sqr xr=<*qk*> by FINSEQ_1:40;
sqrt (q/.1)^2 =|.q/.1.| by COMPLEX1:72
.=|.r.| by A2,FINSEQ_1:40;
then |.xr.|=|.rr.| by A3,FINSOP_1:11;
hence thesis by A1;
end;
theorem
for A being Subset of TOP-REAL n,a being Real st n>=1 & a>0 & A={q: |.
q.|=a} holds BDD A is_inside_component_of A
proof
let A be Subset of TOP-REAL n,a be Real;
{q where q is Point of TOP-REAL n: (|.q.|) ~~~~=1 & a>0 & A={q: |.q.|=a};
A3: P c= A`
proof
let x be object;
assume
A4: x in P;
then reconsider q=x as Point of TOP-REAL n;
A5: ex q1 st q1=q & |.q1.|{} by A3,A8,XBOOLE_0:def 4;
then
A12: Component_of (Down(P,A`)) is a_component by A9,A7,CONNSP_3:9;
then
A13: Component_of (Down(P,A`)) is connected by CONNSP_1:def 5;
Component_of (Down(P,A`)) is bounded Subset of Euclid n
proof
reconsider D2=Component_of (Down(P,A`)) as Subset of TOP-REAL n by A1,
XBOOLE_1:1;
reconsider D=D2 as Subset of Euclid n by TOPREAL3:8;
reconsider D as Subset of Euclid n;
now
reconsider B=A` as non empty Subset of TOP-REAL n by A3,A8;
set p=0.TOP-REAL n;
reconsider RR=(TOP-REAL n) | B as non empty TopSpace;
assume not D2 is bounded;
then consider q such that
A14: q in D2 and
A15: |.q.|>=a by Th21;
A16: A` is open & D2 is connected by A2,A13,Th64,CONNSP_1:23;
D c= the carrier of (TOP-REAL n) | A`;
then
A17: D2 c= A` by PRE_TOPC:8;
then
A18: D2=Down(D2,A`) by XBOOLE_1:28;
RR is locally_connected by A2,Th66;
then Component_of (Down(P,A`)) is open by A11,A7,CONNSP_2:15,CONNSP_3:9;
then consider G being Subset of TOP-REAL n such that
A19: G is open and
A20: Down(D2,A`)=G /\ [#]((TOP-REAL n) | A`) by A18,TOPS_2:24;
A21: G /\ A` = D2 by A18,A20,PRE_TOPC:def 5;
p <> q by A2,A15,TOPRNS_1:23;
then consider f1 being Function of I[01],TOP-REAL n such that
A22: f1 is continuous and
A23: rng f1 c= D2 and
A24: f1.0=p and
A25: f1.1=q by A8,A10,A14,A19,A21,A16,Th63;
A26: |.f1/.1.|>=a by A15,A25,BORSUK_1:def 15,FUNCT_2:def 13;
|.p.|{}(the carrier of TOP-REAL n) by A17,A28,XBOOLE_0:def 4;
then A meets A`;
hence contradiction by XBOOLE_1:79;
end;
hence thesis by Th5;
end;
then
A29: P1 is_inside_component_of A by A12,Th7;
A30: P1 c= union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}
proof
let x be object;
assume
A31: x in P1;
P1 in {B where B is Subset of TOP-REAL n: B is_inside_component_of A}
by A29;
hence thesis by A31,TARSKI:def 4;
end;
now
per cases;
case
A32: n>=2;
union{B where B is Subset of TOP-REAL n: B is_inside_component_of A
} c= P1
proof
reconsider E=A` as non empty Subset of TOP-REAL n by A3,A8;
let x be object;
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
A33: x in y and
A34: 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
A35: B=y and
A36: B is_inside_component_of A by A34;
ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C
is a_component & C is bounded Subset of Euclid n
by A36,Th7;
then reconsider p=x as Point of (TOP-REAL n) | A` by A33,A35;
A37: the carrier of (TOP-REAL n) | A`=A` & p in the carrier of ((
TOP-REAL n) |E) by PRE_TOPC:8;
then reconsider q2=p as Point of TOP-REAL n;
not p in A by A37,XBOOLE_0:def 5;
then |.q2.|<>a by A2;
then
A38: |.q2.|a by XXREAL_0:1;
now
per cases by A38;
case
A39: p in {q: |.q.|>a};
{q: |.q.|>a} c= A`
proof
let z be object;
assume z in {q: |.q.|>a};
then consider q such that
A40: q=z and
A41: |.q.|>a;
now
assume q in A;
then ex q2 st q2=q & |.q2.|=a by A2;
hence contradiction by A41;
end;
hence thesis by A40,XBOOLE_0:def 5;
end;
then reconsider Q={q: |.q.|>a} as Subset of (TOP-REAL n) | A` by
PRE_TOPC:8;
reconsider Q as Subset of (TOP-REAL n) | A`;
{q: |.q.|>a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q: |.q.|>a};
then ex q st q=z & |.q.|>a;
hence thesis;
end;
then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n;
P2 is Subset of Euclid n by TOPREAL3:8;
then reconsider W2={q: |.q.|>a} as Subset of Euclid n;
P2 is connected by A32,Th38;
then
A42: (TOP-REAL n) |P2 is connected by CONNSP_1:def 3;
A43: not W2 is bounded by A32,Th46;
A44: now
assume W2 meets A;
then consider z being object such that
A45: z in W2 & z in A by XBOOLE_0:3;
( ex q st q=z & |.q.|>a)& ex q2 st q2=z & |.q2.|=a by A2,A45;
hence contradiction;
end;
then W2 /\ A``={};
then P2\A`={} by SUBSET_1:13;
then
A46: W2 c= A` by XBOOLE_1:37;
then Q=Down(P2,A`) by XBOOLE_1:28;
then Up(Component_of Q) is_outside_component_of A by A32,A43,A44
,Th38,Th48;
then
A47: Component_of Q c= UBD A by Th14;
(TOP-REAL n) |P2=((TOP-REAL n) | A`) |Q by A46,PRE_TOPC:7;
then Q is connected by A42,CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then
A48: p in Component_of Q by A39;
B c= BDD A by A36,Th13;
then p in (BDD A) /\ (UBD A) by A33,A35,A47,A48,XBOOLE_0:def 4;
then (BDD A) meets (UBD A);
hence thesis by Th15;
end;
case
A49: p in {q1: |.q1.|a by A2;
then
A57: |.q2.|~~a by XXREAL_0:1;
now
per cases by A57;
case
p in {q: |.q.|>a};
then consider q0 being Point of TOP-REAL n such that
A58: q0=p and
A59: |.q0.|>a;
q0 is Element of REAL n by EUCLID:22;
then consider r0 being Element of REAL such that
A60: q0=<*r0*> by A51,FINSEQ_2:97;
A61: |.q0.|=|.r0.| by A60,Th71;
A62: now
per cases;
suppose r0>=0;
then r0=|.r0.| by ABSVALUE:def 1;
hence
p in {q:ex r st q=<*r*> & r>a} or p in {q1:ex r1 st q1=<*
r1*> & r1< -a} by A58,A59,A60,A61;
end;
suppose r0<0;
then -r0>a by A59,A61,ABSVALUE:def 1;
then --r0< -a by XREAL_1:24;
hence
p in {q:ex r st q=<*r*> & r>a} or p in {q1:ex r1 st q1=<*
r1*> & r1< -a} by A58,A60;
end;
end;
now
per cases by A62;
suppose
A63: p in {q:ex r st q=<*r*> & r>a};
{q:ex r st q=<*r*> & r>a} c= A`
proof
let z be object;
assume z in {q:ex r st q=<*r*> & r>a};
then consider q such that
A64: q=z and
A65: ex r st q=<*r*> & r>a;
consider r such that
A66: q=<*r*> and
A67: r>a by A65;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
n=1 by A2,A50,XXREAL_0:1;
then reconsider xr=<*rr*> as Element of REAL n;
len xr=1 by FINSEQ_1:39;
then
A68: q/.1=xr.1 by A66,FINSEQ_4:15;
then
A69: (sqr xr).1=(q/.1)^2 by VALUED_1:11;
A70: sqrt ((q/.1)^2) =|.q/.1.| by COMPLEX1:72
.=|.r.| by A68,FINSEQ_1:40;
reconsider qk = (q/.1)^2 as Element of REAL by XREAL_0:def 1;
len sqr xr =1 by A51,CARD_1:def 7;
then sqr xr=<*qk*> by A69,FINSEQ_1:40;
then
A71: |.q.|=|.r.| by A66,A70,FINSOP_1:11
.=r by A2,A67,ABSVALUE:def 1;
now
assume q in A;
then ex q2 st q2=q & |.q2.|=a by A2;
hence contradiction by A67,A71;
end;
hence thesis by A64,XBOOLE_0:def 5;
end;
then reconsider
Q={q:ex r st q=<*r*> & r>a} as Subset of (TOP-REAL
n) |A` by PRE_TOPC:8;
{q:ex r st q=<*r*> & r>a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q:ex r st q=<*r*> & r>a};
then ex q st q=z & ex r st q=<*r*> & r>a;
hence thesis;
end;
then reconsider
P3={q: ex r st q=<*r*> & r>a} as Subset of TOP-REAL
n;
reconsider W3=P3 as Subset of Euclid n by TOPREAL3:8;
reconsider Q as Subset of (TOP-REAL n) | A`;
{q: |.q.|>a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q: |.q.|>a};
then ex q st q=z & |.q.|>a;
hence thesis;
end;
then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n;
P2 is Subset of Euclid n by TOPREAL3:8;
then reconsider W2={q: |.q.|>a} as Subset of Euclid n;
A72: W3 c= W2
proof
let z be object;
assume z in W3;
then consider q such that
A73: q=z and
A74: ex r st q=<*r*> & r>a;
consider r such that
A75: q=<*r*> and
A76: r>a by A74;
A77: r=|.r.| by A2,A76,ABSVALUE:def 1;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
n=1 by A2,A50,XXREAL_0:1;
then reconsider xr=<*rr*> as Element of REAL n;
len xr=1 by FINSEQ_1:39;
then
A78: q/.1=xr.1 by A75,FINSEQ_4:15;
then
A79: (sqr xr).1=(q/.1)^2 by VALUED_1:11;
reconsider qk = (q/.1)^2 as Element of REAL by XREAL_0:def 1;
len sqr xr =1 by A51,CARD_1:def 7;
then
A80: sqr xr=<*qk*> by A79,FINSEQ_1:40;
sqrt (q/.1)^2 =|.q/.1.| by COMPLEX1:72
.=|.r.| by A78,FINSEQ_1:40;
then |.xr.|=|.rr.| by A80,FINSOP_1:11;
then |.q.|=|.r.| by A75;
hence thesis by A73,A76,A77;
end;
A81: now
set z = the Element of W2 /\ A;
assume
A82: not W2 /\ A={};
then z in W2 by XBOOLE_0:def 4;
then
A83: ex q st q=z & |.q.|>a;
z in A by A82,XBOOLE_0:def 4;
then ex q2 st q2=z & |.q2.|=a by A2;
hence contradiction by A83;
end;
then W3 /\ A={} by A72,XBOOLE_1:3,26;
then
A84: W3 misses A;
W3 /\ A``={} by A81,A72,XBOOLE_1:3,26;
then W3\A`={} by SUBSET_1:13;
then
A85: W3 c= A` by XBOOLE_1:37;
then
A86: (TOP-REAL n) |P3=((TOP-REAL n) | A`) |Q by PRE_TOPC:7;
A87: P3 is convex by A51,Th42;
then (TOP-REAL n) |P3 is connected by CONNSP_1:def 3;
then Q is connected by A86,CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then
A88: p in Component_of Q by A63;
A89: Q=Down(P3,A`) by A85,XBOOLE_1:28;
not W3 is bounded by A51,Th44;
then Up(Component_of Q) is_outside_component_of A
by A87,A84,A89,Th48;
then
A90: Component_of Q c= UBD A by Th14;
B c= BDD A by A55,Th13;
then (BDD A) /\ (UBD A)<>{} by A52,A54,A90,A88,XBOOLE_0:def 4;
then (BDD A) meets (UBD A);
hence thesis by Th15;
end;
suppose
A91: p in {q1:ex r1 st q1=<*r1*> & r1< -a};
{q:ex r st q=<*r*> & r< -a} c= A`
proof
let z be object;
assume z in {q:ex r st q=<*r*> & r< -a};
then consider q such that
A92: q=z and
A93: ex r st q=<*r*> & r< -a;
consider r such that
A94: q=<*r*> and
A95: r< -a by A93;
A96: r< -0 by A2,A95;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
n=1 by A2,A50,XXREAL_0:1;
then reconsider xr=<*rr*> as Element of REAL n;
len xr=1 by FINSEQ_1:39;
then
A97: q/.1=xr.1 by A94,FINSEQ_4:15;
then
A98: (sqr xr).1=(q/.1)^2 by VALUED_1:11;
reconsider qk = (q/.1)^2 as Element of REAL by XREAL_0:def 1;
len (sqr xr) =1 by A51,CARD_1:def 7;
then
A99: sqr xr=<*qk*> by A98,FINSEQ_1:40;
sqrt (q/.1)^2 =|.q/.1.| by COMPLEX1:72
.=|.r.| by A97,FINSEQ_1:40;
then
A100: |.q.|=|.r.| by A94,A99,FINSOP_1:11
.=-r by A96,ABSVALUE:def 1;
now
assume q in A;
then ex q2 st q2=q & |.q2.|=a by A2;
hence contradiction by A95,A100;
end;
hence thesis by A92,XBOOLE_0:def 5;
end;
then reconsider Q={q:ex r st q=<*r*> & r< -a} as Subset of (
TOP-REAL n) |A` by PRE_TOPC:8;
{q:ex r st q=<*r*> & r< -a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q:ex r st q=<*r*> & r< -a};
then ex q st q=z & ex r st q=<*r*> & r< -a;
hence thesis;
end;
then reconsider P3={q: ex r st q=<*r*> & r< -a} as Subset of
TOP-REAL n;
reconsider W3=P3 as Subset of Euclid n by TOPREAL3:8;
reconsider Q as Subset of (TOP-REAL n) | A`;
{q: |.q.|>a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q: |.q.|>a};
then ex q st q=z & |.q.|>a;
hence thesis;
end;
then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n;
P2 is Subset of Euclid n by TOPREAL3:8;
then reconsider W2={q: |.q.|>a} as Subset of Euclid n;
A101: W3 c= W2
proof
let z be object;
assume z in W3;
then consider q such that
A102: q=z and
A103: ex r st q=<*r*> & r< -a;
consider r such that
A104: q=<*r*> and
A105: r< -a by A103;
A106: r< -0 & -r>--a by A2,A105,XREAL_1:24;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
n=1 by A2,A50,XXREAL_0:1;
then reconsider xr=<*rr*> as Element of REAL n;
len xr=1 by FINSEQ_1:39;
then
A107: q/.1=xr.1 by A104,FINSEQ_4:15;
then
A108: (sqr xr).1=(q/.1)^2 by VALUED_1:11;
reconsider qk = (q/.1)^2 as Element of REAL by XREAL_0:def 1;
len sqr xr =1 by A51,CARD_1:def 7;
then
A109: sqr xr=<*qk*> by A108,FINSEQ_1:40;
sqrt (q/.1)^2 =|.q/.1.| by COMPLEX1:72
.=|.r.| by A107,FINSEQ_1:40;
then |.q.|=|.r.| by A104,A109,FINSOP_1:11;
then |.q.|>a by A106,ABSVALUE:def 1;
hence thesis by A102;
end;
A110: now
set z = the Element of W2 /\ A;
assume
A111: not W2 /\ A={};
then z in W2 by XBOOLE_0:def 4;
then
A112: ex q st q=z & |.q.|>a;
z in A by A111,XBOOLE_0:def 4;
then ex q2 st q2=z & |.q2.|=a by A2;
hence contradiction by A112;
end;
then W3 /\ A={} by A101,XBOOLE_1:3,26;
then
A113: W3 misses A;
W3 /\ A``={} by A110,A101,XBOOLE_1:3,26;
then W3\A`={} by SUBSET_1:13;
then
A114: W3 c= A` by XBOOLE_1:37;
then
A115: (TOP-REAL n) |P3=((TOP-REAL n) | A`) |Q by PRE_TOPC:7;
A116: P3 is convex by A51,Th43;
then (TOP-REAL n) |P3 is connected by CONNSP_1:def 3;
then Q is connected by A115,CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then
A117: p in Component_of Q by A91;
A118: Q=Down(P3,A`) by A114,XBOOLE_1:28;
Up(Component_of Q) is_outside_component_of A
by A116,A113,A118,Th48,A51,Th45;
then
A119: Component_of Q c= UBD A by Th14;
B c= BDD A by A55,Th13;
then p in (BDD A) /\ (UBD A) by A52,A54,A119,A117,
XBOOLE_0:def 4;
then (BDD A) meets (UBD A);
hence thesis by Th15;
end;
end;
hence thesis;
end;
case
A120: p in {q1: |.q1.|len (GoB f1) +1 by A27,GOBOARD2:13,XREAL_1:29;
2 in dom (Y_axis(f1)) by A18,SPRECT_2:16;
then (Y_axis(f1)).2=(f1/.2)`2 by GOBOARD1:def 2;
then
A31: (Y_axis(f1)).2=N-bound L~f1 by A28,EUCLID:52;
f1/.5=f1/.1 by A4,FINSEQ_6:def 1;
then
A32: (Y_axis(f1)).5=N-bound L~f1 by A14,A6,EUCLID:52;
A33: rng (Y_axis(f1)) c= {S-bound L~f1,N-bound L~f1}
proof
let z be object;
assume z in rng (Y_axis(f1));
then consider u being object such that
A34: u in dom (Y_axis(f1)) and
A35: z=(Y_axis(f1)).u by FUNCT_1:def 3;
reconsider mu=u as Element of NAT by A34;
u in dom f1 by A34,SPRECT_2:16;
then u in Seg len f1 by FINSEQ_1:def 3;
then 1<=mu & mu<=5 by A4,FINSEQ_1:1;
then
A36: mu=1+0 or ... or mu=1+4 by NAT_1:62;
per cases by A36;
suppose
mu=1;
hence thesis by A23,A35,TARSKI:def 2;
end;
suppose
mu=2;
hence thesis by A31,A35,TARSKI:def 2;
end;
suppose
mu=3;
hence thesis by A10,A35,TARSKI:def 2;
end;
suppose
mu=4;
hence thesis by A8,A35,TARSKI:def 2;
end;
suppose
mu=5;
hence thesis by A32,A35,TARSKI:def 2;
end;
end;
{S-bound L~f1,N-bound L~f1} c= rng (Y_axis(f1))
proof
let z be object;
assume
A37: z in {S-bound L~f1,N-bound L~f1};
per cases by A37,TARSKI:def 2;
suppose
A38: z=S-bound L~f1;
4 in dom (Y_axis(f1)) by A7,SPRECT_2:16;
hence thesis by A8,A38,FUNCT_1:def 3;
end;
suppose
A39: z=N-bound L~f1;
2 in dom (Y_axis(f1)) by A18,SPRECT_2:16;
hence thesis by A31,A39,FUNCT_1:def 3;
end;
end;
then
A40: S-bound L~f1 < N-bound L~f1 & rng (Y_axis(f1))={S-bound L~f1,N-bound L~
f1} by A33,SPRECT_1:32;
A41: width GoB(f1) = card rng Y_axis(f1) by GOBOARD2:13
.=1+1 by A40,CARD_2:57;
then
A42: width GoB f1 in Seg (width GoB f1) by FINSEQ_1:1;
f1/.(1+1) = E-max L~f1 by SPRECT_1:84;
then
A43: f/.2=|[(E-max L~f)`1,(N-max L~f)`2]| by A28,EUCLID:53;
A44: f1/.1 = W-max L~f1 by SPRECT_1:83;
then f/.1=|[(W-max L~f)`1,(N-min L~f)`2]| by A14,EUCLID:53;
then f/.1+f/.2=|[(W-max L~f)`1 +(E-max L~f)`1, (N-min L~f)`2+(N-max L~f)`2
]| by A43,EUCLID:56;
then (1/2)*(f/.1+f/.2)= |[1/2*((W-max L~f)`1 +(E-max L~f)`1),N-bound L~f]|
by A3,EUCLID:58;
then
A45: q1=|[0+1/2*((W-max L~f)`1 +(E-max L~f)`1),r1+r+1+(N-bound L~f)]| by
EUCLID:56
.=|[1/2*((W-max L~f)`1 +(E-max L~f)`1),r1+r+1+(N-bound L~f)]|;
(W-max L~f)`1=W-bound L~f by EUCLID:52;
then
A46: (W-max L~f)`1<(E-max L~f)`1 by A1,EUCLID:52;
A47: f1/.1=W-max L~f1 by SPRECT_1:83;
then
A48: (GoB f1)*(1,1)`1<=(W-max L~f)`1 by A4,A41,JORDAN5D:5;
then (GoB f1)*(1,1)`1<(E-max L~f)`1 by A46,XXREAL_0:2;
then (GoB f1)*(1,1)`1 +(GoB f1)*(1,1)`1<(W-max L~f)`1+(E-max L~f)`1 by A48,
XREAL_1:8;
then
A49: 1/2*(2*((GoB f1)*(1,1)`1))<1/2*((W-max L~f)`1+(E-max L~f)`1) by XREAL_1:68
;
1 in dom (X_axis(f1)) by A22,SPRECT_2:15;
then (X_axis(f1)).1=(f1/.1)`1 by GOBOARD1:def 1;
then
A50: (X_axis(f1)).1=W-bound L~f1 by A47,EUCLID:52;
f1/.5=W-max L~f1 by A4,A44,FINSEQ_6:def 1;
then
A51: (X_axis(f1)).5=W-bound L~f1 by A12,EUCLID:52;
A52: rng (X_axis(f1)) c= {W-bound L~f1,E-bound L~f1}
proof
let z be object;
assume z in rng (X_axis(f1));
then consider u being object such that
A53: u in dom (X_axis(f1)) and
A54: z=(X_axis(f1)).u by FUNCT_1:def 3;
reconsider mu=u as Element of NAT by A53;
u in dom f1 by A53,SPRECT_2:15;
then u in Seg len f1 by FINSEQ_1:def 3;
then 1<=mu & mu<=5 by A4,FINSEQ_1:1;
then
A55: mu=1+0 or ... or mu=1+4 by NAT_1:62;
per cases by A55;
suppose
mu=1;
hence thesis by A50,A54,TARSKI:def 2;
end;
suppose
mu=2;
hence thesis by A20,A54,TARSKI:def 2;
end;
suppose
mu=3;
hence thesis by A11,A54,TARSKI:def 2;
end;
suppose
mu=4;
hence thesis by A15,A54,TARSKI:def 2;
end;
suppose
mu=5;
hence thesis by A51,A54,TARSKI:def 2;
end;
end;
{W-bound L~f1,E-bound L~f1} c= rng (X_axis(f1))
proof
let z be object;
assume
A56: z in {W-bound L~f1,E-bound L~f1};
per cases by A56,TARSKI:def 2;
suppose
A57: z=W-bound L~f1;
1 in dom (X_axis(f1)) by A22,SPRECT_2:15;
hence thesis by A50,A57,FUNCT_1:def 3;
end;
suppose
A58: z=E-bound L~f1;
2 in dom (X_axis(f1)) by A18,SPRECT_2:15;
hence thesis by A20,A58,FUNCT_1:def 3;
end;
end;
then
A59: rng (X_axis(f1))={W-bound L~f1,E-bound L~f1} by A52;
A60: len GoB(f1) = card rng X_axis(f1) by GOBOARD2:13
.=1+1 by A1,A59,CARD_2:57;
then
A61: (GoB f1)*(1+1,1)`1>=(E-max L~f)`1 by A4,A17,A41,JORDAN5D:5;
then (W-max L~f)`1 <(GoB f1)*(1+1,1)`1 by A46,XXREAL_0:2;
then (W-max L~f)`1+(E-max L~f)`1< (GoB f1)*(1+1,1)`1 +(GoB f1)*(1+1,1)`1 by
A61,XREAL_1:8;
then
A62: 1/2*((W-max L~f)`1+(E-max L~f)`1)< 1/2*(2*((GoB f1)*(1+1,1)`1)) by
XREAL_1:68;
A63: card rng (X_axis(f1))=2 by A1,A59,CARD_2:57;
for p being FinSequence of the carrier of TOP-REAL 2 st p in rng GoB
f1 holds len p = 2
proof
len GoB(Incr(X_axis(f1)),Incr(Y_axis(f1)) ) =len (Incr(X_axis(f1)))
by GOBOARD2:def 1
.=2 by A63,SEQ_4:def 21;
then consider s1 being FinSequence such that
A64: s1 in rng GoB(Incr(X_axis(f1)),Incr(Y_axis(f1)) ) and
A65: len s1 = width GoB(Incr(X_axis(f1)),Incr(Y_axis(f1))) by MATRIX_0:def 3;
let p be FinSequence of the carrier of TOP-REAL 2;
consider n being Nat such that
A66: for x st x in rng GoB f1 ex s being FinSequence st s=x & len s =
n by MATRIX_0:def 1;
assume p in rng GoB f1;
then
A67: ex s2 being FinSequence st s2=p & len s2 = n by A66;
ex s being FinSequence st s=s1 & len s = n by A16,A64,A66;
hence thesis by A41,A65,A67,GOBOARD2:def 2;
end;
then
A68: GoB f1 is Matrix of 2,2,the carrier of TOP-REAL 2 by A60,MATRIX_0:def 2;
len GoB f1 in Seg len GoB f1 by A60,FINSEQ_1:1;
then [len GoB f1,width GoB f1] in [:Seg (len GoB f1),Seg (width GoB f1):]
by A42,ZFMISC_1:87;
then
A69: [len GoB f1,width GoB f1] in Indices GoB f1 by A60,A41,A68,MATRIX_0:24;
1 in Seg len GoB f1 by A60,FINSEQ_1:1;
then [1,width GoB f1] in [:Seg (len GoB f1),Seg (width GoB f1):] by A42,
ZFMISC_1:87;
then
A70: [1,width GoB f1] in Indices GoB f1 by A60,A41,A68,MATRIX_0:24;
card rng X_axis(f1) >1 by A27,A29,XXREAL_0:2;
then
A71: 1=|.(|[0,r1+r+1]|).|-r1 & r width (GoB f1)+1;
f1/.(1+1)=(GoB f1)*(len (GoB f1),width (GoB f1)) by A60,A41,Th73;
then left_cell(f1,1) = cell(GoB(f1),1,width GoB(f1)) by A4,A70,A69,A72,A30
,A76,GOBOARD5:def 7;
then
A77: Int (left_cell(f1,1))= { |[r2,s]| : (GoB f1)*(1,1)`1 < r2 & r2 < (GoB
f1)*(1+1,1)`1 & (GoB f1)*(1,width (GoB f1))`2 < s } by A71,GOBOARD6:25;
A78: |.q4.|=r1 by A2,Th21;
A7: now
assume q4 in {q where q is Point of TOP-REAL 2: (|.q.|) =r1 by Th21;
A15: now
assume q3 in {q where q is Point of TOP-REAL 2: (|.q.|) {} & UBD (L~SpStSeq D)
is_outside_component_of (L~SpStSeq D) & BDD (L~SpStSeq D)<>{} & BDD (L~SpStSeq
D) is_inside_component_of (L~SpStSeq D)
proof
set f=SpStSeq D;
A1: UBD (L~SpStSeq D)=LeftComp (SpStSeq D) by Th79;
hence UBD (L~SpStSeq D)<>{};
LeftComp f is_a_component_of (L~f)` & not LeftComp f is bounded by Th74,
GOBOARD9:def 1;
hence UBD (L~SpStSeq D) is_outside_component_of (L~SpStSeq D) by A1;
A2: BDD (L~SpStSeq D)=RightComp (SpStSeq D) by Th79;
hence BDD (L~SpStSeq D)<>{};
RightComp (SpStSeq D) is_a_component_of (L~f)` & RightComp (SpStSeq D)
is bounded by Th78,GOBOARD9:def 2;
hence thesis by A2;
end;
begin :: Jordan property and boundary property
theorem Th81:
for G being non empty TopSpace, A being Subset of G st A`<>{}
holds A is boundary iff for x being set,V being Subset of G st x in A & x in V
& V is open ex B being Subset of G st B is_a_component_of A` & V meets B
proof
let G be non empty TopSpace,A be Subset of G;
assume
A1: A`<>{};
hereby
reconsider A1=A` as non empty Subset of G by A1;
reconsider A2=A` as Subset of G;
assume A is boundary;
then A` is dense by TOPS_1:def 4;
then
A2: Cl (A`)=[#] G by TOPS_1:def 3;
let x be set,V be Subset of G;
assume that
x in A and
A3: x in V & V is open;
A2 meets V by A3,A2,PRE_TOPC:def 7;
then consider z being object such that
A4: z in A` and
A5: z in V by XBOOLE_0:3;
reconsider p=z as Point of G|A` by A4,PRE_TOPC:8;
Component_of p c= the carrier of G|A`;
then Component_of p c= A` by PRE_TOPC:8;
then reconsider B0=Component_of p as Subset of G by XBOOLE_1:1;
A6: G|A1 is non empty;
then p in Component_of p by CONNSP_1:38;
then p in V /\ B0 by A5,XBOOLE_0:def 4;
then
A7: V meets B0;
Component_of p is a_component by A6,CONNSP_1:40;
then B0 is_a_component_of A` by CONNSP_1:def 6;
hence ex B being Subset of G st B is_a_component_of A` & V meets B by A7;
end;
assume
A8: for x being set,V being Subset of G st x in A & x in V & V is open
ex B being Subset of G st B is_a_component_of A` & V meets B;
the carrier of G c= Cl (A`)
proof
let z be object;
assume
A9: z in the carrier of G;
per cases;
suppose
A10: z in A;
for G1 being Subset of G st G1 is open holds z in G1 implies (A`)
meets G1
proof
let G1 be Subset of G;
assume
A11: G1 is open;
assume z in G1;
then consider B being Subset of G such that
A12: B is_a_component_of A` and
A13: G1 meets B by A8,A10,A11;
A14: G1 /\ B <> {} by A13;
consider B1 being Subset of G|A` such that
A15: B1 = B and
B1 is a_component by A12,CONNSP_1:def 6;
B1 c= the carrier of (G|A`);
then B1 c= A` by PRE_TOPC:8;
then (A`) /\ G1 <> {}G by A15,A14,XBOOLE_1:3,26;
hence thesis;
end;
hence thesis by A9,PRE_TOPC:def 7;
end;
suppose
A16: not z in A;
A17: A` c= Cl(A`) by PRE_TOPC:18;
z in (the carrier of G) \ A by A9,A16,XBOOLE_0:def 5;
hence thesis by A17;
end;
end;
then Cl (A`)=[#] G;
then A` is dense by TOPS_1:def 3;
hence thesis by TOPS_1:def 4;
end;
theorem Th82:
for A being Subset of TOP-REAL 2 st A`<>{} holds A is boundary
& A is Jordan iff ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1
misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being
Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component
& C2 is a_component
proof
let A be Subset of TOP-REAL 2;
assume
A1: A`<>{};
hereby
assume that
A2: A is boundary and
A3: A is Jordan;
consider A1,A2 being Subset of TOP-REAL 2 such that
A4: A` = A1 \/ A2 and
A5: A1 misses A2 and
A6: (Cl A1) \ A1 = (Cl A2) \ A2 and
A7: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2
holds C1 is a_component & C2 is a_component by A3,JORDAN1:def 2;
A=(A1 \/ A2)` by A4;
then
A8: A=A1` /\ A2` by XBOOLE_1:53;
A2 c= A` by A4,XBOOLE_1:7;
then reconsider D2=A2 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8;
A1 c= A` by A4,XBOOLE_1:7;
then reconsider D1=A1 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8;
D2=A2;
then
A9: D1 is a_component by A7;
A10: A c= (Cl A1) \ A1
proof
let z be object;
assume
A11: z in A;
for G being Subset of (TOP-REAL 2) st G is open holds z in G
implies (A1 \/ A2) meets G
proof
let G be Subset of (TOP-REAL 2);
assume
A12: G is open;
hereby
assume z in G;
then consider B being Subset of TOP-REAL 2 such that
A13: B is_a_component_of A` and
A14: G meets B by A1,A2,A11,A12,Th81;
consider B1 being Subset of (TOP-REAL 2) | A` such that
A15: B1 = B and
A16: B1 is a_component by A13,CONNSP_1:def 6;
A17: now
per cases by A9,A16,CONNSP_1:34;
case
B1=D1;
hence B1 c= A1 \/ A2 by XBOOLE_1:7;
end;
case
B1,D1 are_separated;
then
A18: Cl B1 misses D1 or B1 misses Cl D1 by CONNSP_1:def 1;
B1 is closed & D1 is closed by A9,A16,CONNSP_1:33;
then B1 misses D1 by A18,PRE_TOPC:22;
then
A19: B1 /\ D1={};
B1 c= the carrier of (TOP-REAL 2) | A`;
then B1 c= A` by PRE_TOPC:8;
then B1 = B1 /\ A` by XBOOLE_1:28
.=B1 /\ A1 \/ B1 /\ A2 by A4,XBOOLE_1:23
.= B1 /\ A2 by A19;
then
A20: B1 c= A2 by XBOOLE_1:17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence B1 c= A1 \/ A2 by A20;
end;
end;
G /\ B <> {} by A14;
then (A1 \/ A2) /\ G <> {} by A15,A17,XBOOLE_1:3,26;
hence (A1 \/ A2) meets G;
end;
end;
then z in Cl (A1 \/ A2) by A11,PRE_TOPC:def 7;
then z in (Cl A1) \/ Cl A2 by PRE_TOPC:20;
then
A21: z in Cl A1 or z in Cl A2 by XBOOLE_0:def 3;
not z in A` by A11,XBOOLE_0:def 5;
then ( not z in A1)& not z in A2 by A4,XBOOLE_0:def 3;
hence thesis by A6,A21,XBOOLE_0:def 5;
end;
(Cl A1) \A1 c= A1` & (Cl A2) \A2 c= A2` by XBOOLE_1:33;
then (Cl A1) \A1 c= A by A6,A8,XBOOLE_1:19;
then A=Cl A1 \ A1 by A10;
hence
ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1 misses A2 &
(Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being Subset of
(TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component
& C2 is a_component by A4,A5,A6,A7;
end;
hereby
assume ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1 misses
A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being Subset of
(TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component
& C2 is a_component;
then consider A1,A2 being Subset of TOP-REAL 2 such that
A22: A` = A1 \/ A2 and
A23: A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 and
A24: A=(Cl A1) \ A1 and
A25: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2
holds C1 is a_component & C2 is a_component;
for x being set,V being Subset of TOP-REAL 2 st x in A & x in V & V
is open ex B being Subset of TOP-REAL 2 st B is_a_component_of A` & V meets B
proof
A2 c= A` by A22,XBOOLE_1:7;
then reconsider D2=A2 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8;
A1 c= A` by A22,XBOOLE_1:7;
then reconsider D1=A1 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8;
let x be set,V be Subset of TOP-REAL 2;
assume that
A26: x in A and
A27: x in V & V is open;
D2=A2;
then D1 is a_component by A25;
then
A28: A1 is_a_component_of A` by CONNSP_1:def 6;
x in Cl A1 by A24,A26,XBOOLE_0:def 5;
then A1 meets V by A27,PRE_TOPC:def 7;
hence thesis by A28;
end;
hence A is boundary & A is Jordan by A1,A22,A23,A25,Th81,JORDAN1:def 2;
end;
end;
theorem Th83:
for p being Point of TOP-REAL n, P being Subset of TOP-REAL n
st n>=1 & P={p} holds P is boundary
proof
let p be Point of TOP-REAL n, P be Subset of TOP-REAL n;
assume that
A1: n>=1 and
A2: P={p};
the carrier of (TOP-REAL n) c= Cl (P`)
proof
let z be object;
assume
A3: z in the carrier of TOP-REAL n;
per cases;
suppose
A4: z=p;
reconsider ez=z as Point of Euclid n by A3,TOPREAL3:8;
for G1 being Subset of (TOP-REAL n) st G1 is open holds z in G1
implies (P`) meets G1
proof
let G1 be Subset of TOP-REAL n;
assume
A5: G1 is open;
thus z in G1 implies (P`) meets G1
proof
A6: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider GG = G1 as Subset of TopSpaceMetr Euclid n;
assume
A7: z in G1;
GG is open by A5,A6,PRE_TOPC:30;
then consider r be Real such that
A8: r>0 and
A9: Ball(ez,r) c= GG by A7,TOPMETR:15;
reconsider r as Real;
set p2=p-(r/2/sqrt n)*(1.REAL n);
reconsider ep2=p2 as Point of Euclid n by TOPREAL3:8;
A10: 00 by A8,XREAL_1:139;
then p<>p2 by A11,TOPRNS_1:28;
then not p2 in P by A2,TARSKI:def 1;
then
A12: p2 in P` by XBOOLE_0:def 5;
r/2p;
then not z in P by A2,TARSKI:def 1;
then
A13: z in P` by A3,XBOOLE_0:def 5;
P` c= Cl(P`) by PRE_TOPC:18;
hence thesis by A13;
end;
end;
then Cl (P`)=[#] (TOP-REAL n);
then P` is dense by TOPS_1:def 3;
hence thesis by TOPS_1:def 4;
end;
theorem Th84:
for p,q being Point of TOP-REAL 2,r st p`1=q`2 & -p`2=q`1 & p=r
*q holds p`1=0 & p`2=0 & p=0.TOP-REAL 2
proof
let p,q be Point of TOP-REAL 2,r;
A1: 1+r*r>0+0 by XREAL_1:8,63;
assume p`1=q`2 & -p`2=q`1 & p=r*q;
then
A2: p=|[r*(-p`2),r*(p`1)]| by EUCLID:57;
then p`2=r*(p`1) by EUCLID:52;
then p`1=-(r*(r*(p`1))) by A2,EUCLID:52
.=-(r*r*(p`1));
then (1+r*r)*p`1=0;
hence
A3: p`1=0 by A1,XCMPLX_1:6;
p`1=r*(-p`2) by A2,EUCLID:52;
then p`2=-(r*r*(p`2)) by A2,EUCLID:52;
then (1+r*r)*p`2=0;
hence p`2=0 by A1,XCMPLX_1:6;
hence thesis by A3,EUCLID:53,54;
end;
theorem Th85:
for q1,q2 being Point of TOP-REAL 2 holds LSeg(q1,q2) is boundary
proof
let q1,q2 be Point of TOP-REAL 2;
per cases;
suppose
q1=q2;
then LSeg(q1,q2)={q1} by RLTOPSP1:70;
hence thesis by Th83;
end;
suppose
A1: q1<>q2;
set P=LSeg(q1,q2);
the carrier of (TOP-REAL 2) c= Cl (P`)
proof
let z be object;
assume
A2: z in the carrier of TOP-REAL 2;
per cases;
suppose
A3: z in P;
reconsider ez=z as Point of Euclid 2 by A2,TOPREAL3:8;
set p1=q1-q2;
consider s being Real such that
A4: z=(1-s)*q1+s*q2 and
0<=s and
s<=1 by A3;
set p=(1-s)*q1+s*q2;
A5: now
assume |.p1.|=0;
then p1=0.TOP-REAL 2 by TOPRNS_1:24;
hence contradiction by A1,RLVECT_1:21;
end;
for G1 being Subset of (TOP-REAL 2) st G1 is open holds z in G1
implies (P`) meets G1
proof
let G1 be Subset of TOP-REAL 2;
assume
A6: G1 is open;
thus z in G1 implies (P`) meets G1
proof
A7: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8
;
then reconsider GG = G1 as Subset of TopSpaceMetr Euclid 2;
assume
A8: z in G1;
GG is open by A6,A7,PRE_TOPC:30;
then consider r be Real such that
A9: r>0 and
A10: Ball(ez,r) c= G1 by A8,TOPMETR:15;
reconsider r as Real;
A11: r/20 by A5;
then |[-p1`2,p1`1]|=0.TOP-REAL 2 by A9,A14,A15,RLVECT_1:11
,XCMPLX_1:6;
then
A16: (0.TOP-REAL 2)`1=-p1`2 & (0.TOP-REAL 2)`2=p1`1 by EUCLID:52;
(0.TOP-REAL 2)`1=0 & (0.TOP-REAL 2)`2=0 by EUCLID:52,54;
hence contradiction by A1,A16,EUCLID:53,54,RLVECT_1:21;
end;
A17: p2-p = (r/2/|.p1.|)*|[-p1`2,p1`1]| by RLVECT_4:1;
p2-p=(1-s2)*q1+s2*q2 -(1-s)*q1-s*q2 by A12,RLVECT_1:27
.=(1-s2)*q1-(1-s)*q1+s2*q2 -s*q2 by RLVECT_1:def 3
.=((1-s2)-(1-s))*q1+s2*q2 -s*q2 by RLVECT_1:35
.=(s-s2)*q1+(s2*q2 -s*q2) by RLVECT_1:def 3
.=(s-s2)*q1+(s2-s)*q2 by RLVECT_1:35
.=(s-s2)*q1+(-(s-s2))*q2
.=(s-s2)*q1-(s-s2)*q2 by RLVECT_1:79
.=(s-s2)*p1 by RLVECT_1:34;
then 1/(s-s2)*(s-s2)*p1= 1/(s-s2)*((r/2/|.p1.|)*|[- p1`2,p1`1]|
) by A17,RLVECT_1:def 7;
then 1 *p1= 1/(s-s2)*((r/2/|.p1.|)*|[-p1`2,p1`1]|) by A13,
XCMPLX_1:106;
then p1= 1/(s-s2)*((r/2/|.p1.|)*|[-p1`2,p1`1]|) by RLVECT_1:def 8
;
then
A18: p1= 1/(s-s2)*(r/2/|.p1.|)*|[-p1`2,p1`1]| by RLVECT_1:def 7;
p1`1=(|[-p1`2,p1`1]|)`2 & -p1`2=(|[-p1`2,p1`1]|)`1 by EUCLID:52;
then p1=0.TOP-REAL 2 by A18,Th84;
hence contradiction by A1,RLVECT_1:21;
end;
then
A19: p2 in (the carrier of TOP-REAL 2) \P by XBOOLE_0:def 5;
reconsider ep2=p2 as Point of Euclid 2 by TOPREAL3:8;
A20: p+-(r/2/|.p1.|)*|[-p1`2,p1`1]| -p = -(r/2/|.p1.|)*|[-p1`2,p1
`1]| by RLVECT_4:1;
A21: |[-p1`2,p1`1]|`1=-p1`2 & |[-p1`2,p1`1]|`2=p1`1 by EUCLID:52;
|.p-p2.|=|.p-(r/2/|.p1.|)*|[-p1`2,p1`1]| -p.| by RLVECT_1:27
.=|.-(r/2/|.p1.|)*|[-p1`2,p1`1]|.| by A20
.=|.(r/2/|.p1.|)*|[-p1`2,p1`1]|.| by TOPRNS_1:26
.=|.r/2/|.p1.|.|*|.|[-p1`2,p1`1]|.| by TOPRNS_1:7
.=|.r/2/|.p1.|.|*(sqrt ((-p1`2)^2+(p1`1)^2)) by A21,JGRAPH_1:30
.=|.r/2/|.p1.|.|*(sqrt ((p1`1)^2+(p1`2)^2))
.=|.r/2/|.p1.|.|*|.p1.| by JGRAPH_1:30
.=|.r/2.|/(|.|.p1.|.|)*|.p1.| by COMPLEX1:67
.=|.r/2.|/(|.p1.|)*|.p1.| by ABSVALUE:def 1
.=|.r/2.| by A5,XCMPLX_1:87
.=r/2 by A9,ABSVALUE:def 1;
then dist(ez,ep2) boundary;
coherence by Th85;
end;
theorem Th86:
for f being FinSequence of TOP-REAL 2 holds L~f is boundary
proof
let f be FinSequence of TOP-REAL 2;
A1: L~f=union { LSeg(f,i) : 1 <= i & i+1 <= len f } by TOPREAL1:def 4;
defpred P[Nat] means
for R1 being Subset of TOP-REAL 2 st R1=
union { LSeg(f,i) : 1 <= i & i+1 <= $1 } holds R1 is boundary;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A3: now
per cases;
case
1<=k & k+1<=len f;
then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3;
hence LSeg(f,k) is boundary;
end;
case
not(1<=k & k+1<=len f);
then LSeg(f,k)={} by TOPREAL1:def 3;
hence LSeg(f,k) is boundary;
end;
end;
union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } c= the carrier of TOP-REAL 2
proof
let z be object;
assume z in union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k };
then consider x being set such that
A4: z in x & x in { LSeg(f,i) : 1 <= i & i+1 <= k } by TARSKI:def 4;
ex i st x=LSeg(f,i) & 1 <= i & i+1 <= k by A4;
hence thesis by A4;
end;
then reconsider R3=union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } as Subset of
TOP-REAL 2;
assume for R1 being Subset of TOP-REAL 2 st R1=union { LSeg(f,i) : 1 <= i
& i+1 <= k } holds R1 is boundary;
then
A5: R3 is boundary;
thus for R2 being Subset of TOP-REAL 2 st R2=union { LSeg(f,i2) : 1 <= i2
& i2+1 <= k+1 } holds R2 is boundary
proof
let R2 be Subset of TOP-REAL 2;
assume
A6: R2=union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k+1 };
A7: R3 \/ LSeg(f,k) c= R2
proof
let z be object;
assume
A8: z in R3 \/ LSeg(f,k);
per cases by A8,XBOOLE_0:def 3;
suppose
z in R3;
then consider x being set such that
A9: z in x & x in { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } by TARSKI:def 4;
consider i2 such that
A10: x=LSeg(f,i2) & 1 <= i2 and
A11: i2+1 <= k by A9;
i2+1k;
then k+1<=i2+1 by NAT_1:13;
then i2+1=k+1 by A16,XXREAL_0:1;
hence z in R3 or z in LSeg(f,k) by A13,A14;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
then R2=R3 \/ LSeg(f,k) by A7;
hence thesis by A5,A3,TOPS_1:49;
end;
end;
union { LSeg(f,i) : 1 <= i & i+1 <= 0 } c= {}
proof
let z be object;
assume z in union { LSeg(f,i) : 1 <= i & i+1 <= 0 };
then consider x being set such that
A17: z in x & x in { LSeg(f,i) : 1 <= i & i+1 <= 0 } by TARSKI:def 4;
ex i st x=LSeg(f,i) & 1 <= i & i+1 <= 0 by A17;
hence thesis;
end;
then
A18: P[0];
for j holds P[j] from NAT_1:sch 2(A18,A2);
hence thesis by A1;
end;
registration
let f be FinSequence of TOP-REAL 2;
cluster L~f -> boundary;
coherence by Th86;
end;
theorem Th87:
for ep being Point of Euclid n,p,q being Point of TOP-REAL n st
p=ep & q in Ball(ep,r) holds |.p-q.|0 & p in L~SpStSeq D
holds ex q being Point of TOP-REAL 2 st q in UBD (L~SpStSeq D) & |.p-q.|0 and
A2: p in L~SpStSeq D;
set q1 = the Element of UBD (L~SpStSeq D);
set A=L~SpStSeq D;
A`<>{} by SPRECT_1:def 3;
then consider A1,A2 being Subset of TOP-REAL 2 such that
A3: A` = A1 \/ A2 and
A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: A=(Cl A1) \ A1 and
A6: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component
by Th82;
A7: Down(A2,A`)=A2 by A3,XBOOLE_1:21;
UBD A is_outside_component_of A by Th53;
then UBD (L~SpStSeq D) is_a_component_of A`;
then consider B1 being Subset of (TOP-REAL 2) | A` such that
A8: B1 = UBD (L~SpStSeq D) and
A9: B1 is a_component by CONNSP_1:def 6;
B1 c= [#]((TOP-REAL 2) | A`);
then
A10: UBD (L~SpStSeq D) c= A1 \/ A2 by A3,A8,PRE_TOPC:def 5;
A11: Down(A1,A`)=A1 by A3,XBOOLE_1:21;
then
A12: Down(A1,A`) is a_component by A6,A7;
A13: Down(A2,A`) is a_component by A6,A11,A7;
A14: UBD (L~SpStSeq D) <>{} by Th80;
then
A15: q1 in UBD (L~SpStSeq D);
per cases by A10,A15,XBOOLE_0:def 3;
suppose
q1 in A1;
then B1 /\ Down(A1,A`)<>{}((TOP-REAL 2) | A`) by A11,A8,A14,XBOOLE_0:def 4;
then B1 meets Down(A1,A`);
then B1=Down(A1,A`) by A12,A9,CONNSP_1:35;
then
A16: p in Cl(UBD (L~SpStSeq D)) by A2,A5,A11,A8,XBOOLE_0:def 5;
reconsider ep=p as Point of Euclid 2 by TOPREAL3:8;
reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8;
the distance of Euclid 2 is Reflexive by METRIC_1:def 6;
then dist(ep,ep)=0;
then
A17: p in Ball(ep,a) by A1,METRIC_1:11;
G2 is open by GOBOARD6:3;
then (UBD (L~SpStSeq D)) meets G2 by A16,A17,PRE_TOPC:def 7;
then consider t2 being object such that
A18: t2 in UBD (L~SpStSeq D) and
A19: t2 in G2 by XBOOLE_0:3;
reconsider qt2=t2 as Point of TOP-REAL 2 by A18;
|.p-qt2.|{}((TOP-REAL 2) | A`) by A7,A8,A14,XBOOLE_0:def 4;
then B1 meets Down(A2,A`);
then B1=Down(A2,A`) by A13,A9,CONNSP_1:35;
then
A20: p in Cl(UBD (L~SpStSeq D)) by A2,A4,A5,A7,A8,XBOOLE_0:def 5;
reconsider ep=p as Point of Euclid 2 by TOPREAL3:8;
reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8;
(the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6;
then dist(ep,ep)=0;
then
A21: p in Ball(ep,a) by A1,METRIC_1:11;
G2 is open by GOBOARD6:3;
then (UBD (L~SpStSeq D)) meets G2 by A20,A21,PRE_TOPC:def 7;
then consider t2 being object such that
A22: t2 in (UBD (L~SpStSeq D)) and
A23: t2 in G2 by XBOOLE_0:3;
reconsider qt2=t2 as Point of TOP-REAL 2 by A22;
|.p-qt2.|=1;
set a=r;
reconsider P=(REAL n)\ {q : (|.q.|) < a } as Subset of TOP-REAL n by
EUCLID:22;
A3: P c= A`
proof
let z be object;
assume
A4: z in P;
then reconsider q0=z as Point of TOP-REAL n;
not z in {q : (|.q.|) < a } by A4,XBOOLE_0:def 5;
then (|.q0.|) >= a;
then not q0 in A by A1;
hence thesis by XBOOLE_0:def 5;
end;
then
A5: Down(P,A`)=P by XBOOLE_1:28;
now
per cases;
suppose
n>=2;
then
A6: P is connected by Th40;
now
assume not BDD A is bounded;
then consider q being Point of TOP-REAL n such that
A7: q in BDD A and
A8: not |.q.|= a by A8;
then not q in {q2 where q2 is Point of TOP-REAL n: (|.q2.|) < a };
then q in P by A13,XBOOLE_0:def 5;
then P /\ B4<>{}((TOP-REAL n) | A`) by A9,A11,A14,XBOOLE_0:def 4;
then P meets B4;
then
A16: P c= B4 by A5,A6,A15,CONNSP_1:36,46;
B3 is bounded by A12;
hence contradiction by A2,A14,A16,Th41,RLTOPSP1:42;
end;
hence thesis;
end;
suppose
A17: n<2;
{q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]|
holds r2>=a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q where q is Point of TOP-REAL n: for r2 being Real
st q=|[r2]| holds r2>=a};
then ex q being Point of TOP-REAL n st q=z & for r2 being Real st q=
|[r2]| holds r2>=a;
hence thesis;
end;
then reconsider
P2={q where q is Point of TOP-REAL n: for r2 being Real st
q=|[r2]| holds r2>=a} as Subset of TOP-REAL n;
{q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]|
holds r2<=-a} c= the carrier of TOP-REAL n
proof
let z be object;
assume z in {q where q is Point of TOP-REAL n: for r2 being Real
st q=|[r2]| holds r2<=-a};
then ex q being Point of TOP-REAL n st q=z & for r2 being Real st q=
|[r2]| holds r2<=-a;
hence thesis;
end;
then reconsider
P1={q where q is Point of TOP-REAL n: for r2 being Real st
q=|[r2]| holds r2<=-a} as Subset of TOP-REAL n;
n<1+1 by A17;
then
n<=1 by NAT_1:13;
then
A18: n=1 by A2,XXREAL_0:1;
A19: P c= P1 \/ P2
proof
let z be object;
assume
A20: z in P;
then reconsider q0=z as Point of TOP-REAL n;
consider r3 being Real such that
A21: q0=<*r3*> by A18,JORDAN2B:20;
not z in {q : (|.q.|) < a } by A20,XBOOLE_0:def 5;
then (|.q0.|) >= a;
then
A22: |.r3.|>=a by A21,Th4;
per cases by A22,SEQ_2:1;
suppose
-a>=r3;
then for r2 being Real st q0=|[r2]| holds r2<=-a by A21,JORDAN2B:23
;
then q0 in P1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
r3>=a;
then for r2 being Real st q0=|[r2]| holds r2>=a by A21,JORDAN2B:23;
then q0 in P2;
hence thesis by XBOOLE_0:def 3;
end;
end;
P1 \/ P2 c= P
proof
let z be object;
assume
A23: z in P1 \/ P2;
per cases by A23,XBOOLE_0:def 3;
suppose
A24: z in P1;
then
A25: ex q being Point of TOP-REAL n st q=z & for r2 being Real st q
=|[r2]| holds r2<=-a;
for q2 being Point of TOP-REAL n st q2=z holds |.q2.| >= a
proof
let q2 be Point of TOP-REAL n;
consider r3 being Real such that
A26: q2=<*r3*> by A18,JORDAN2B:20;
assume
A27: q2=z;
then
A28: r3<=-a by A25,A26;
now
per cases;
case
a<0;
hence |.r3.| >=a by COMPLEX1:46;
end;
case
a>=0;
then -a<=-0;
then |.r3.|=-r3 by A28,ABSVALUE:30;
hence |.r3.|>=a by A25,A27,A26,XREAL_1:25;
end;
end;
hence thesis by A26,Th4;
end;
then
A29: not z in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a };
z in the carrier of TOP-REAL n by A24;
then z in REAL n by EUCLID:22;
hence thesis by A29,XBOOLE_0:def 5;
end;
suppose
A30: z in P2;
then
A31: ex q being Point of TOP-REAL n st q=z & for r2 being Real st q
=|[r2]| holds r2>=a;
for q2 being Point of TOP-REAL n st q2=z holds |.q2.| >= a
proof
let q2 be Point of TOP-REAL n;
consider r3 being Real such that
A32: q2=<*r3*> by A18,JORDAN2B:20;
assume q2=z;
then
A33: r3>=a by A31,A32;
now
per cases;
suppose
a<0;
hence |.r3.|>=a by COMPLEX1:46;
end;
suppose
a>=0;
hence |.r3.| >=a by A33,ABSVALUE:def 1;
end;
end;
hence thesis by A32,Th4;
end;
then
A34: not z in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a };
z in the carrier of TOP-REAL n by A30;
then z in REAL n by EUCLID:22;
hence thesis by A34,XBOOLE_0:def 5;
end;
end;
then
A35: P=P1 \/ P2 by A19;
then P2 c= P by XBOOLE_1:7;
then
A36: Down(P2,A`)=P2 by A3,XBOOLE_1:1,28;
for w1,w2 being Point of TOP-REAL n st w1 in P2 & w2 in P2 holds
LSeg(w1,w2) c= P2
proof
let w1,w2 be Point of TOP-REAL n;
assume that
A37: w1 in P2 and
A38: w2 in P2;
A39: ex q2 being Point of TOP-REAL n st q2=w2 & for r2 being Real st
q2=|[r2]| holds r2>=a by A38;
consider r3 being Real such that
A40: w1=<*r3*> by A18,JORDAN2B:20;
consider r4 being Real such that
A41: w2=<*r4*> by A18,JORDAN2B:20;
A42: ex q1 being Point of TOP-REAL n st q1=w1 & for r2 being Real st
q1=|[r2]| holds r2>=a by A37;
thus LSeg(w1,w2) c= P2
proof
let z be object;
assume z in LSeg(w1,w2);
then consider r2 such that
A43: z=(1-r2)*w1 + r2*w2 and
A44: 0 <= r2 and
A45: r2 <= 1;
reconsider q4=z as Point of TOP-REAL n by A43;
(1-r2)*w1=|[(1-r2)*r3]| & r2*w2=|[r2*r4]| by A18,A40,A41,
JORDAN2B:21;
then
A46: z=|[(1-r2)*r3+r2*r4]| by A18,A43,JORDAN2B:22;
for r5 being Real st q4=|[r5]| holds r5>=a
proof
let r5 be Real;
assume q4=|[r5]|;
then
A47: r5=(1-r2)*r3+r2*r4 by A46,JORDAN2B:23;
1-r2>=0 by A45,XREAL_1:48;
then
A48: (1-r2)*r3>=(1-r2)*(a) by A42,A40,XREAL_1:64;
r2*r4>=r2*(a) & (1-r2)*(a)+r2*(a)=a by A39,A41,A44,XREAL_1:64;
hence thesis by A47,A48,XREAL_1:7;
end;
hence thesis;
end;
end;
then P2 is convex by JORDAN1:def 1;
then
A49: Down(P2,A`) is connected by A36,CONNSP_1:46;
P1 c= P by A35,XBOOLE_1:7;
then
A50: Down(P1,A`)=P1 by A3,XBOOLE_1:1,28;
A51: now
assume P2 is bounded;
then consider r being Real such that
A52: for q being Point of TOP-REAL n st q in P2 holds |.q.|=a
proof
let r5 be Real;
assume p3=|[r5]|;
then
A55: r5=(|.r.|+|.a.|) by JORDAN2B:23;
a<=|.a.| & |.a.|<=|.a.|+|.r.| by ABSVALUE:4,COMPLEX1:46,XREAL_1:31;
hence thesis by A55,XXREAL_0:2;
end;
then
A56: p3 in P2 by A18;
|.p3.|=|.(|.r.|+|.a.|).| & r<=|.r.| by Th4,ABSVALUE:4;
hence contradiction by A52,A56,A53,A54,XXREAL_0:2;
end;
A57: now
assume P1 is bounded;
then consider r being Real such that
A58: for q being Point of TOP-REAL n st q in P1 holds |.q.|= -(|.a.|+|.r.|) by XREAL_1:24;
assume p3=|[r5]|;
then r5=-(|.r.|+|.a.|) by JORDAN2B:23;
hence thesis by A61,A62,XXREAL_0:2;
end;
then
A63: p3 in P1 by A18;
|.p3.|=|.-(|.r.|+|.a.|).| by Th4
.=|.(|.r.|+|.a.|).| by COMPLEX1:52;
hence contradiction by A58,A63,A59,A60,XXREAL_0:2;
end;
for w1,w2 being Point of TOP-REAL n st w1 in P1 & w2 in P1 holds
LSeg(w1,w2) c= P1
proof
let w1,w2 be Point of TOP-REAL n;
assume that
A64: w1 in P1 and
A65: w2 in P1;
consider r4 being Real such that
A66: w2=<*r4*> by A18,JORDAN2B:20;
ex q2 being Point of TOP-REAL n st q2=w2 & for r2 being Real st
q2=|[r2]| holds r2<=-a by A65;
then
A67: r4<=-a by A66;
consider r3 being Real such that
A68: w1=<*r3*> by A18,JORDAN2B:20;
ex q1 being Point of TOP-REAL n st q1=w1 & for r2 being Real st
q1=|[r2]| holds r2<=-a by A64;
then
A69: r3<=-a by A68;
thus LSeg(w1,w2) c= P1
proof
let z be object;
assume z in LSeg(w1,w2);
then consider r2 such that
A70: z=(1-r2)*w1 + r2*w2 and
A71: 0 <= r2 and
A72: r2 <= 1;
reconsider q4=z as Point of TOP-REAL n by A70;
A73: r2*w2=|[r2*r4]| by A18,A66,JORDAN2B:21;
(1-r2)*w1 = (1-r2)*|[r3]| by A68
.=|[(1-r2)*r3]| by JORDAN2B:21;
then
A74: z=|[(1-r2)*r3+r2*r4]| by A18,A70,A73,JORDAN2B:22;
for r5 being Real st q4=|[r5]| holds r5<=-a
proof
let r5 be Real;
assume q4=|[r5]|;
then
A75: r5=(1-r2)*r3+r2*r4 by A74,JORDAN2B:23;
1-r2>=0 by A72,XREAL_1:48;
then
A76: (1-r2)*r3<=(1-r2)*(-a) by A69,XREAL_1:64;
r2*r4<=r2*(-a) & (1-r2)*(-a)+r2*(-a)=-a by A67,A71,XREAL_1:64;
hence thesis by A75,A76,XREAL_1:7;
end;
hence thesis;
end;
end;
then P1 is convex by JORDAN1:def 1;
then
A77: Down(P1,A`) is connected by A50,CONNSP_1:46;
now
assume not BDD A is bounded;
then consider q being Point of TOP-REAL n such that
A78: q in BDD A and
A79: not |.q.|= a by A79;
then not q in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a };
then
A85: q in P by A84,XBOOLE_0:def 5;
B3 is_a_component_of A` by A83;
then consider B4 being Subset of (TOP-REAL n) | A` such that
A86: B4 = B3 and
A87: B4 is a_component by CONNSP_1:def 6;
per cases by A19,A85,XBOOLE_0:def 3;
suppose
q in P1;
then P1 /\ B4<>{}((TOP-REAL n) | A`) by A80,A82,A86,XBOOLE_0:def 4;
then
A88: P1 meets B4;
B3 is bounded by A83;
hence contradiction
by A50,A57,A77,A86,A87,A88,CONNSP_1:36,RLTOPSP1:42;
end;
suppose
q in P2;
then P2 /\ B4<>{}((TOP-REAL n) | A`) by A80,A82,A86,XBOOLE_0:def 4;
then
A89: P2 meets B4;
B3 is bounded by A83;
hence contradiction
by A36,A51,A49,A86,A87,A89,CONNSP_1:36,RLTOPSP1:42;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
n<1;
then n<0+1;
then
A90: n=0 by NAT_1:13;
for q2 being Point of TOP-REAL n holds |.q2.|<1
proof
let q2 be Point of TOP-REAL n;
q2=0.TOP-REAL n by A90,EUCLID:77;
hence thesis by TOPRNS_1:23;
end;
then for q2 being Point of TOP-REAL n st q2 in [#] (TOP-REAL n) holds |.
q2.|<1;
then [#](TOP-REAL n) is bounded by Th21;
hence thesis by RLTOPSP1:42;
end;
end;
theorem Th91:
for G being non empty TopSpace,A,B,C,D being Subset of G st B
is a_component & C is a_component & A \/ B=the carrier of G & C
misses A holds C=B
proof
let G be non empty TopSpace,A,B,C,D be Subset of G;
assume that
A1: B is a_component and
A2: C is a_component and
A3: A \/ B=the carrier of G and
A4: C misses A;
now
C /\ (the carrier of G)=C by XBOOLE_1:28;
then
A5: C /\ A \/ C /\ B=C by A3,XBOOLE_1:23;
assume C misses B;
then
A6: C /\ B = {};
C <> {}G by A2,CONNSP_1:32;
hence contradiction by A4,A6,A5;
end;
hence thesis by A1,A2,CONNSP_1:35;
end;
theorem Th92:
for A being Subset of TOP-REAL 2 st A is bounded & A is Jordan
holds BDD A is_inside_component_of A
proof
let A be Subset of TOP-REAL 2;
assume that
A1: A is bounded and
A2: A is Jordan;
reconsider D=A` as non empty Subset of TOP-REAL 2 by A2,JORDAN1:def 2;
consider A1,A2 being Subset of TOP-REAL 2 such that
A3: A` = A1 \/ A2 and
A4: A1 misses A2 and
(Cl A1) \ A1 = (Cl A2) \ A2 and
A5: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component
by A2,JORDAN1:def 2;
A6: UBD A is_outside_component_of A by A1,Th53;
then UBD A is_a_component_of A`;
then consider B1 being Subset of (TOP-REAL 2) | A` such that
A7: B1 = UBD A and
A8: B1 is a_component by CONNSP_1:def 6;
A9: Down(A1,A`)=A1 by A3,XBOOLE_1:21;
A10: Down(A2,A`)=A2 by A3,XBOOLE_1:21;
then
A11: Down(A2,A`) is a_component by A5,A9;
then
A12: A2 is_a_component_of A` by A10,CONNSP_1:def 6;
A13: (TOP-REAL 2) | D is non empty;
A14: Down(A1,A`) is a_component by A5,A9,A10;
then
A15: A1 is_a_component_of A` by A9,CONNSP_1:def 6;
per cases by A9,A14,A8,CONNSP_1:35;
suppose
A16: B1=A1;
A17: now
assume not BDD A c= A2;
then consider x being object such that
A18: x in BDD A and
A19: not x in A2;
consider y being set such that
A20: x in y and
A21: y in {B3 where B3 is Subset of TOP-REAL 2: B3
is_inside_component_of A} by A18,TARSKI:def 4;
consider B3 being Subset of TOP-REAL 2 such that
A22: y=B3 and
A23: B3 is_inside_component_of A by A21;
A24: B3 is_a_component_of A` by A23;
then consider B4 being Subset of (TOP-REAL 2) | A` such that
A25: B4 = B3 and
A26: B4 is a_component by CONNSP_1:def 6;
A27: B3<>{}((TOP-REAL 2) | A`) by A13,A25,A26,CONNSP_1:32;
B4 <> Down(A1,A`) by A9,A7,A16,A23,A25,A6;
then
A28: B3 misses A1 by A9,A14,A25,A26,CONNSP_1:35;
B4=Down(A2,A`) or B4 misses Down(A2,A`) by A11,A26,CONNSP_1:35;
then
A29: B4=Down(A2,A`) or B4 /\ Down(A2,A`)={}((TOP-REAL 2) | A`);
B3=B3 /\ (A1 \/ A2) by A3,A24,SPRECT_1:5,XBOOLE_1:28
.=(B3 /\ A1) \/ (B3 /\ A2 ) by XBOOLE_1:23
.={} by A10,A19,A20,A22,A25,A29,A28;
hence contradiction by A27;
end;
now
assume not A2 is bounded;
then A2 is_outside_component_of A by A12;
then A2 /\ UBD A <> {} by Th14,XBOOLE_1:28;
hence contradiction by A4,A7,A16;
end;
then
A30: A2 is_inside_component_of A by A12;
then A2 c= BDD A by Th13;
hence thesis by A30,A17,XBOOLE_0:def 10;
end;
suppose
A31: B1 misses Down(A1,A`);
set E1=Down(A1,A`), E2=Down(A2,A`);
E1 \/ E2=[#]((TOP-REAL 2) | A`) by A3,A9,A10,PRE_TOPC:def 5;
then
A32: UBD A=A2 by A10,A11,A13,A7,A8,A31,Th91;
A33: BDD A \/ UBD A=A` by Th18;
A34: BDD A misses UBD A by Th15;
A35: BDD A c= A1
proof
let z be object;
assume z in BDD A;
then z in A` & not z in UBD A by A34,A33,XBOOLE_0:3,def 3;
hence thesis by A3,A32,XBOOLE_0:def 3;
end;
A36: BDD A is bounded by A1,Th90;
A1 c= BDD A
proof
let z be object;
assume z in A1;
then z in A` & not z in UBD A by A3,A4,A32,XBOOLE_0:3,def 3;
hence thesis by A33,XBOOLE_0:def 3;
end;
then BDD A = A1 by A35;
hence thesis by A15,A36;
end;
end;
theorem
for a being Real,p being Point of TOP-REAL 2 st a>0 & p in (L~SpStSeq
D) holds ex q being Point of TOP-REAL 2 st q in BDD (L~SpStSeq D) & |.p-q.|0 and
A2: p in (L~SpStSeq D);
set q1 = the Element of BDD (L~SpStSeq D);
set A=L~SpStSeq D;
A`<>{} by SPRECT_1:def 3;
then consider A1,A2 being Subset of TOP-REAL 2 such that
A3: A` = A1 \/ A2 and
A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: A=(Cl A1) \ A1 and
A6: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component
by Th82;
A7: Down(A2,A`)=A2 by A3,XBOOLE_1:21;
BDD A is_inside_component_of A by Th92;
then BDD (L~SpStSeq D) is_a_component_of A`;
then consider B1 being Subset of (TOP-REAL 2) | A` such that
A8: B1 = BDD (L~SpStSeq D) and
A9: B1 is a_component by CONNSP_1:def 6;
B1 c= the carrier of (TOP-REAL 2) | A`;
then
A10: BDD (L~SpStSeq D) c= A1 \/ A2 by A3,A8,PRE_TOPC:8;
A11: Down(A1,A`)=A1 by A3,XBOOLE_1:21;
then
A12: Down(A1,A`) is a_component by A6,A7;
A13: Down(A2,A`) is a_component by A6,A11,A7;
A14: BDD (L~SpStSeq D) <>{} by Th80;
then
A15: q1 in BDD (L~SpStSeq D);
per cases by A10,A15,XBOOLE_0:def 3;
suppose
q1 in A1;
then B1 /\ Down(A1,A`)<>{}((TOP-REAL 2) | A`) by A11,A8,A14,XBOOLE_0:def 4;
then B1 meets Down(A1,A`);
then B1=Down(A1,A`) by A12,A9,CONNSP_1:35;
then
A16: p in Cl(BDD (L~SpStSeq D)) by A2,A5,A11,A8,XBOOLE_0:def 5;
reconsider ep=p as Point of Euclid 2 by TOPREAL3:8;
reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8;
(the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6;
then dist(ep,ep)=0;
then
A17: p in Ball(ep,a) by A1,METRIC_1:11;
G2 is open by GOBOARD6:3;
then (BDD (L~SpStSeq D)) meets G2 by A16,A17,PRE_TOPC:def 7;
then consider t2 being object such that
A18: t2 in (BDD (L~SpStSeq D)) and
A19: t2 in G2 by XBOOLE_0:3;
reconsider qt2=t2 as Point of TOP-REAL 2 by A18;
|.p-qt2.|{}((TOP-REAL 2) | A`) by A7,A8,A14,XBOOLE_0:def 4;
then B1 meets Down(A2,A`);
then B1=Down(A2,A`) by A13,A9,CONNSP_1:35;
then
A20: p in Cl(BDD (L~SpStSeq D)) by A2,A4,A5,A7,A8,XBOOLE_0:def 5;
reconsider ep=p as Point of Euclid 2 by TOPREAL3:8;
reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8;
(the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6;
then dist(ep,ep)=0;
then
A21: p in Ball(ep,a) by A1,METRIC_1:11;
G2 is open by GOBOARD6:3;
then (BDD (L~SpStSeq D)) meets G2 by A20,A21,PRE_TOPC:def 7;
then consider t2 being object such that
A22: t2 in (BDD (L~SpStSeq D)) and
A23: t2 in G2 by XBOOLE_0:3;
reconsider qt2=t2 as Point of TOP-REAL 2 by A22;
|.p-qt2.| E-bound (
L~f) holds p in LeftComp f
proof
let p be Point of TOP-REAL 2;
assume that
A1: f/.1 = N-min L~f and
A2: p`1> E-bound(L~f);
set g=SpStSeq L~f;
A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41;
E-bound L~ g=E-bound L~f by SPRECT_1:61;
then p in LeftComp g by A2,SPRECT_3:40;
hence thesis by A3;
end;
theorem
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 < S-bound (
L~f) holds p in LeftComp f
proof
let p be Point of TOP-REAL 2;
assume that
A1: f/.1 = N-min L~f and
A2: p`2< S-bound(L~f);
set g=SpStSeq L~f;
A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41;
S-bound L~ g=S-bound L~f by SPRECT_1:59;
then p in LeftComp g by A2,SPRECT_3:40;
hence thesis by A3;
end;
theorem
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 > N-bound (
L~f) holds p in LeftComp f
proof
let p be Point of TOP-REAL 2;
assume that
A1: f/.1 = N-min L~f and
A2: p`2>N-bound(L~f);
set g=SpStSeq L~f;
A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41;
N-bound L~ g=N-bound L~f by SPRECT_1:60;
then p in LeftComp g by A2,SPRECT_3:40;
hence thesis by A3;
end;
:: Moved from GOBRD14, AK, 22.02.2006
theorem
for T being TopSpace, A being Subset of T, B being Subset of T st B
is_a_component_of A holds B is connected
proof
let T be TopSpace, A be Subset of T, B be Subset of T;
assume B is_a_component_of A;
then consider C being Subset of T|A such that
A1: C = B and
A2: C is a_component by CONNSP_1:def 6;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:23;
end;
theorem
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B
is_inside_component_of A holds B is connected
proof
let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n;
assume B is_inside_component_of A;
then consider C being Subset of (TOP-REAL n) | A` such that
A1: C = B and
A2: C is a_component and
C is bounded Subset of Euclid n by Th7;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:23;
end;
theorem Th100:
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
st B is_outside_component_of A holds B is connected
proof
let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n;
assume B is_outside_component_of A;
then consider C being Subset of (TOP-REAL n) | A` such that
A1: C = B and
A2: C is a_component and
not C is bounded Subset of Euclid n by Th8;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:23;
end;
theorem
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B
is_a_component_of A` holds A misses B
by SPRECT_1:5,SUBSET_1:23;
theorem
P is_outside_component_of Q & R is_inside_component_of Q implies P misses R
proof
assume
A1: P is_outside_component_of Q;
assume
A2: R is_inside_component_of Q;
(BDD Q) misses (UBD Q) by Th15;
then P misses BDD Q by A1,Th14,XBOOLE_1:63;
hence thesis by A2,Th13,XBOOLE_1:63;
end;
theorem
2 <= n implies for A, B, P being Subset of TOP-REAL n st P is bounded
& A is_outside_component_of P & B is_outside_component_of P holds A = B
proof
assume
A1: 2 <= n;
let A, B, P be Subset of TOP-REAL n such that
A2: P is bounded and
A3: A is_outside_component_of P and
A4: B is_outside_component_of P;
A5: B is_a_component_of P` by A4;
UBD P is_outside_component_of P by A1,A2,Th53;
then
A6: UBD P is_a_component_of P`;
A7: P` is non empty by A1,A2,Th51,XXREAL_0:2;
A8: B <> {} by A4;
A9: B c= UBD P by A4,Th14;
A10: A c= UBD P by A3,Th14;
A11: A is_a_component_of P` by A3;
then A <> {} by A7,SPRECT_1:4;
then A = UBD P by A11,A6,A10,GOBOARD9:1,XBOOLE_1:69;
hence thesis by A5,A8,A6,A9,GOBOARD9:1,XBOOLE_1:69;
end;
registration
let C be closed Subset of TOP-REAL 2;
cluster BDD C -> open;
coherence
proof
set F = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C};
F c= bool the carrier of TOP-REAL 2
proof
let f be object;
assume f in F;
then
ex B being Subset of TOP-REAL 2 st f = B & B is_inside_component_of C;
hence thesis;
end;
then reconsider F as Subset-Family of TOP-REAL 2;
F is open
proof
let P be Subset of TOP-REAL 2;
assume P in F;
then consider B being Subset of TOP-REAL 2 such that
A1: P = B and
A2: B is_inside_component_of C;
B is_a_component_of C` by A2;
hence thesis by A1,SPRECT_3:8;
end;
hence thesis by TOPS_2:19;
end;
cluster UBD C -> open;
coherence
proof
set F = {B where B is Subset of TOP-REAL 2: B is_outside_component_of C};
F c= bool the carrier of TOP-REAL 2
proof
let f be object;
assume f in F;
then ex B being Subset of TOP-REAL 2 st f = B & B
is_outside_component_of C;
hence thesis;
end;
then reconsider F as Subset-Family of TOP-REAL 2;
F is open
proof
let P be Subset of TOP-REAL 2;
assume P in F;
then consider B being Subset of TOP-REAL 2 such that
A3: P = B and
A4: B is_outside_component_of C;
B is_a_component_of C` by A4;
hence thesis by A3,SPRECT_3:8;
end;
hence thesis by TOPS_2:19;
end;
end;
registration
let C be compact Subset of TOP-REAL 2;
cluster UBD C -> connected;
coherence by Th53,Th100;
end;
:: Moved from JORDAN1C, AK, 22.02.2006
reserve p for Point of TOP-REAL 2;
theorem Th104:
west_halfline p is non bounded
proof
set Wp = west_halfline p;
set p11 = p`1, p12 = p`2;
assume Wp is bounded;
then reconsider C = Wp as bounded Subset of Euclid 2 by Th5;
consider r being Real such that
A1: 0 < r and
A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y)
<= r by TBSP_1:def 7;
set EX1 = p`1-2*r;
reconsider p1 = p, EX = |[p`1-2*r, p`2]| as Point of Euclid 2 by EUCLID:67;
0 + p`1 <= 2*r + p`1 by A1,XREAL_1:6;
then p`1 - 2*r <= p`1 by XREAL_1:20;
then
A3: |[p`1-2*r, p`2]|`1 <= p`1 by EUCLID:52;
then
A4: p1 in Wp by TOPREAL1:def 13;
|[p`1-2*r, p`2]|`2 = p`2 by EUCLID:52;
then
A5: EX in Wp by A3,TOPREAL1:def 13;
p = |[p11,p12]| by EUCLID:53;
then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - p`2)^2) by GOBOARD6:6
.= 2*r by A1,SQUARE_1:22;
hence thesis by A1,A2,A5,A4,XREAL_1:155;
end;
theorem Th105:
east_halfline p is non bounded
proof
set Wp = east_halfline p;
set p11 = p`1, p12 = p`2;
assume Wp is bounded;
then reconsider C = Wp as bounded Subset of Euclid 2 by Th5;
consider r being Real such that
A1: 0 < r and
A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y)
<= r by TBSP_1:def 7;
set EX1 = p`1+2*r, EX2 = p`2;
reconsider p1 = p, EX = |[p`1+2*r, p`2]| as Point of Euclid 2 by EUCLID:67;
0 + p`1 <= 2*r + p`1 by A1,XREAL_1:6;
then
A3: |[EX1, p`2]|`1 >= p`1 by EUCLID:52;
then
A4: p1 in Wp by TOPREAL1:def 11;
|[EX1, p`2]|`2 = p`2 by EUCLID:52;
then
A5: EX in Wp by A3,TOPREAL1:def 11;
p = |[p11,p12]| by EUCLID:53;
then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6
.= sqrt ((EX1 - p11)^2 + 0)
.= 2*r by A1,SQUARE_1:22;
hence thesis by A1,A2,A5,A4,XREAL_1:155;
end;
theorem Th106:
north_halfline p is non bounded
proof
set Wp = north_halfline p;
set p11 = p`1, p12 = p`2;
assume Wp is bounded;
then reconsider C = Wp as bounded Subset of Euclid 2 by Th5;
consider r being Real such that
A1: 0 < r and
A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y)
<= r by TBSP_1:def 7;
set EX2 = p`2+2*r, EX1 = p`1;
reconsider p1 = p, EX = |[p`1, p`2+2*r]| as Point of Euclid 2 by EUCLID:67;
A3: |[p`1, EX2]|`1 = p`1 by EUCLID:52;
then
A4: p1 in Wp by TOPREAL1:def 10;
0 + p`2 <= 2*r + p`2 by A1,XREAL_1:6;
then |[p`1, EX2]|`2 >= p`2 by EUCLID:52;
then
A5: EX in Wp by A3,TOPREAL1:def 10;
p = |[p11,p12]| by EUCLID:53;
then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6
.= sqrt ((EX2 - p12)^2 + 0)
.= 2*r by A1,SQUARE_1:22;
hence thesis by A1,A2,A5,A4,XREAL_1:155;
end;
theorem Th107:
south_halfline p is non bounded
proof
set Wp = south_halfline p;
set p11 = p`1, p12 = p`2;
assume Wp is bounded;
then reconsider C = Wp as bounded Subset of Euclid 2 by Th5;
consider r being Real such that
A1: 0 < r and
A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y)
<= r by TBSP_1:def 7;
set EX2 = p`2-2*r, EX1 = p`1;
reconsider p1 = p, EX = |[p`1, p`2-2*r]| as Point of Euclid 2 by EUCLID:67;
p = |[p11,p12]| by EUCLID:53;
then
A3: dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6
.= 2*r by A1,SQUARE_1:22;
A4: |[p`1, EX2]|`1 = p`1 by EUCLID:52;
then
A5: p1 in Wp by TOPREAL1:def 12;
0 + p`2 <= 2*r + p`2 by A1,XREAL_1:6;
then p`2 - 2*r <= p`2 by XREAL_1:20;
then |[p`1, EX2]|`2 <= p`2 by EUCLID:52;
then EX in Wp by A4,TOPREAL1:def 12;
hence thesis by A1,A2,A5,A3,XREAL_1:155;
end;
registration
let C be compact Subset of TOP-REAL 2;
cluster UBD C -> non empty;
coherence
proof
A1: UBD C is_outside_component_of C by Th53;
thus thesis by A1;
end;
end;
theorem Th108:
for C being compact Subset of TOP-REAL 2 holds UBD C is_a_component_of C`
proof
let C be compact Subset of TOP-REAL 2;
UBD C is_outside_component_of C by Th53;
hence thesis;
end;
theorem Th109:
for C being compact Subset of TOP-REAL 2 for WH being connected
Subset of TOP-REAL 2 st WH is non bounded & WH misses C holds WH c= UBD C
proof
let C be compact Subset of TOP-REAL 2;
let WH be connected Subset of TOP-REAL 2;
assume that
A1: WH is non bounded and
A2: WH misses C;
A3: WH meets UBD C
proof
(BDD C) \/ (UBD C) = C` & [#]the carrier of TOP-REAL 2 = C \/ C` by Th18,
SUBSET_1:10;
then
A4: WH c= (UBD C) \/ BDD C by A2,XBOOLE_1:73;
assume
A5: WH misses UBD C;
BDD C is bounded by Th90;
hence thesis by A1,A5,A4,RLTOPSP1:42,XBOOLE_1:73;
end;
WH c= C` by A2,SUBSET_1:23;
hence thesis by A3,Th108,GOBOARD9:4;
end;
theorem
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st west_halfline p misses C holds west_halfline p c= UBD C
proof
let C be compact Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set WH = west_halfline p;
assume
A1: WH misses C;
WH is non bounded non empty connected by Th104;
hence thesis by A1,Th109;
end;
theorem
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st east_halfline p misses C holds east_halfline p c= UBD C
proof
let C be compact Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set WH = east_halfline p;
assume
A1: WH misses C;
WH is non bounded non empty connected by Th105;
hence thesis by A1,Th109;
end;
theorem
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st south_halfline p misses C holds south_halfline p c= UBD C
proof
let C be compact Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set WH = south_halfline p;
assume
A1: WH misses C;
WH is non bounded non empty connected by Th107;
hence thesis by A1,Th109;
end;
theorem
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st north_halfline p misses C holds north_halfline p c= UBD C
proof
let C be compact Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set WH = north_halfline p;
assume
A1: WH misses C;
WH is non bounded non empty connected by Th106;
hence thesis by A1,Th109;
end;
theorem
for n being Nat, r being Real st r > 0
for x,y,z being Element of Euclid n st x = 0*n
for p being Element of TOP-REAL n st p = y & r*p = z
holds r*dist(x,y) = dist(x,z) by Lm1;
theorem
for n being Nat, r,s being Real st r > 0
for x being Element of Euclid n st x = 0*n
for A being Subset of TOP-REAL n st A = Ball(x,s)
holds r*A = Ball(x,r*s) by Lm2;
theorem
for n being Nat, r,s,t be Real st 0 < s & s <= t
for x being Element of Euclid n st x = 0*n
for BA being Subset of TOP-REAL n st BA = Ball(x,r)
holds s*BA c= t*BA by Lm3;