:: Bounded Domains and Unbounded Domains :: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski :: :: Received January 7, 1999 :: Copyright (c) 1999-2021 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; begin :: from, RLAFFIN2, 2011.08.01, A.T. registration let n be Nat; cluster TOP-REAL n -> add-continuous Mult-continuous; end; begin :: Definitions of Bounded Domain and Unbounded Domain reserve m,n,i,i2,j for Nat, r,r1,r2,s,t for Real, x,y,z for object; ::$CT 5 theorem :: JORDAN2C:6 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; ::$CT theorem :: JORDAN2C:8 |.|.q.|.|=|.q.|; theorem :: JORDAN2C:9 |.|.q1.|- |.q2.|.|<=|.q1-q2.|; theorem :: JORDAN2C:10 |.|[r]|.|=|.r.|; theorem :: JORDAN2C:11 for n being Nat, A be Subset of TOP-REAL n holds A is bounded iff A is bounded Subset of Euclid n; theorem :: JORDAN2C:12 for A,B being Subset of TOP-REAL n st B is bounded & A c= B holds A is bounded; definition ::$CD let n be Nat; let A, B be Subset of TOP-REAL n; pred B is_inside_component_of A means :: JORDAN2C:def 2 B is_a_component_of A` & B is bounded; end; registration let M be non empty MetrStruct; cluster bounded for Subset of M; end; theorem :: JORDAN2C:13 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; definition let n be Nat; let A, B be Subset of TOP-REAL n; pred B is_outside_component_of A means :: JORDAN2C:def 3 B is_a_component_of A` & B is not bounded; end; theorem :: JORDAN2C:14 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; theorem :: JORDAN2C:15 for A,B being Subset of TOP-REAL n st B is_inside_component_of A holds B c= A`; theorem :: JORDAN2C:16 for A,B being Subset of TOP-REAL n st B is_outside_component_of A holds B c= A`; definition let n be Nat; let A be Subset of TOP-REAL n; func BDD A -> Subset of TOP-REAL n equals :: JORDAN2C:def 4 union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}; end; definition let n be Nat; let A be Subset of TOP-REAL n; func UBD A -> Subset of TOP-REAL n equals :: JORDAN2C:def 5 union{B where B is Subset of TOP-REAL n: B is_outside_component_of A}; end; registration let n be Nat; cluster [#](TOP-REAL n) -> convex; end; registration let n; cluster [#](TOP-REAL n) -> a_component; end; ::$CT 3 theorem :: JORDAN2C:20 for A being Subset of TOP-REAL n holds BDD A is a_union_of_components of (TOP-REAL n) | A`; theorem :: JORDAN2C:21 for A being Subset of TOP-REAL n holds UBD A is a_union_of_components of (TOP-REAL n) | A`; theorem :: JORDAN2C:22 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:23 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:24 for A being Subset of TOP-REAL n holds BDD A misses UBD A; theorem :: JORDAN2C:25 for A being Subset of TOP-REAL n holds BDD A c= A`; theorem :: JORDAN2C:26 for A being Subset of TOP-REAL n holds UBD A c= A`; theorem :: JORDAN2C:27 for A being Subset of TOP-REAL n holds (BDD A) \/ (UBD A) = A`; reserve u for Point of Euclid n; theorem :: JORDAN2C:28 for P being Subset of TOP-REAL n st P=REAL n holds P is connected; ::$CT 4 theorem :: JORDAN2C:33 for W being Subset of Euclid n st n>=1 & W=REAL n holds W is not bounded; theorem :: JORDAN2C:34 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.|=1 implies not [#](TOP-REAL n) is bounded; theorem :: JORDAN2C:36 n>=1 implies UBD {}(TOP-REAL n)=REAL n; theorem :: JORDAN2C:37 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; theorem :: JORDAN2C:38 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; theorem :: JORDAN2C:39 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; theorem :: JORDAN2C:40 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; theorem :: JORDAN2C:41 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); theorem :: JORDAN2C:42 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:43 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; theorem :: JORDAN2C:44 for f being FinSequence of REAL holds f is Element of REAL (len f) & f is Point of TOP-REAL (len f); theorem :: JORDAN2C:45 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; theorem :: JORDAN2C:46 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; theorem :: JORDAN2C:47 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:48 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:49 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:50 for a being Real st n>=1 holds {q: |.q.| >a} <>{}; theorem :: JORDAN2C:51 for a being Real, P being Subset of TOP-REAL n st n>=2 & P={q : |.q.| > a } holds P is connected; theorem :: JORDAN2C:52 for a being Real st n>=1 holds (REAL n) \ {q: |.q.| < a} <> {}; theorem :: JORDAN2C:53 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:54 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:55 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:56 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; ::$CT 2 theorem :: JORDAN2C:59 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; theorem :: JORDAN2C:60 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; theorem :: JORDAN2C:61 for W being Subset of Euclid n,a being Real st n>=2 & W={q : |.q.| > a } holds W is not bounded; theorem :: JORDAN2C:62 for W being Subset of Euclid n,a being Real st n>=2 & W=(REAL n)\ {q : (|.q.|) < a } holds W is not bounded; theorem :: JORDAN2C:63 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= Component_of (Down(P,Q`)) & W misses Q holds P1 is_outside_component_of Q; theorem :: JORDAN2C:64 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; theorem :: JORDAN2C:65 for A being Subset of TOP-REAL n st A is compact holds A is bounded; registration let n be Element of NAT; cluster compact -> bounded for Subset of TOP-REAL n; end; theorem :: JORDAN2C:66 for A being Subset of TOP-REAL n st 1<=n & A is bounded holds A` <> {}; theorem :: JORDAN2C:67 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:68 for A being Subset of TOP-REAL n st n>=2 & A is bounded holds UBD A is_outside_component_of A; theorem :: JORDAN2C:69 for a being Real, P being Subset of TOP-REAL n st P={q : (|.q.|) < a } holds P is convex; theorem :: JORDAN2C:70 for a being Real,P being Subset of TOP-REAL n st P=Ball(u,a) holds P is convex; reserve R for Subset of TOP-REAL n; reserve P,Q for Subset of TOP-REAL n; ::$CT theorem :: JORDAN2C:72 :: uogolnic na wypukle !!! p <> 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); theorem :: JORDAN2C:73 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); theorem :: JORDAN2C:74 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; theorem :: JORDAN2C:75 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; theorem :: JORDAN2C:76 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; theorem :: JORDAN2C:77 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; theorem :: JORDAN2C:78 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; theorem :: JORDAN2C:79 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; theorem :: JORDAN2C:80 for A being Subset of TOP-REAL n, a being Real st A={q: |.q.|=a} holds A` is open & A is closed; theorem :: JORDAN2C:81 for B being non empty Subset of TOP-REAL n st B is open holds (TOP-REAL n) | B is locally_connected; theorem :: JORDAN2C:82 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; theorem :: JORDAN2C:83 for f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.| ) holds f is continuous; theorem :: JORDAN2C:84 ex f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.|) & f is continuous; theorem :: JORDAN2C:85 for g being Function of I[01],TOP-REAL n st g is continuous holds ex f being Function of I[01],R^1 st (for t being Point of I[01] holds f.t =|.g.t.|) & f is continuous; theorem :: JORDAN2C:86 for g being Function of I[01],TOP-REAL n,a being Real st g is continuous & |.g/.0 .|<=a & a<=|.g/.1 .| holds ex s being Point of I[01] st |.g/.s.|=a; theorem :: JORDAN2C:87 q=<*r*> implies |.q.|=|.r.|; theorem :: JORDAN2C:88 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; begin ::bounded and Unbounded Domains of Rectangles reserve D for non vertical non horizontal non empty compact Subset of TOP-REAL 2; theorem :: JORDAN2C:89 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:90 LeftComp SpStSeq D is non bounded; theorem :: JORDAN2C:91 LeftComp SpStSeq D c= UBD (L~SpStSeq D); theorem :: JORDAN2C:92 for G being TopSpace,A,B,C being Subset of G st A is a_component & B is a_component & C is connected & A meets C & B meets C holds A=B; theorem :: JORDAN2C:93 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:94 RightComp SpStSeq D c= BDD (L~SpStSeq D) & RightComp SpStSeq D is bounded; theorem :: JORDAN2C:95 LeftComp SpStSeq D = UBD (L~SpStSeq D) & RightComp SpStSeq D = BDD (L~SpStSeq D); theorem :: JORDAN2C:96 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:97 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:98 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; theorem :: JORDAN2C:99 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:100 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; theorem :: JORDAN2C:101 for q1,q2 being Point of TOP-REAL 2 holds LSeg(q1,q2) is boundary; registration let q1,q2 be Point of TOP-REAL 2; cluster LSeg(q1,q2) -> boundary; end; theorem :: JORDAN2C:102 for f being FinSequence of TOP-REAL 2 holds L~f is boundary; registration let f be FinSequence of TOP-REAL 2; cluster L~f -> boundary; end; theorem :: JORDAN2C:103 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 & p in (L~SpStSeq D) holds ex q being Point of TOP-REAL 2 st q in BDD (L~SpStSeq D) & |.p-q.| E-bound ( L~f) holds p in LeftComp f; theorem :: JORDAN2C:112 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:113 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; :: Moved from GOBRD14, AK, 22.02.2006 theorem :: JORDAN2C:114 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; theorem :: JORDAN2C:115 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; theorem :: JORDAN2C:116 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; theorem :: JORDAN2C:117 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; theorem :: JORDAN2C:118 P is_outside_component_of Q & R is_inside_component_of Q implies P misses R; theorem :: JORDAN2C:119 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; registration let C be closed Subset of TOP-REAL 2; cluster BDD C -> open; cluster UBD C -> open; end; registration let C be compact Subset of TOP-REAL 2; cluster UBD C -> connected; end; :: Moved from JORDAN1C, AK, 22.02.2006 reserve p for Point of TOP-REAL 2; theorem :: JORDAN2C:120 west_halfline p is non bounded; theorem :: JORDAN2C:121 east_halfline p is non bounded; theorem :: JORDAN2C:122 north_halfline p is non bounded; theorem :: JORDAN2C:123 south_halfline p is non bounded; registration let C be compact Subset of TOP-REAL 2; cluster UBD C -> non empty; end; theorem :: JORDAN2C:124 for C being compact Subset of TOP-REAL 2 holds UBD C is_a_component_of C`; theorem :: JORDAN2C:125 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; theorem :: JORDAN2C:126 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; theorem :: JORDAN2C:127 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; theorem :: JORDAN2C:128 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; theorem :: JORDAN2C:129 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; theorem :: JORDAN2C:130 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); theorem :: JORDAN2C:131 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); theorem :: JORDAN2C:132 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;