Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Bounded Domains and Unbounded Domains

**by****Yatsuka Nakamura,****Andrzej Trybulec, and****Czeslaw Bylinski**- Received January 7, 1999
- MML identifier: JORDAN2C

- [ Mizar article, MML identifier index ]

environ vocabulary ABSVALUE, ARYTM_1, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC, EUCLID, COMPLEX1, SQUARE_1, RLVECT_1, RVSUM_1, TOPREAL1, RELAT_2, BORSUK_1, TOPS_2, SUBSET_1, RCOMP_1, BOOLE, LATTICES, CONNSP_1, TARSKI, CONNSP_3, SETFAM_1, GRAPH_1, ARYTM_3, TREAL_1, SEQ_1, FUNCT_4, TOPMETR, COMPTS_1, FINSEQ_2, METRIC_1, PCOMPS_1, WEIERSTR, SEQ_4, SEQ_2, VECTSP_1, FUNCOP_1, PARTFUN1, JORDAN3, TBSP_1, CONNSP_2, SPPOL_1, GOBOARD2, SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1, MCART_1, CARD_1, MATRIX_1, GOBOARD9, SEQM_3, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2, JORDAN2C, FINSEQ_4, CARD_3, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, CARD_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, STRUCT_0, PCOMPS_1, CONNSP_1, CONNSP_2, TBSP_1, CONNSP_3, TOPRNS_1, TOPMETR, RCOMP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, SQUARE_1, ABSVALUE, BORSUK_2, WEIERSTR, SEQ_4, JORDAN3, BINARITH, FUNCOP_1, FUNCT_3, VECTSP_1, TREAL_1, FUNCT_4, RVSUM_1, EUCLID, SPPOL_1, PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1, MATRIX_1, GOBOARD1, JORDAN1, GOBOARD2, GOBOARD5, GOBOARD9, JORDAN2B; constructors WEIERSTR, REAL_1, TOPS_1, TOPS_2, COMPTS_1, REALSET1, CONNSP_1, TBSP_1, CONNSP_3, FINSEQ_4, JORDAN1, RCOMP_1, GOBOARD2, GOBOARD9, FINSEQOP, SQUARE_1, ABSVALUE, BORSUK_2, JORDAN3, TREAL_1, FUNCT_4, SPPOL_1, SPRECT_1, TOPREAL2, SPRECT_2, PSCOMP_1, BINARITH, JORDAN2B, PARTFUN1, TOPRNS_1, DOMAIN_1, MEMBERED, XCMPLX_0; clusters SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, SPRECT_1, TOPMETR, TOPREAL1, BORSUK_1, FUNCT_1, FUNCOP_1, FINSEQ_1, XREAL_0, FINSET_1, SPRECT_3, EUCLID, GOBOARD1, GOBOARD2, ARYTM_3, MEMBERED, ZFMISC_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin ::Definitions of Bounded Domain and Unbounded Domain reserve m,n,i,i2,j for Nat, r,r1,r2,s for Real, x,y,z,y1,y2 for set; theorem :: JORDAN2C:1 r<=0 implies abs(r)=-r; theorem :: JORDAN2C:2 for n,m st n<=m & m<=n+2 holds m=n or m=n+1 or m=n+2; theorem :: JORDAN2C:3 for n,m st n<=m & m<=n+3 holds m=n or m=n+1 or m=n+2 or m=n+3; theorem :: JORDAN2C:4 for n,m st n<=m & m<=n+4 holds m=n or m=n+1 or m=n+2 or m=n+3 or m=n+4; theorem :: JORDAN2C:5 for a,b being real number st a>=0 & b>=0 holds a+b>=0; theorem :: JORDAN2C:6 for a,b being real number st a>0 & b>=0 holds a+b>0; theorem :: JORDAN2C:7 for f being FinSequence st rng f={x,y} & len f=2 holds f.1=x & f.2=y or f.1=y & f.2=x; theorem :: JORDAN2C:8 for f being increasing FinSequence of REAL st rng f={r,s} & len f=2 & r<=s holds f.1=r & f.2=s; reserve p,p1,p2,p3,q,q1,q2,q3,q4 for Point of TOP-REAL n; theorem :: JORDAN2C:9 p1+p2-p3=p1-p3+p2; theorem :: JORDAN2C:10 abs(|.q.|)=|.q.|; theorem :: JORDAN2C:11 abs(|.q1.|- |.q2.|)<=|.q1-q2.|; theorem :: JORDAN2C:12 |.|[r]|.|=abs(r); theorem :: JORDAN2C:13 q-0.REAL n=q & (0.REAL n)-q = -q; theorem :: JORDAN2C:14 for P being Subset of TOP-REAL n st P is convex holds P is connected; theorem :: JORDAN2C:15 for G being non empty TopSpace, P being Subset of G,A being Subset of G, Q being Subset of G|A st P=Q & P is connected holds Q is connected; definition let n;let A be Subset of TOP-REAL n; canceled; attr A is Bounded means :: JORDAN2C:def 2 ex C being Subset of Euclid n st C=A & C is bounded; end; theorem :: JORDAN2C:16 for A,B being Subset of TOP-REAL n st B is Bounded & A c= B holds A is Bounded; definition let n;let A be Subset of TOP-REAL n; let B be Subset of TOP-REAL n; pred B is_inside_component_of A means :: JORDAN2C:def 3 B is_a_component_of A` & B is Bounded; end; definition let M be non empty MetrStruct; cluster bounded Subset of M; end; theorem :: JORDAN2C:17 for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n holds B is_inside_component_of A iff ex C being Subset of ((TOP-REAL n)|(A`)) st C=B & C is_a_component_of ((TOP-REAL n)|(A`)) & C is bounded Subset of Euclid n; definition let n;let A be Subset of TOP-REAL n; let B be Subset of TOP-REAL n; pred B is_outside_component_of A means :: JORDAN2C:def 4 B is_a_component_of A` & B is not Bounded; end; theorem :: JORDAN2C:18 for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n holds B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n)|(A`)) st C=B & C is_a_component_of ((TOP-REAL n)|(A`)) & C is not bounded Subset of Euclid n; theorem :: JORDAN2C:19 for A,B being Subset of TOP-REAL n st B is_inside_component_of A holds B c= A`; theorem :: JORDAN2C:20 for A,B being Subset of TOP-REAL n st B is_outside_component_of A holds B c= A`; definition let n;let A be Subset of TOP-REAL n; func BDD A -> Subset of TOP-REAL n equals :: JORDAN2C:def 5 union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}; end; definition let n;let A be Subset of TOP-REAL n; func UBD A -> Subset of TOP-REAL n equals :: JORDAN2C:def 6 union{B where B is Subset of TOP-REAL n: B is_outside_component_of A}; end; theorem :: JORDAN2C:21 [#](TOP-REAL n) is convex; theorem :: JORDAN2C:22 [#](TOP-REAL n) is connected; definition let n; cluster [#](TOP-REAL n) -> connected; end; theorem :: JORDAN2C:23 [#](TOP-REAL n) is_a_component_of TOP-REAL n; theorem :: JORDAN2C:24 for A being Subset of TOP-REAL n holds BDD A is a_union_of_components of (TOP-REAL n)|A`; theorem :: JORDAN2C:25 for A being Subset of TOP-REAL n holds UBD A is a_union_of_components of (TOP-REAL n)|A`; theorem :: JORDAN2C:26 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; theorem :: JORDAN2C:27 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; theorem :: JORDAN2C:28 for A being Subset of TOP-REAL n holds BDD A misses UBD A; theorem :: JORDAN2C:29 for A being Subset of TOP-REAL n holds BDD A c= A`; theorem :: JORDAN2C:30 for A being Subset of TOP-REAL n holds UBD A c= A`; theorem :: JORDAN2C:31 for A being Subset of TOP-REAL n holds (BDD A) \/ (UBD A) = A`; reserve u for Point of Euclid n; theorem :: JORDAN2C:32 for G being non empty TopSpace, w1,w2,w3 being Point of G, h1,h2 being map of I[01],G st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous & w2=h2.0 & w3=h2.1 holds ex h3 being map of I[01],G st h3 is continuous & w1=h3.0 & w3=h3.1 & rng h3 c= (rng h1) \/ (rng h2); theorem :: JORDAN2C:33 for P being Subset of TOP-REAL n st P=REAL n holds P is connected; definition let n; func 1*n -> FinSequence of REAL equals :: JORDAN2C:def 7 n |-> (1 qua Real); end; definition let n; redefine func 1*n -> Element of REAL n; end; definition let n; func 1.REAL n -> Point of TOP-REAL n equals :: JORDAN2C:def 8 1*n; end; theorem :: JORDAN2C:34 abs 1*n = n |-> (1 qua Real); theorem :: JORDAN2C:35 |.1*n.| = sqrt n; theorem :: JORDAN2C:36 1.REAL 1 = <* 1 qua Real *>; theorem :: JORDAN2C:37 |. (1.REAL n) .| = sqrt n; theorem :: JORDAN2C:38 1<=n implies 1<=|. (1.REAL n) .|; theorem :: JORDAN2C:39 for W being Subset of Euclid n st n>=1 & W=REAL n holds W is not bounded; theorem :: JORDAN2C:40 for A being Subset of TOP-REAL n holds A is Bounded iff ex r being Real st for q being Point of TOP-REAL n st q in A holds |.q.|<r; theorem :: JORDAN2C:41 n>=1 implies not [#](TOP-REAL n) is Bounded; theorem :: JORDAN2C:42 n>=1 implies UBD {}(TOP-REAL n)=REAL n; theorem :: JORDAN2C:43 for w1,w2,w3 being Point of TOP-REAL n, P being non empty Subset of TOP-REAL n, h1,h2 being map of I[01],(TOP-REAL n)|P st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous & w2=h2.0 & w3=h2.1 holds ex h3 being map of I[01],(TOP-REAL n)|P st h3 is continuous & w1=h3.0 & w3=h3.1; theorem :: JORDAN2C:44 for P being Subset of TOP-REAL n, w1,w2,w3 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P ex h being map of I[01],(TOP-REAL n)|P st h is continuous & w1=h.0 & w3=h.1; theorem :: JORDAN2C:45 for P being Subset of TOP-REAL n, w1,w2,w3,w4 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P & LSeg(w3,w4) c= P ex h being map of I[01],(TOP-REAL n)|P st h is continuous & w1=h.0 & w4=h.1; theorem :: JORDAN2C:46 for P being Subset of TOP-REAL n, w1,w2,w3,w4,w5,w6,w7 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P & LSeg(w3,w4) c= P & LSeg(w4,w5) c= P & LSeg(w5,w6) c= P & LSeg(w6,w7) c= P ex h being map of I[01],(TOP-REAL n)|P st h is continuous & w1=h.0 & w7=h.1; reserve s2 for Real; theorem :: JORDAN2C:47 for w1,w2 being Point of TOP-REAL n st not (ex r being Real st w1=r*w2 or w2=r*w1) holds not (0.REAL n) in LSeg(w1,w2); theorem :: JORDAN2C:48 for w1,w2 being Point of TOP-REAL n,P being Subset of TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)& not (0.REAL n) in LSeg(w1,w2) holds ex w0 being Point of TOP-REAL n st w0 in LSeg(w1,w2) & |.w0.|>0 & |.w0.|=(dist_min(P)).(0.REAL n); theorem :: JORDAN2C:49 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; theorem :: JORDAN2C:50 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; canceled; theorem :: JORDAN2C:52 for f being FinSequence of REAL holds f is Element of REAL (len f) & f is Point of TOP-REAL (len f); theorem :: JORDAN2C:53 for x being Element of REAL n,f,g being FinSequence of REAL, r being Real st f=x & g=r*x holds len f=len g & for i being Nat st 1<=i & i<=len f holds g/.i=r*f/.i; theorem :: JORDAN2C:54 for x being Element of REAL n,f being FinSequence st x<> 0*n & x=f holds ex i being Nat st 1<=i & i<=n & f.i<>0; theorem :: JORDAN2C:55 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; theorem :: JORDAN2C:56 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; theorem :: JORDAN2C:57 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; theorem :: JORDAN2C:58 for a being Real st n>=1 holds {q: |.q.| >a} <>{}; theorem :: JORDAN2C:59 for a being Real, P being Subset of TOP-REAL n st n>=2 & P={q : |.q.| > a } holds P is connected; theorem :: JORDAN2C:60 for a being Real st n>=1 holds (REAL n) \ {q: |.q.| < a} <> {}; theorem :: JORDAN2C:61 for a being Real,P being Subset of TOP-REAL n st n>=2 & P=(REAL n)\ {q : |.q.| < a } holds P is connected; theorem :: JORDAN2C:62 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; theorem :: JORDAN2C:63 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; theorem :: JORDAN2C:64 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; theorem :: JORDAN2C:65 for a being Real,P being Subset of TOP-REAL 1 st P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a } holds P is connected; theorem :: JORDAN2C:66 for a being Real,P being Subset of TOP-REAL 1 st P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } holds P is connected; theorem :: JORDAN2C:67 for W being Subset of Euclid 1,a being Real, P being Subset of TOP-REAL 1 st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a } & P=W holds P is connected & W is not bounded; theorem :: JORDAN2C:68 for W being Subset of Euclid 1,a being Real, P being Subset of TOP-REAL 1 st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } & P=W holds P is connected & W is not bounded; theorem :: JORDAN2C:69 for W being Subset of Euclid n,a being Real, P being Subset of TOP-REAL n st n>=2 & W={q : |.q.| > a } & P=W holds P is connected & W is not bounded; theorem :: JORDAN2C:70 for W being Subset of Euclid n,a being Real, P being Subset of TOP-REAL n st n>=2 & W=(REAL n)\ {q : (|.q.|) < a } & P=W holds P is connected & W is not bounded; theorem :: JORDAN2C:71 for P, P1 being Subset of TOP-REAL n, Q being Subset of TOP-REAL n, W being Subset of Euclid n st P=W & P is connected & W is not bounded & P1=skl (Down(P,Q`)) & W misses Q holds P1 is_outside_component_of Q; theorem :: JORDAN2C:72 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= B & A=C & C is bounded holds A is bounded; theorem :: JORDAN2C:73 for A being Subset of TOP-REAL n st A is compact holds A is Bounded; theorem :: JORDAN2C:74 for A being Subset of TOP-REAL n st 1<=n & A is Bounded holds A` <> {}; theorem :: JORDAN2C:75 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; theorem :: JORDAN2C:76 for A being Subset of TOP-REAL n st n>=2 & A is Bounded ex B being Subset of TOP-REAL n st B is_outside_component_of A & B=UBD A; theorem :: JORDAN2C:77 for a being Real, P being Subset of TOP-REAL n st P={q : (|.q.|) < a } holds P is convex; theorem :: JORDAN2C:78 for a being Real,P being Subset of TOP-REAL n st P=Ball(u,a) holds P is convex; theorem :: JORDAN2C:79 for a being Real,P being Subset of TOP-REAL n st P={q : |.q.| < a } holds P is connected; reserve R for Subset of TOP-REAL n; reserve P for Subset of TOP-REAL n; theorem :: JORDAN2C:80 p <> q & p in Ball(u,r) & q in Ball(u,r) implies ex h being map of I[01],TOP-REAL n st h is continuous & h.0=p & h.1=q & rng h c= Ball(u,r); theorem :: JORDAN2C:81 for f being map 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 map of I[01],TOP-REAL n st h is continuous & h.0=p1 & h.1=p & rng h c= rng f \/ Ball(u,r); theorem :: JORDAN2C:82 for f being map 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 map of I[01],TOP-REAL n st f1 is continuous & rng f1 c= P & f1.0=p1 & f1.1=p; theorem :: JORDAN2C:83 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 map of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds P is open; theorem :: JORDAN2C:84 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 map of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds P is open; theorem :: JORDAN2C:85 for R being Subset of TOP-REAL n holds p in R & P={q: q=p or ex f being map of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} implies P c= R; theorem :: JORDAN2C:86 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 map of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds R c= P; theorem :: JORDAN2C:87 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 map of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q; theorem :: JORDAN2C:88 for A being Subset of TOP-REAL n, a being real number st A={q: |.q.|=a} holds A` is open & A is closed; theorem :: JORDAN2C:89 for B being non empty Subset of TOP-REAL n st B is open holds (TOP-REAL n)|B is locally_connected; theorem :: JORDAN2C:90 for B being non empty Subset of TOP-REAL n, A being Subset of TOP-REAL n,a being real number st A={q: |.q.|=a} & A`=B holds (TOP-REAL n)|B is locally_connected; theorem :: JORDAN2C:91 for f being map of TOP-REAL n,R^1 st (for q holds f.q=|.q.|) holds f is continuous; theorem :: JORDAN2C:92 ex f being map of TOP-REAL n,R^1 st (for q holds f.q=|.q.|) & f is continuous; definition canceled; let X, Y be non empty 1-sorted, f be map of X,Y, x be set; assume x is Point of X; func pi(f,x) -> Point of Y equals :: JORDAN2C:def 10 f.x; end; theorem :: JORDAN2C:93 for g being map of I[01],TOP-REAL n st g is continuous holds ex f being map of I[01],R^1 st (for t being Point of I[01] holds f.t=|.g.t.|) & f is continuous; theorem :: JORDAN2C:94 for g being map of I[01],TOP-REAL n,a being Real st g is continuous & |.pi(g,0).|<=a & a<=|.pi(g,1).| holds ex s being Point of I[01] st |.pi(g,s).|=a; theorem :: JORDAN2C:95 q=<*r*> implies |.q.|=abs(r); theorem :: JORDAN2C:96 for A being Subset of TOP-REAL n,a being Real st n>=1 & a>0 & A={q: |.q.|=a} holds ex B being Subset of TOP-REAL n st B is_inside_component_of A & B=BDD A; begin ::Bounded and Unbounded Domains of Rectangles reserve D for non vertical non horizontal non empty compact Subset of TOP-REAL 2; theorem :: JORDAN2C:97 len (GoB SpStSeq D)=2 & width (GoB SpStSeq D)=2 & (SpStSeq D)/.1=(GoB SpStSeq D)*(1,2) & (SpStSeq D)/.2=(GoB SpStSeq D)*(2,2) & (SpStSeq D)/.3=(GoB SpStSeq D)*(2,1) & (SpStSeq D)/.4=(GoB SpStSeq D)*(1,1) & (SpStSeq D)/.5=(GoB SpStSeq D)*(1,2); theorem :: JORDAN2C:98 LeftComp SpStSeq D is non Bounded; theorem :: JORDAN2C:99 LeftComp SpStSeq D c= UBD (L~SpStSeq D); theorem :: JORDAN2C:100 for G being TopSpace,A,B,C being Subset of G st A is_a_component_of G & B is_a_component_of G & C is connected & A meets C & B meets C holds A=B; theorem :: JORDAN2C:101 for B being Subset of TOP-REAL 2 st B is_a_component_of (L~SpStSeq D)` & not B is Bounded holds B=LeftComp SpStSeq D; theorem :: JORDAN2C:102 RightComp SpStSeq D c= BDD (L~SpStSeq D) & RightComp SpStSeq D is Bounded; theorem :: JORDAN2C:103 LeftComp SpStSeq D = UBD (L~SpStSeq D) & RightComp SpStSeq D = BDD (L~SpStSeq D); theorem :: JORDAN2C:104 UBD (L~SpStSeq D)<>{} & 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); begin :: Jordan property and boundary property theorem :: JORDAN2C:105 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; theorem :: JORDAN2C:106 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_of (TOP-REAL 2)|A` & C2 is_a_component_of (TOP-REAL 2)|A`; theorem :: JORDAN2C:107 for p being Point of TOP-REAL n, P being Subset of TOP-REAL n st n>=1 & P={p} holds P is boundary; theorem :: JORDAN2C:108 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.REAL 2; theorem :: JORDAN2C:109 for q1,q2 being Point of TOP-REAL 2 holds LSeg(q1,q2) is boundary; definition let q1,q2 be Point of TOP-REAL 2; cluster LSeg(q1,q2) -> boundary; end; theorem :: JORDAN2C:110 for f being FinSequence of TOP-REAL 2 holds L~f is boundary; definition let f be FinSequence of TOP-REAL 2; cluster L~f -> boundary; end; theorem :: JORDAN2C:111 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.|<r & |.q-p.|<r; theorem :: JORDAN2C:112 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 UBD (L~SpStSeq D) & |.p-q.|<a; theorem :: JORDAN2C:113 REAL 0 = {0.REAL 0}; theorem :: JORDAN2C:114 for A being Subset of TOP-REAL n st A is Bounded holds BDD A is Bounded; theorem :: JORDAN2C:115 for G being non empty TopSpace,A,B,C,D being Subset of G st A is_a_component_of G & B is_a_component_of G & C is_a_component_of G & A \/ B=the carrier of G & C misses A holds C=B; theorem :: JORDAN2C:116 for A being Subset of TOP-REAL 2 st A is Bounded & A is Jordan holds BDD A is_inside_component_of A; theorem :: JORDAN2C:117 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.|<a; begin :: Points in LeftComp reserve f for clockwise_oriented (non constant standard special_circular_sequence); theorem :: JORDAN2C:118 for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`1 < W-bound (L~f) holds p in LeftComp f; theorem :: JORDAN2C:119 for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`1 > E-bound (L~f) holds p in LeftComp f; theorem :: JORDAN2C:120 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; theorem :: JORDAN2C:121 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;

Back to top