:: Bounded Domains and Unbounded Domains
:: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski
::
:: Copyright (c) 1999-2019 Association of Mizar Users

registration
let n be Nat;
coherence
proof end;
end;

theorem :: JORDAN2C:1
canceled;

theorem :: JORDAN2C:2
canceled;

theorem :: JORDAN2C:3
canceled;

theorem :: JORDAN2C:4
canceled;

theorem :: JORDAN2C:5
canceled;

::$CT 5 theorem Th1: :: 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 ) proof end; theorem :: JORDAN2C:7 canceled; ::$CT
theorem :: JORDAN2C:8
for n being Nat
for q being Point of () holds = |.q.| by ABSVALUE:def 1;

theorem Th3: :: JORDAN2C:9
for n being Nat
for q1, q2 being Point of () holds |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|
proof end;

theorem Th4: :: JORDAN2C:10
for r being Real holds = |.r.|
proof end;

Lm1: for n being Nat
for r being Real st r > 0 holds
for x, y, z being Element of () st x = 0* n holds
for p being Element of () st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)

proof end;

Lm2: for n being Nat
for r, s being Real st r > 0 holds
for x being Element of () st x = 0* n holds
for A being Subset of () st A = Ball (x,s) holds
r * A = Ball (x,(r * s))

proof end;

Lm3: for n being Nat
for r, s, t being Real st 0 < s & s <= t holds
for x being Element of () st x = 0* n holds
for BA being Subset of () st BA = Ball (x,r) holds
s * BA c= t * BA

proof end;

theorem Th5: :: JORDAN2C:11
for n being Nat
for A being Subset of () holds
( A is bounded iff A is bounded Subset of () )
proof end;

theorem :: JORDAN2C:12
for n being Nat
for A, B being Subset of () st B is bounded & A c= B holds
A is bounded by RLTOPSP1:42;

definition
let n be Nat;
let A, B be Subset of ();
end;

:: deftheorem JORDAN2C:def 1 :
canceled;

:: deftheorem defines is_inside_component_of JORDAN2C:def 2 :
for n being Nat
for A, B being Subset of () 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
proof end;
end;

theorem Th7: :: JORDAN2C:13
for n being Nat
for A, B being Subset of () holds
( B is_inside_component_of A iff ex C being Subset of (() | (A )) st
( C = B & C is a_component & C is bounded Subset of () ) )
proof end;

definition
let n be Nat;
let A, B be Subset of ();
pred B is_outside_component_of A means :: JORDAN2C:def 3
( B is_a_component_of A  & not B is bounded );
end;

:: deftheorem defines is_outside_component_of JORDAN2C:def 3 :
for n being Nat
for A, B being Subset of () holds
( B is_outside_component_of A iff ( B is_a_component_of A  & not B is bounded ) );

theorem Th8: :: JORDAN2C:14
for n being Nat
for A, B being Subset of () holds
( B is_outside_component_of A iff ex C being Subset of (() | (A )) st
( C = B & C is a_component & C is not bounded Subset of () ) )
proof end;

theorem :: JORDAN2C:15
for n being Nat
for A, B being Subset of () st B is_inside_component_of A holds
B c= A  by SPRECT_1:5;

theorem :: JORDAN2C:16
for n being Nat
for A, B being Subset of () 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 ();
func BDD A -> Subset of () equals :: JORDAN2C:def 4
union { B where B is Subset of () : B is_inside_component_of A } ;
correctness
coherence
union { B where B is Subset of () : B is_inside_component_of A } is Subset of ()
;
proof end;
end;

:: deftheorem defines BDD JORDAN2C:def 4 :
for n being Nat
for A being Subset of () holds BDD A = union { B where B is Subset of () : B is_inside_component_of A } ;

definition
let n be Nat;
let A be Subset of ();
func UBD A -> Subset of () equals :: JORDAN2C:def 5
union { B where B is Subset of () : B is_outside_component_of A } ;
correctness
coherence
union { B where B is Subset of () : B is_outside_component_of A } is Subset of ()
;
proof end;
end;

:: deftheorem defines UBD JORDAN2C:def 5 :
for n being Nat
for A being Subset of () holds UBD A = union { B where B is Subset of () : B is_outside_component_of A } ;

registration
let n be Nat;
cluster [#] () -> convex ;
coherence
[#] () is convex
;
end;

registration
let n be Nat;
coherence
[#] () is a_component
proof end;
end;

theorem :: JORDAN2C:17
canceled;

theorem :: JORDAN2C:18
canceled;

theorem :: JORDAN2C:19
canceled;

::$CT 3 theorem Th11: :: JORDAN2C:20 for n being Nat for A being Subset of () holds BDD A is a_union_of_components of () | (A ) proof end; theorem Th12: :: JORDAN2C:21 for n being Nat for A being Subset of () holds UBD A is a_union_of_components of () | (A ) proof end; theorem Th13: :: JORDAN2C:22 for n being Nat for A, B being Subset of () st B is_inside_component_of A holds B c= BDD A proof end; theorem Th14: :: JORDAN2C:23 for n being Nat for A, B being Subset of () st B is_outside_component_of A holds B c= UBD A proof end; theorem Th15: :: JORDAN2C:24 for n being Nat for A being Subset of () holds BDD A misses UBD A proof end; theorem Th16: :: JORDAN2C:25 for n being Nat for A being Subset of () holds BDD A c= A  proof end; theorem Th17: :: JORDAN2C:26 for n being Nat for A being Subset of () holds UBD A c= A  proof end; theorem Th18: :: JORDAN2C:27 for n being Nat for A being Subset of () holds (BDD A) \/ (UBD A) = A  proof end; theorem Th19: :: JORDAN2C:28 for n being Nat for P being Subset of () st P = REAL n holds P is connected proof end; theorem :: JORDAN2C:29 canceled; theorem :: JORDAN2C:30 canceled; theorem :: JORDAN2C:31 canceled; theorem :: JORDAN2C:32 canceled; ::$CT 4
theorem Th20: :: JORDAN2C:33
for n being Nat
for W being Subset of () st n >= 1 & W = REAL n holds
not W is bounded
proof end;

theorem Th21: :: JORDAN2C:34
for n being Nat
for A being Subset of () holds
( A is bounded iff ex r being Real st
for q being Point of () st q in A holds
|.q.| < r )
proof end;

theorem Th22: :: JORDAN2C:35
for n being Nat st n >= 1 holds
not [#] () is bounded
proof end;

theorem Th23: :: JORDAN2C:36
for n being Nat st n >= 1 holds
UBD ({} ()) = REAL n
proof end;

theorem Th24: :: JORDAN2C:37
for n being Nat
for w1, w2, w3 being Point of ()
for P being non empty Subset of ()
for h1, h2 being Function of I,(() | 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,(() | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
proof end;

theorem Th25: :: JORDAN2C:38
for n being Nat
for P being Subset of ()
for w1, w2, w3 being Point of () 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,(() | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
proof end;

theorem Th26: :: JORDAN2C:39
for n being Nat
for P being Subset of ()
for w1, w2, w3, w4 being Point of () 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,(() | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
proof end;

theorem Th27: :: JORDAN2C:40
for n being Nat
for P being Subset of ()
for w1, w2, w3, w4, w5, w6, w7 being Point of () 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,(() | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 )
proof end;

theorem Th28: :: JORDAN2C:41
for n being Nat
for w1, w2 being Point of ()
for P being Subset of () st P = LSeg (w1,w2) & not 0. () in LSeg (w1,w2) holds
ex w0 being Point of () st
( w0 in LSeg (w1,w2) & |.w0.| > 0 & |.w0.| = () . (0. ()) )
proof end;

theorem Th29: :: JORDAN2C:42
for n being Nat
for a being Real
for Q being Subset of ()
for w1, w4 being Point of () st Q = { q where q is Point of () : |.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 () st
( w2 in Q & w3 in Q & LSeg (w1,w2) c= Q & LSeg (w2,w3) c= Q & LSeg (w3,w4) c= Q )
proof end;

theorem Th30: :: JORDAN2C:43
for n being Nat
for a being Real
for Q being Subset of ()
for w1, w4 being Point of () st Q = (REAL n) \ { q where q is Point of () : |.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 () st
( w2 in Q & w3 in Q & LSeg (w1,w2) c= Q & LSeg (w2,w3) c= Q & LSeg (w3,w4) c= Q )
proof end;

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 Th32: :: JORDAN2C:45
for n being 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) ) )
proof end;

theorem Th33: :: JORDAN2C:46
for n being 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 )
proof end;

theorem Th34: :: JORDAN2C:47
for n being 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 )
proof end;

theorem Th35: :: JORDAN2C:48
for n being Nat
for a being Real
for Q being Subset of ()
for w1, w7 being Point of () st n >= 2 & Q = { q where q is Point of () : |.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 () 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 end;

theorem Th36: :: JORDAN2C:49
for n being Nat
for a being Real
for Q being Subset of ()
for w1, w7 being Point of () st n >= 2 & Q = (REAL n) \ { q where q is Point of () : |.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 () 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 end;

theorem Th37: :: JORDAN2C:50
for n being Nat
for a being Real st n >= 1 holds
{ q where q is Point of () : |.q.| > a } <> {}
proof end;

theorem Th38: :: JORDAN2C:51
for n being Nat
for a being Real
for P being Subset of () st n >= 2 & P = { q where q is Point of () : |.q.| > a } holds
P is connected
proof end;

theorem Th39: :: JORDAN2C:52
for n being Nat
for a being Real st n >= 1 holds
(REAL n) \ { q where q is Point of () : |.q.| < a } <> {}
proof end;

theorem Th40: :: JORDAN2C:53
for n being Nat
for a being Real
for P being Subset of () st n >= 2 & P = (REAL n) \ { q where q is Point of () : |.q.| < a } holds
P is connected
proof end;

theorem Th41: :: JORDAN2C:54
for a being Real
for n being Nat
for P being Subset of () st n >= 1 & P = (REAL n) \ { q where q is Point of () : |.q.| < a } holds
not P is bounded
proof end;

theorem Th42: :: JORDAN2C:55
for a being Real
for P being Subset of () st P = { q where q is Point of () : ex r being Real st
( q = <*r*> & r > a )
}
holds
P is convex
proof end;

theorem Th43: :: JORDAN2C:56
for a being Real
for P being Subset of () st P = { q where q is Point of () : ex r being Real st
( q = <*r*> & r < - a )
}
holds
P is convex
proof end;

theorem :: JORDAN2C:57
canceled;

theorem :: JORDAN2C:58
canceled;

::$CT 2 theorem Th44: :: JORDAN2C:59 for W being Subset of () for a being Real st W = { q where q is Point of () : ex r being Real st ( q = <*r*> & r > a ) } holds not W is bounded proof end; theorem Th45: :: JORDAN2C:60 for W being Subset of () for a being Real st W = { q where q is Point of () : ex r being Real st ( q = <*r*> & r < - a ) } holds not W is bounded proof end; theorem Th46: :: JORDAN2C:61 for n being Nat for W being Subset of () for a being Real st n >= 2 & W = { q where q is Point of () : |.q.| > a } holds not W is bounded proof end; theorem Th47: :: JORDAN2C:62 for n being Nat for W being Subset of () for a being Real st n >= 2 & W = (REAL n) \ { q where q is Point of () : |.q.| < a } holds not W is bounded proof end; theorem Th48: :: JORDAN2C:63 for n being Nat for P, P1, Q being Subset of () for W being Subset of () 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 proof end; theorem Th49: :: JORDAN2C:64 for n being Nat for A being Subset of () for B being non empty Subset of () for C being Subset of (() | B) st A = C & C is bounded holds A is bounded proof end; theorem Th50: :: JORDAN2C:65 for n being Nat for A being Subset of () st A is compact holds A is bounded proof end; registration let n be Element of NAT ; cluster compact -> bounded for Element of bool the carrier of (); coherence for b1 being Subset of () st b1 is compact holds b1 is bounded by Th50; end; theorem Th51: :: JORDAN2C:66 for n being Nat for A being Subset of () st 1 <= n & A is bounded holds A  <> {} proof end; theorem Th52: :: JORDAN2C:67 for n being Nat for r being Real holds ( ex B being Subset of () st B = { q where q is Point of () : |.q.| < r } & ( for A being Subset of () st A = { q1 where q1 is Point of () : |.q1.| < r } holds A is bounded ) ) proof end; theorem Th53: :: JORDAN2C:68 for n being Nat for A being Subset of () st n >= 2 & A is bounded holds UBD A is_outside_component_of A proof end; theorem Th54: :: JORDAN2C:69 for n being Nat for a being Real for P being Subset of () st P = { q where q is Point of () : |.q.| < a } holds P is convex proof end; theorem Th55: :: JORDAN2C:70 for n being Nat for u being Point of () for a being Real for P being Subset of () st P = Ball (u,a) holds P is convex proof end; theorem :: JORDAN2C:71 canceled; ::$CT
theorem Th56: :: JORDAN2C:72
for n being Nat
for r being Real
for p, q being Point of ()
for u being Point of () st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex h being Function of I,() st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
proof end;

theorem Th57: :: JORDAN2C:73
for n being Nat
for r being Real
for p, p1, p2 being Point of ()
for u being Point of ()
for f being Function of I,() 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,() st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
proof end;

theorem Th58: :: JORDAN2C:74
for n being Nat
for r being Real
for p, p1, p2 being Point of ()
for u being Point of ()
for P being Subset of ()
for f being Function of I,() 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,() st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
proof end;

theorem Th59: :: JORDAN2C:75
for n being Nat
for R being Subset of ()
for p being Point of ()
for P being Subset of () st R is connected & R is open & P = { q where q is Point of () : ( q <> p & q in R & ( for f being Function of I,() 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
proof end;

theorem Th60: :: JORDAN2C:76
for n being Nat
for p being Point of ()
for R, P being Subset of () st R is connected & R is open & p in R & P = { q where q is Point of () : ( q = p or ex f being Function of I,() st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
P is open
proof end;

theorem Th61: :: JORDAN2C:77
for n being Nat
for p being Point of ()
for P, R being Subset of () st p in R & P = { q where q is Point of () : ( q = p or ex f being Function of I,() st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
P c= R
proof end;

theorem Th62: :: JORDAN2C:78
for n being Nat
for P, R being Subset of ()
for p being Point of () st R is connected & R is open & p in R & P = { q where q is Point of () : ( q = p or ex f being Function of I,() st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
}
holds
R c= P
proof end;

theorem Th63: :: JORDAN2C:79
for n being Nat
for R being Subset of ()
for p, q being Point of () st R is connected & R is open & p in R & q in R & p <> q holds
ex f being Function of I,() st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q )
proof end;

theorem Th64: :: JORDAN2C:80
for n being Nat
for A being Subset of ()
for a being Real st A = { q where q is Point of () : |.q.| = a } holds
( A  is open & A is closed )
proof end;

theorem Th65: :: JORDAN2C:81
for n being Nat
for B being non empty Subset of () st B is open holds
() | B is locally_connected
proof end;

theorem Th66: :: JORDAN2C:82
for n being Nat
for B being non empty Subset of ()
for A being Subset of ()
for a being Real st A = { q where q is Point of () : |.q.| = a } & A  = B holds
() | B is locally_connected
proof end;

theorem Th67: :: JORDAN2C:83
for n being Nat
for f being Function of (),R^1 st ( for q being Point of () holds f . q = |.q.| ) holds
f is continuous
proof end;

theorem Th68: :: JORDAN2C:84
for n being Nat ex f being Function of (),R^1 st
( ( for q being Point of () holds f . q = |.q.| ) & f is continuous )
proof end;

theorem Th69: :: JORDAN2C:85
for n being Nat
for g being Function of I,() st g is continuous holds
ex f being Function of I,R^1 st
( ( for t being Point of I holds f . t = |.(g . t).| ) & f is continuous )
proof end;

theorem Th70: :: JORDAN2C:86
for n being Nat
for g being Function of I,()
for a being Real st g is continuous & |.(g /. 0).| <= a & a <= |.(g /. 1).| holds
ex s being Point of I st |.(g /. s).| = a
proof end;

theorem Th71: :: JORDAN2C:87
for n being Nat
for r being Real
for q being Point of () st q = <*r*> holds
|.q.| = |.r.|
proof end;

theorem :: JORDAN2C:88
for n being Nat
for A being Subset of ()
for a being Real st n >= 1 & a > 0 & A = { q where q is Point of () : |.q.| = a } holds
BDD A is_inside_component_of A
proof end;

theorem Th73: :: JORDAN2C:89
for D being non empty compact non horizontal non vertical Subset of () holds
( len (GoB ()) = 2 & width (GoB ()) = 2 & () /. 1 = (GoB ()) * (1,2) & () /. 2 = (GoB ()) * (2,2) & () /. 3 = (GoB ()) * (2,1) & () /. 4 = (GoB ()) * (1,1) & () /. 5 = (GoB ()) * (1,2) )
proof end;

theorem Th74: :: JORDAN2C:90
for D being non empty compact non horizontal non vertical Subset of () holds not LeftComp () is bounded
proof end;

theorem Th75: :: JORDAN2C:91
for D being non empty compact non horizontal non vertical Subset of () holds LeftComp () c= UBD (L~ ())
proof end;

theorem Th76: :: 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
proof end;

theorem Th77: :: JORDAN2C:93
for D being non empty compact non horizontal non vertical Subset of ()
for B being Subset of () st B is_a_component_of (L~ ())  & not B is bounded holds
B = LeftComp ()
proof end;

theorem Th78: :: JORDAN2C:94
for D being non empty compact non horizontal non vertical Subset of () holds
( RightComp () c= BDD (L~ ()) & RightComp () is bounded )
proof end;

theorem Th79: :: JORDAN2C:95
for D being non empty compact non horizontal non vertical Subset of () holds
( LeftComp () = UBD (L~ ()) & RightComp () = BDD (L~ ()) )
proof end;

theorem Th80: :: JORDAN2C:96
for D being non empty compact non horizontal non vertical Subset of () holds
( UBD (L~ ()) <> {} & UBD (L~ ()) is_outside_component_of L~ () & BDD (L~ ()) <> {} & BDD (L~ ()) is_inside_component_of L~ () )
proof end;

theorem Th81: :: 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 ) )
proof end;

theorem Th82: :: JORDAN2C:98
for A being Subset of () st A  <> {} holds
( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of () st
( A  = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of (() | (A )) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) )
proof end;

theorem Th83: :: JORDAN2C:99
for n being Nat
for p being Point of ()
for P being Subset of () st n >= 1 & P = {p} holds
P is boundary
proof end;

theorem Th84: :: JORDAN2C:100
for p, q being Point of ()
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. () )
proof end;

theorem Th85: :: JORDAN2C:101
for q1, q2 being Point of () holds LSeg (q1,q2) is boundary
proof end;

registration
let q1, q2 be Point of ();
cluster LSeg (q1,q2) -> boundary ;
coherence
LSeg (q1,q2) is boundary
by Th85;
end;

theorem Th86: :: JORDAN2C:102
for f being FinSequence of () holds L~ f is boundary
proof end;

registration
let f be FinSequence of ();
coherence
L~ f is boundary
by Th86;
end;

theorem Th87: :: JORDAN2C:103
for n being Nat
for r being Real
for ep being Point of ()
for p, q being Point of () st p = ep & q in Ball (ep,r) holds
( |.(p - q).| < r & |.(q - p).| < r )
proof end;

theorem :: JORDAN2C:104
for D being non empty compact non horizontal non vertical Subset of ()
for a being Real
for p being Point of () st a > 0 & p in L~ () holds
ex q being Point of () st
( q in UBD (L~ ()) & |.(p - q).| < a )
proof end;

theorem :: JORDAN2C:105
REAL 0 = {(0. ())} by EUCLID:77;

theorem Th90: :: JORDAN2C:106
for n being Nat
for A being Subset of () st A is bounded holds
BDD A is bounded
proof end;

theorem Th91: :: 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
proof end;

theorem Th92: :: JORDAN2C:108
for A being Subset of () st A is bounded & A is Jordan holds
BDD A is_inside_component_of A
proof end;

theorem :: JORDAN2C:109
for D being non empty compact non horizontal non vertical Subset of ()
for a being Real
for p being Point of () st a > 0 & p in L~ () holds
ex q being Point of () st
( q in BDD (L~ ()) & |.(p - q).| < a )
proof end;

theorem :: JORDAN2C:110
for f being V23() standard clockwise_oriented special_circular_sequence
for p being Point of () st f /. 1 = N-min (L~ f) & p 1 < W-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:111
for f being V23() standard clockwise_oriented special_circular_sequence
for p being Point of () st f /. 1 = N-min (L~ f) & p 1 > E-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:112
for f being V23() standard clockwise_oriented special_circular_sequence
for p being Point of () st f /. 1 = N-min (L~ f) & p 2 < S-bound (L~ f) holds
p in LeftComp f
proof end;

theorem :: JORDAN2C:113
for f being V23() standard clockwise_oriented special_circular_sequence
for p being Point of () st f /. 1 = N-min (L~ f) & p 2 > N-bound (L~ f) holds
p in LeftComp f
proof end;

:: 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
proof end;

theorem :: JORDAN2C:115
for n being Nat
for A, B being Subset of () st B is_inside_component_of A holds
B is connected
proof end;

theorem Th100: :: JORDAN2C:116
for n being Nat
for A, B being Subset of () st B is_outside_component_of A holds
B is connected
proof end;

theorem :: JORDAN2C:117
for n being Nat
for A, B being Subset of () st B is_a_component_of A  holds
A misses B by ;

theorem :: JORDAN2C:118
for n being Nat
for R, P, Q being Subset of () st P is_outside_component_of Q & R is_inside_component_of Q holds
P misses R
proof end;

theorem :: JORDAN2C:119
for n being Nat st 2 <= n holds
for A, B, P being Subset of () st P is bounded & A is_outside_component_of P & B is_outside_component_of P holds
A = B
proof end;

registration
let C be closed Subset of ();
cluster BDD C -> open ;
coherence
BDD C is open
proof end;
cluster UBD C -> open ;
coherence
UBD C is open
proof end;
end;

registration
let C be compact Subset of ();
coherence
UBD C is connected
by ;
end;

theorem Th104: :: JORDAN2C:120
for p being Point of () holds not west_halfline p is bounded
proof end;

theorem Th105: :: JORDAN2C:121
for p being Point of () holds not east_halfline p is bounded
proof end;

theorem Th106: :: JORDAN2C:122
for p being Point of () holds not north_halfline p is bounded
proof end;

theorem Th107: :: JORDAN2C:123
for p being Point of () holds not south_halfline p is bounded
proof end;

registration
let C be compact Subset of ();
cluster UBD C -> non empty ;
coherence
not UBD C is empty
proof end;
end;

theorem Th108: :: JORDAN2C:124
for C being compact Subset of () holds UBD C is_a_component_of C
proof end;

theorem Th109: :: JORDAN2C:125
for C being compact Subset of ()
for WH being connected Subset of () st not WH is bounded & WH misses C holds
WH c= UBD C
proof end;

theorem :: JORDAN2C:126
for C being compact Subset of ()
for p being Point of () st west_halfline p misses C holds
west_halfline p c= UBD C
proof end;

theorem :: JORDAN2C:127
for C being compact Subset of ()
for p being Point of () st east_halfline p misses C holds
east_halfline p c= UBD C
proof end;

theorem :: JORDAN2C:128
for C being compact Subset of ()
for p being Point of () st south_halfline p misses C holds
south_halfline p c= UBD C
proof end;

theorem :: JORDAN2C:129
for C being compact Subset of ()
for p being Point of () st north_halfline p misses C holds
north_halfline p c= UBD C
proof end;

theorem :: JORDAN2C:130
for n being Nat
for r being Real st r > 0 holds
for x, y, z being Element of () st x = 0* n holds
for p being Element of () 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 () st x = 0* n holds
for A being Subset of () 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 () st x = 0* n holds
for BA being Subset of () st BA = Ball (x,r) holds
s * BA c= t * BA by Lm3;