:: Bounded Domains and Unbounded Domains :: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski :: :: Received January 7, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin registration let n be Nat; cluster TOP-REAL n -> add-continuous Mult-continuous ; coherence ( TOP-REAL n is add-continuous & TOP-REAL n is Mult-continuous ) proofend; end; begin theorem :: JORDAN2C:1 canceled; theorem :: JORDAN2C:2 canceled; theorem :: JORDAN2C:3 canceled; theorem :: JORDAN2C:4 canceled; theorem :: JORDAN2C:5 canceled; theorem Th6: :: JORDAN2C:6 for r, s being Real for f being increasing FinSequence of REAL st rng f = {r,s} & len f = 2 & r <= s holds ( f . 1 = r & f . 2 = s ) proofend; theorem :: JORDAN2C:7 canceled; theorem :: JORDAN2C:8 for n being Element of NAT for q being Point of (TOP-REAL n) holds abs |.q.| = |.q.| by ABSVALUE:def_1; theorem Th9: :: JORDAN2C:9 for n being Element of NAT for q1, q2 being Point of (TOP-REAL n) holds abs (|.q1.| - |.q2.|) <= |.(q1 - q2).| proofend; theorem Th10: :: JORDAN2C:10 for r being Real holds |.|[r]|.| = abs r proofend; Lm1: for n being Nat for r being Real st r > 0 holds for x, y, z being Element of (Euclid n) st x = 0* n holds for p being Element of (TOP-REAL n) st p = y & r * p = z holds r * (dist (x,y)) = dist (x,z) proofend; Lm2: for n being Nat for r, s being Real st r > 0 holds for x being Element of (Euclid n) st x = 0* n holds for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds r * A = Ball (x,(r * s)) proofend; Lm3: for n being Nat for r, s, t being Real st 0 < s & s <= t holds for x being Element of (Euclid n) st x = 0* n holds for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds s * BA c= t * BA proofend; theorem Th11: :: JORDAN2C:11 for n being Nat for A being Subset of (TOP-REAL n) holds ( A is bounded iff A is bounded Subset of (Euclid n) ) proofend; theorem :: JORDAN2C:12 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is bounded & A c= B holds A is bounded by RLTOPSP1:42; definition canceled; let n be Nat; let A, B be Subset of (TOP-REAL n); predB is_inside_component_of A means :Def2: :: JORDAN2C:def 2 ( B is_a_component_of A ` & B is bounded ); end; :: deftheorem JORDAN2C:def_1_:_ canceled; :: deftheorem Def2 defines is_inside_component_of JORDAN2C:def_2_:_ for n being Nat for A, B being Subset of (TOP-REAL n) holds ( B is_inside_component_of A iff ( B is_a_component_of A ` & B is bounded ) ); registration let M be non empty MetrStruct ; cluster bounded for Element of bool the carrier of M; existence ex b1 being Subset of M st b1 is bounded proofend; end; theorem Th13: :: JORDAN2C:13 for n being Element of NAT for A, 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) ) ) proofend; definition let n be Nat; let A, B be Subset of (TOP-REAL n); predB is_outside_component_of A means :Def3: :: JORDAN2C:def 3 ( B is_a_component_of A ` & not B is bounded ); end; :: deftheorem Def3 defines is_outside_component_of JORDAN2C:def_3_:_ for n being Nat for A, B being Subset of (TOP-REAL n) holds ( B is_outside_component_of A iff ( B is_a_component_of A ` & not B is bounded ) ); theorem Th14: :: JORDAN2C:14 for n being Element of NAT for A, 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) ) ) proofend; theorem :: JORDAN2C:15 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds B c= A ` proofend; theorem :: JORDAN2C:16 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds B c= A ` proofend; 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 } ; correctness coherence union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } is Subset of (TOP-REAL n); proofend; end; :: deftheorem defines BDD JORDAN2C:def_4_:_ for n being Nat for A being Subset of (TOP-REAL n) holds BDD A = union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ; 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 } ; correctness coherence union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } is Subset of (TOP-REAL n); proofend; end; :: deftheorem defines UBD JORDAN2C:def_5_:_ for n being Nat for A being Subset of (TOP-REAL n) holds UBD A = union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } ; registration let n be Nat; cluster [#] (TOP-REAL n) -> convex ; coherence [#] (TOP-REAL n) is convex proofend; end; registration let n be Element of NAT ; cluster [#] (TOP-REAL n) -> a_component ; coherence [#] (TOP-REAL n) is a_component proofend; end; theorem :: JORDAN2C:17 canceled; theorem :: JORDAN2C:18 canceled; theorem :: JORDAN2C:19 canceled; theorem Th20: :: JORDAN2C:20 for n being Element of NAT for A being Subset of (TOP-REAL n) holds BDD A is a_union_of_components of (TOP-REAL n) | (A `) proofend; theorem Th21: :: JORDAN2C:21 for n being Element of NAT for A being Subset of (TOP-REAL n) holds UBD A is a_union_of_components of (TOP-REAL n) | (A `) proofend; theorem Th22: :: JORDAN2C:22 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds B c= BDD A proofend; theorem Th23: :: JORDAN2C:23 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds B c= UBD A proofend; theorem Th24: :: JORDAN2C:24 for n being Element of NAT for A being Subset of (TOP-REAL n) holds BDD A misses UBD A proofend; theorem Th25: :: JORDAN2C:25 for n being Element of NAT for A being Subset of (TOP-REAL n) holds BDD A c= A ` proofend; theorem Th26: :: JORDAN2C:26 for n being Element of NAT for A being Subset of (TOP-REAL n) holds UBD A c= A ` proofend; theorem Th27: :: JORDAN2C:27 for n being Element of NAT for A being Subset of (TOP-REAL n) holds (BDD A) \/ (UBD A) = A ` proofend; theorem Th28: :: JORDAN2C:28 for n being Element of NAT for P being Subset of (TOP-REAL n) st P = REAL n holds P is connected proofend; theorem :: JORDAN2C:29 canceled; theorem :: JORDAN2C:30 canceled; theorem :: JORDAN2C:31 canceled; theorem :: JORDAN2C:32 canceled; theorem Th33: :: JORDAN2C:33 for n being Element of NAT for W being Subset of (Euclid n) st n >= 1 & W = REAL n holds not W is bounded proofend; theorem Th34: :: JORDAN2C:34 for n being Element of NAT 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 ) proofend; theorem Th35: :: JORDAN2C:35 for n being Element of NAT st n >= 1 holds not [#] (TOP-REAL n) is bounded proofend; theorem Th36: :: JORDAN2C:36 for n being Element of NAT st n >= 1 holds UBD ({} (TOP-REAL n)) = REAL n proofend; theorem Th37: :: JORDAN2C:37 for n being Element of NAT for w1, w2, w3 being Point of (TOP-REAL n) for P being non empty Subset of (TOP-REAL n) for 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 ) proofend; theorem Th38: :: JORDAN2C:38 for n being Element of NAT for P being Subset of (TOP-REAL n) for 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 holds ex h being Function of I[01],((TOP-REAL n) | P) st ( h is continuous & w1 = h . 0 & w3 = h . 1 ) proofend; theorem Th39: :: JORDAN2C:39 for n being Element of NAT for P being Subset of (TOP-REAL n) for 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 holds ex h being Function of I[01],((TOP-REAL n) | P) st ( h is continuous & w1 = h . 0 & w4 = h . 1 ) proofend; theorem Th40: :: JORDAN2C:40 for n being Element of NAT for P being Subset of (TOP-REAL n) for 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 holds ex h being Function of I[01],((TOP-REAL n) | P) st ( h is continuous & w1 = h . 0 & w7 = h . 1 ) proofend; theorem Th41: :: JORDAN2C:41 for n being Element of NAT for w1, w2 being Point of (TOP-REAL n) for 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)) ) proofend; theorem Th42: :: JORDAN2C:42 for n being Element of NAT for a being Real for Q being Subset of (TOP-REAL n) for w1, w4 being Point of (TOP-REAL n) st Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } & w1 in Q & w4 in Q & ( for r being Real holds ( not w1 = r * w4 & not 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 ) proofend; theorem Th43: :: JORDAN2C:43 for n being Element of NAT for a being Real for Q being Subset of (TOP-REAL n) for w1, w4 being Point of (TOP-REAL n) st Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & w1 in Q & w4 in Q & ( for r being Real holds ( not w1 = r * w4 & not 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 ) proofend; 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)) ) by EUCLID:76; theorem Th45: :: JORDAN2C:45 for n being Element of NAT for x being Element of REAL n for f, g being FinSequence of REAL for 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) ) ) proofend; theorem Th46: :: JORDAN2C:46 for n being Element of NAT for x being Element of REAL n for f being FinSequence st x <> 0* n & x = f holds ex i being Element of NAT st ( 1 <= i & i <= n & f . i <> 0 ) proofend; theorem Th47: :: JORDAN2C:47 for n being Element of NAT for x being Element of REAL n st n >= 2 & x <> 0* n holds ex y being Element of REAL n st for r being Real holds ( not y = r * x & not x = r * y ) proofend; theorem Th48: :: JORDAN2C:48 for n being Element of NAT for a being Real for Q being Subset of (TOP-REAL n) for w1, w7 being Point of (TOP-REAL n) st n >= 2 & Q = { q where q is Point of (TOP-REAL n) : |.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 ) proofend; theorem Th49: :: JORDAN2C:49 for n being Element of NAT for a being Real for Q being Subset of (TOP-REAL n) for w1, w7 being Point of (TOP-REAL n) st n >= 2 & Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.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 ) proofend; theorem Th50: :: JORDAN2C:50 for n being Element of NAT for a being Real st n >= 1 holds { q where q is Point of (TOP-REAL n) : |.q.| > a } <> {} proofend; theorem Th51: :: JORDAN2C:51 for n being Element of NAT for a being Real for P being Subset of (TOP-REAL n) st n >= 2 & P = { q where q is Point of (TOP-REAL n) : |.q.| > a } holds P is connected proofend; theorem Th52: :: JORDAN2C:52 for n being Element of NAT for a being Real st n >= 1 holds (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {} proofend; theorem Th53: :: JORDAN2C:53 for n being Element of NAT for a being Real for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds P is connected proofend; theorem Th54: :: JORDAN2C:54 for a being Real for n being Element of NAT for 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 proofend; theorem Th55: :: JORDAN2C:55 for a being Real for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st ( q = <*r*> & r > a ) } holds P is convex proofend; theorem Th56: :: JORDAN2C:56 for a being Real for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st ( q = <*r*> & r < - a ) } holds P is convex proofend; theorem :: JORDAN2C:57 canceled; theorem :: JORDAN2C:58 canceled; theorem Th59: :: JORDAN2C:59 for W being Subset of (Euclid 1) for a being Real st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st ( q = <*r*> & r > a ) } holds not W is bounded proofend; theorem Th60: :: JORDAN2C:60 for W being Subset of (Euclid 1) for a being Real st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st ( q = <*r*> & r < - a ) } holds not W is bounded proofend; theorem Th61: :: JORDAN2C:61 for n being Element of NAT for W being Subset of (Euclid n) for a being Real st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } holds not W is bounded proofend; theorem Th62: :: JORDAN2C:62 for n being Element of NAT for W being Subset of (Euclid n) for a being Real st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds not W is bounded proofend; theorem Th63: :: JORDAN2C:63 for n being Element of NAT for P, P1, Q being Subset of (TOP-REAL n) for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q holds P1 is_outside_component_of Q proofend; theorem Th64: :: JORDAN2C:64 for n being Element of NAT for A being Subset of (Euclid n) for B being non empty Subset of (Euclid n) for C being Subset of ((Euclid n) | B) st A = C & C is bounded holds A is bounded proofend; theorem Th65: :: JORDAN2C:65 for n being Element of NAT for A being Subset of (TOP-REAL n) st A is compact holds A is bounded proofend; registration let n be Element of NAT ; cluster compact -> bounded for Element of bool the carrier of (TOP-REAL n); coherence for b1 being Subset of (TOP-REAL n) st b1 is compact holds b1 is bounded by Th65; end; theorem Th66: :: JORDAN2C:66 for n being Element of NAT for A being Subset of (TOP-REAL n) st 1 <= n & A is bounded holds A ` <> {} proofend; theorem Th67: :: JORDAN2C:67 for n being Element of NAT for r being Real holds ( ex B being Subset of (Euclid n) st B = { q where q is Point of (TOP-REAL n) : |.q.| < r } & ( for A being Subset of (Euclid n) st A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } holds A is bounded ) ) proofend; theorem Th68: :: JORDAN2C:68 for n being Element of NAT for A being Subset of (TOP-REAL n) st n >= 2 & A is bounded holds UBD A is_outside_component_of A proofend; theorem Th69: :: JORDAN2C:69 for n being Element of NAT for a being Real for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds P is convex proofend; theorem Th70: :: JORDAN2C:70 for n being Element of NAT for u being Point of (Euclid n) for a being Real for P being Subset of (TOP-REAL n) st P = Ball (u,a) holds P is convex proofend; theorem :: JORDAN2C:71 canceled; theorem Th72: :: JORDAN2C:72 for n being Element of NAT for r being Real for p, q being Point of (TOP-REAL n) for u being Point of (Euclid n) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds 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) ) proofend; theorem Th73: :: JORDAN2C:73 for n being Element of NAT for r being Real for p1, p2, p being Point of (TOP-REAL n) for u being Point of (Euclid n) 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) holds 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)) ) proofend; theorem Th74: :: JORDAN2C:74 for n being Element of NAT for r being Real for p1, p2, p being Point of (TOP-REAL n) for u being Point of (Euclid n) for P being Subset of (TOP-REAL n) 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 holds ex f1 being Function of I[01],(TOP-REAL n) st ( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p ) proofend; theorem Th75: :: JORDAN2C:75 for n being Element of NAT for R being Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st R is connected & R is open & P = { q where q is Point of (TOP-REAL n) : ( q <> p & q in R & ( for f being Function of I[01],(TOP-REAL n) holds ( not f is continuous or not rng f c= R or not f . 0 = p or not f . 1 = q ) ) ) } holds P is open proofend; theorem Th76: :: JORDAN2C:76 for n being Element of NAT for p being Point of (TOP-REAL n) for R, P being Subset of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( 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 proofend; theorem Th77: :: JORDAN2C:77 for n being Element of NAT for p being Point of (TOP-REAL n) for P, R being Subset of (TOP-REAL n) st p in R & P = { q where q is Point of (TOP-REAL n) : ( 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 c= R proofend; theorem Th78: :: JORDAN2C:78 for n being Element of NAT for P, R being Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( 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 proofend; theorem Th79: :: JORDAN2C:79 for n being Element of NAT for R being Subset of (TOP-REAL n) for 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 ) proofend; theorem Th80: :: JORDAN2C:80 for n being Element of NAT for A being Subset of (TOP-REAL n) for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds ( A ` is open & A is closed ) proofend; theorem Th81: :: JORDAN2C:81 for n being Element of NAT for B being non empty Subset of (TOP-REAL n) st B is open holds (TOP-REAL n) | B is locally_connected proofend; theorem Th82: :: JORDAN2C:82 for n being Element of NAT for B being non empty Subset of (TOP-REAL n) for A being Subset of (TOP-REAL n) for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B holds (TOP-REAL n) | B is locally_connected proofend; theorem Th83: :: JORDAN2C:83 for n being Element of NAT for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) holds f is continuous proofend; theorem Th84: :: JORDAN2C:84 for n being Element of NAT ex f being Function of (TOP-REAL n),R^1 st ( ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) & f is continuous ) proofend; theorem Th85: :: JORDAN2C:85 for n being Element of NAT 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 ) proofend; theorem Th86: :: JORDAN2C:86 for n being Element of NAT for g being Function of I[01],(TOP-REAL n) for 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 proofend; theorem Th87: :: JORDAN2C:87 for n being Element of NAT for r being Real for q being Point of (TOP-REAL n) st q = <*r*> holds |.q.| = abs r proofend; theorem :: JORDAN2C:88 for n being Element of NAT for A being Subset of (TOP-REAL n) for a being Real st n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds BDD A is_inside_component_of A proofend; begin theorem Th89: :: JORDAN2C:89 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 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) ) proofend; theorem Th90: :: JORDAN2C:90 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds not LeftComp (SpStSeq D) is bounded proofend; theorem Th91: :: JORDAN2C:91 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D)) proofend; theorem Th92: :: JORDAN2C:92 for G being TopSpace for 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 proofend; theorem Th93: :: JORDAN2C:93 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) 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) proofend; theorem Th94: :: JORDAN2C:94 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) & RightComp (SpStSeq D) is bounded ) proofend; theorem Th95: :: JORDAN2C:95 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) & RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) ) proofend; theorem Th96: :: JORDAN2C:96 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 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) ) proofend; begin theorem Th97: :: JORDAN2C:97 for G being non empty TopSpace for A being Subset of G st A ` <> {} holds ( A is boundary iff for x being set for V being Subset of G st x in A & x in V & V is open holds ex B being Subset of G st ( B is_a_component_of A ` & V meets B ) ) proofend; theorem Th98: :: 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 ) ) ) ) proofend; theorem Th99: :: JORDAN2C:99 for n being Element of NAT for p being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st n >= 1 & P = {p} holds P is boundary proofend; theorem Th100: :: JORDAN2C:100 for p, q being Point of (TOP-REAL 2) for r being Real st p `1 = q `2 & - (p `2) = q `1 & p = r * q holds ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) ) proofend; theorem Th101: :: JORDAN2C:101 for q1, q2 being Point of (TOP-REAL 2) holds LSeg (q1,q2) is boundary proofend; registration let q1, q2 be Point of (TOP-REAL 2); cluster LSeg (q1,q2) -> boundary ; coherence LSeg (q1,q2) is boundary by Th101; end; theorem Th102: :: JORDAN2C:102 for f being FinSequence of (TOP-REAL 2) holds L~ f is boundary proofend; registration let f be FinSequence of (TOP-REAL 2); cluster L~ f -> boundary ; coherence L~ f is boundary by Th102; end; theorem Th103: :: JORDAN2C:103 for n being Element of NAT for r being Real for ep being Point of (Euclid n) for p, q being Point of (TOP-REAL n) st p = ep & q in Ball (ep,r) holds ( |.(p - q).| < r & |.(q - p).| < r ) proofend; theorem :: JORDAN2C:104 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for a being Real for 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 ) proofend; theorem :: JORDAN2C:105 REAL 0 = {(0. (TOP-REAL 0))} by EUCLID:77; theorem Th106: :: JORDAN2C:106 for n being Element of NAT for A being Subset of (TOP-REAL n) st A is bounded holds BDD A is bounded proofend; theorem Th107: :: JORDAN2C:107 for G being non empty TopSpace for 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 proofend; theorem Th108: :: JORDAN2C:108 for A being Subset of (TOP-REAL 2) st A is bounded & A is Jordan holds BDD A is_inside_component_of A proofend; theorem :: JORDAN2C:109 for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for a being Real for 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 ) proofend; begin theorem :: JORDAN2C:110 for f being non constant standard clockwise_oriented special_circular_sequence 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 proofend; theorem :: JORDAN2C:111 for f being non constant standard clockwise_oriented special_circular_sequence 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 proofend; theorem :: JORDAN2C:112 for f being non constant standard clockwise_oriented special_circular_sequence 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 proofend; theorem :: JORDAN2C:113 for f being non constant standard clockwise_oriented special_circular_sequence 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 proofend; :: Moved from GOBRD14, AK, 22.02.2006 theorem :: JORDAN2C:114 for T being TopSpace for A, B being Subset of T st B is_a_component_of A holds B is connected proofend; theorem :: JORDAN2C:115 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds B is connected proofend; theorem Th116: :: JORDAN2C:116 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds B is connected proofend; theorem :: JORDAN2C:117 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st B is_a_component_of A ` holds A misses B proofend; theorem :: JORDAN2C:118 for n being Element of NAT for R, P, Q being Subset of (TOP-REAL n) st P is_outside_component_of Q & R is_inside_component_of Q holds P misses R proofend; theorem :: JORDAN2C:119 for n being Element of NAT st 2 <= n holds 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 proofend; registration let C be closed Subset of (TOP-REAL 2); cluster BDD C -> open ; coherence BDD C is open proofend; cluster UBD C -> open ; coherence UBD C is open proofend; end; registration let C be compact Subset of (TOP-REAL 2); cluster UBD C -> connected ; coherence UBD C is connected by Th68, Th116; end; theorem Th120: :: JORDAN2C:120 for p being Point of (TOP-REAL 2) holds not west_halfline p is bounded proofend; theorem Th121: :: JORDAN2C:121 for p being Point of (TOP-REAL 2) holds not east_halfline p is bounded proofend; theorem Th122: :: JORDAN2C:122 for p being Point of (TOP-REAL 2) holds not north_halfline p is bounded proofend; theorem Th123: :: JORDAN2C:123 for p being Point of (TOP-REAL 2) holds not south_halfline p is bounded proofend; registration let C be compact Subset of (TOP-REAL 2); cluster UBD C -> non empty ; coherence not UBD C is empty proofend; end; theorem Th124: :: JORDAN2C:124 for C being compact Subset of (TOP-REAL 2) holds UBD C is_a_component_of C ` proofend; theorem Th125: :: JORDAN2C:125 for C being compact Subset of (TOP-REAL 2) for WH being connected Subset of (TOP-REAL 2) st not WH is bounded & WH misses C holds WH c= UBD C proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: JORDAN2C:130 for n being Nat for r being Real st r > 0 holds for x, y, z being Element of (Euclid n) st x = 0* n holds 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 :: JORDAN2C:131 for n being Nat for r, s being Real st r > 0 holds for x being Element of (Euclid n) st x = 0* n holds for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds r * A = Ball (x,(r * s)) by Lm2; theorem :: JORDAN2C:132 for n being Nat for r, s, t being Real st 0 < s & s <= t holds for x being Element of (Euclid n) st x = 0* n holds for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds s * BA c= t * BA by Lm3;