:: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski

::

:: Received January 7, 1999

:: Copyright (c) 1999 Association of Mizar Users

begin

theorem Th1: :: JORDAN2C:1

proof end;

theorem Th2: :: JORDAN2C:2

proof end;

theorem Th3: :: JORDAN2C:3

for n, m being Element of NAT st n <= m & m <= n + 3 & not m = n & not m = n + 1 & not m = n + 2 holds

m = n + 3

m = n + 3

proof end;

theorem Th4: :: JORDAN2C:4

for n, m being Element of NAT st n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 holds

m = n + 4

m = n + 4

proof end;

theorem :: JORDAN2C:5

canceled;

theorem :: JORDAN2C:6

canceled;

theorem Th7: :: JORDAN2C:7

for x, y being set

for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds

( f . 1 = y & f . 2 = x )

for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds

( f . 1 = y & f . 2 = x )

proof end;

theorem Th8: :: JORDAN2C:8

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 )

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:9

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) - p3 = (p1 - p3) + p2 by EUCLID:30;

for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) - p3 = (p1 - p3) + p2 by EUCLID:30;

theorem :: JORDAN2C:10

for n being Element of NAT

for q being Point of (TOP-REAL n) holds abs |.q.| = |.q.| by ABSVALUE:def 1;

for q being Point of (TOP-REAL n) holds abs |.q.| = |.q.| by ABSVALUE:def 1;

theorem Th11: :: JORDAN2C:11

for n being Element of NAT

for q1, q2 being Point of (TOP-REAL n) holds abs (|.q1.| - |.q2.|) <= |.(q1 - q2).|

for q1, q2 being Point of (TOP-REAL n) holds abs (|.q1.| - |.q2.|) <= |.(q1 - q2).|

proof end;

theorem Th12: :: JORDAN2C:12

proof end;

theorem :: JORDAN2C:13

canceled;

theorem :: JORDAN2C:14

canceled;

theorem Th15: :: JORDAN2C:15

for G being non empty TopSpace

for P, A being Subset of G

for Q being Subset of (G | A) st P = Q & P is connected holds

Q is connected

for P, A being Subset of G

for Q being Subset of (G | A) st P = Q & P is connected holds

Q is connected

proof end;

definition

let n be Nat;

let A be Subset of (TOP-REAL n);

canceled;

attr A is Bounded means :Def2: :: JORDAN2C:def 2

A is bounded Subset of (Euclid n);

correctness

;

end;
let A be Subset of (TOP-REAL n);

canceled;

attr A is Bounded means :Def2: :: JORDAN2C:def 2

A is bounded Subset of (Euclid n);

correctness

;

:: deftheorem JORDAN2C:def 1 :

canceled;

:: deftheorem Def2 defines Bounded JORDAN2C:def 2 :

for n being Nat

for A being Subset of (TOP-REAL n) holds

( A is Bounded iff A is bounded Subset of (Euclid n) );

theorem Th16: :: JORDAN2C:16

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

for A, B being Subset of (TOP-REAL n) st B is Bounded & A c= B holds

A is Bounded

proof end;

definition

let n be Nat;

let A, B be Subset of (TOP-REAL n);

pred B is_inside_component_of A means :Def3: :: JORDAN2C:def 3

( B is_a_component_of A ` & B is Bounded );

end;
let A, B be Subset of (TOP-REAL n);

pred B is_inside_component_of A means :Def3: :: JORDAN2C:def 3

( B is_a_component_of A ` & B is Bounded );

:: deftheorem Def3 defines is_inside_component_of JORDAN2C:def 3 :

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 Element of bool the carrier of M;

existence

ex b_{1} being Subset of M st b_{1} is bounded

end;
cluster bounded Element of bool the carrier of M;

existence

ex b

proof end;

theorem Th17: :: JORDAN2C:17

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) ) )

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) ) )

proof end;

definition

let n be Nat;

let A, B be Subset of (TOP-REAL n);

pred B is_outside_component_of A means :Def4: :: JORDAN2C:def 4

( B is_a_component_of A ` & not B is Bounded );

end;
let A, B be Subset of (TOP-REAL n);

pred B is_outside_component_of A means :Def4: :: JORDAN2C:def 4

( B is_a_component_of A ` & not B is Bounded );

:: deftheorem Def4 defines is_outside_component_of JORDAN2C:def 4 :

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 Th18: :: JORDAN2C:18

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) ) )

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) ) )

proof end;

theorem :: JORDAN2C:19

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 `

for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds

B c= A `

proof end;

theorem :: JORDAN2C:20

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 `

for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds

B c= A `

proof end;

definition

let n be Nat;

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 } ;

correctness

coherence

union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } is Subset of (TOP-REAL n);

end;
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 } ;

correctness

coherence

union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } is Subset of (TOP-REAL n);

proof end;

:: deftheorem defines BDD JORDAN2C:def 5 :

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 6

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);

end;
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 } ;

correctness

coherence

union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } is Subset of (TOP-REAL n);

proof end;

:: deftheorem defines UBD JORDAN2C:def 6 :

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 } ;

theorem Th21: :: JORDAN2C:21

proof end;

theorem :: JORDAN2C:22

registration

let n be Element of NAT ;

cluster [#] (TOP-REAL n) -> connected ;

coherence

[#] (TOP-REAL n) is connected by Th21, JORDAN1:9;

end;
cluster [#] (TOP-REAL n) -> connected ;

coherence

[#] (TOP-REAL n) is connected by Th21, JORDAN1:9;

registration

let n be Element of NAT ;

cluster [#] (TOP-REAL n) -> a_component ;

coherence

[#] (TOP-REAL n) is a_component

end;
cluster [#] (TOP-REAL n) -> a_component ;

coherence

[#] (TOP-REAL n) is a_component

proof end;

theorem Th23: :: JORDAN2C:23

theorem Th24: :: JORDAN2C:24

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 `)

for A being Subset of (TOP-REAL n) holds BDD A is a_union_of_components of (TOP-REAL n) | (A `)

proof end;

theorem Th25: :: JORDAN2C:25

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 `)

for A being Subset of (TOP-REAL n) holds UBD A is a_union_of_components of (TOP-REAL n) | (A `)

proof end;

theorem Th26: :: JORDAN2C:26

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

for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds

B c= BDD A

proof end;

theorem Th27: :: JORDAN2C:27

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

for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds

B c= UBD A

proof end;

theorem Th28: :: JORDAN2C:28

proof end;

theorem Th29: :: JORDAN2C:29

proof end;

theorem Th30: :: JORDAN2C:30

proof end;

theorem Th31: :: JORDAN2C:31

proof end;

theorem :: JORDAN2C:32

canceled;

theorem Th33: :: JORDAN2C:33

proof end;

definition

let n be Nat;

func 1* n -> FinSequence of REAL equals :: JORDAN2C:def 7

n |-> 1;

coherence

n |-> 1 is FinSequence of REAL ;

end;
func 1* n -> FinSequence of REAL equals :: JORDAN2C:def 7

n |-> 1;

coherence

n |-> 1 is FinSequence of REAL ;

:: deftheorem defines 1* JORDAN2C:def 7 :

for n being Nat holds 1* n = n |-> 1;

definition

let n be Nat;

:: original: 1*

redefine func 1* n -> Element of REAL n;

coherence

1* n is Element of REAL n

end;
:: original: 1*

redefine func 1* n -> Element of REAL n;

coherence

1* n is Element of REAL n

proof end;

definition

let n be Nat;

func 1.REAL n -> Point of (TOP-REAL n) equals :: JORDAN2C:def 8

1* n;

coherence

1* n is Point of (TOP-REAL n) by EUCLID:25;

end;
func 1.REAL n -> Point of (TOP-REAL n) equals :: JORDAN2C:def 8

1* n;

coherence

1* n is Point of (TOP-REAL n) by EUCLID:25;

:: deftheorem defines 1.REAL JORDAN2C:def 8 :

for n being Nat holds 1.REAL n = 1* n;

theorem :: JORDAN2C:34

proof end;

theorem Th35: :: JORDAN2C:35

proof end;

theorem :: JORDAN2C:36

canceled;

theorem :: JORDAN2C:37

theorem Th38: :: JORDAN2C:38

proof end;

theorem Th39: :: JORDAN2C:39

for n being Element of NAT

for W being Subset of (Euclid n) st n >= 1 & W = REAL n holds

not W is bounded

for W being Subset of (Euclid n) st n >= 1 & W = REAL n holds

not W is bounded

proof end;

theorem Th40: :: JORDAN2C:40

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 )

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 )

proof end;

theorem Th41: :: JORDAN2C:41

proof end;

theorem Th42: :: JORDAN2C:42

proof end;

theorem Th43: :: JORDAN2C:43

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 )

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 )

proof end;

theorem Th44: :: JORDAN2C:44

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 )

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 )

proof end;

theorem Th45: :: JORDAN2C:45

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 )

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 )

proof end;

theorem Th46: :: JORDAN2C:46

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 )

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 )

proof end;

theorem :: JORDAN2C:47

canceled;

theorem Th48: :: JORDAN2C:48

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)) )

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)) )

proof end;

theorem Th49: :: JORDAN2C:49

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 )

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 )

proof end;

theorem Th50: :: JORDAN2C:50

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 )

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 )

proof end;

theorem :: JORDAN2C:51

canceled;

theorem Th52: :: JORDAN2C:52

for f being FinSequence of REAL holds

( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )

( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )

proof end;

theorem Th53: :: JORDAN2C:53

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) ) )

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 Th54: :: JORDAN2C:54

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 )

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 Th55: :: JORDAN2C:55

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 )

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 Th56: :: JORDAN2C:56

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 )

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 )

proof end;

theorem Th57: :: JORDAN2C:57

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 )

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 )

proof end;

theorem Th58: :: JORDAN2C:58

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 } <> {}

for a being Real st n >= 1 holds

{ q where q is Point of (TOP-REAL n) : |.q.| > a } <> {}

proof end;

theorem Th59: :: JORDAN2C:59

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

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

proof end;

theorem Th60: :: JORDAN2C:60

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 } <> {}

for a being Real st n >= 1 holds

(REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {}

proof end;

theorem Th61: :: JORDAN2C:61

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

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

proof end;

theorem Th62: :: JORDAN2C:62

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

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

proof end;

theorem Th63: :: JORDAN2C:63

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

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

proof end;

theorem Th64: :: JORDAN2C:64

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

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

proof end;

theorem :: JORDAN2C:65

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 connected by Th63, JORDAN1:9;

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 connected by Th63, JORDAN1:9;

theorem :: JORDAN2C:66

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 connected by Th64, JORDAN1:9;

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 connected by Th64, JORDAN1:9;

theorem Th67: :: JORDAN2C:67

for W being Subset of (Euclid 1)

for a being Real

for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st

( q = <*r*> & r > a ) } & P = W holds

( P is connected & not W is bounded )

for a being Real

for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st

( q = <*r*> & r > a ) } & P = W holds

( P is connected & not W is bounded )

proof end;

theorem Th68: :: JORDAN2C:68

for W being Subset of (Euclid 1)

for a being Real

for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st

( q = <*r*> & r < - a ) } & P = W holds

( P is connected & not W is bounded )

for a being Real

for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st

( q = <*r*> & r < - a ) } & P = W holds

( P is connected & not W is bounded )

proof end;

theorem Th69: :: JORDAN2C:69

for n being Element of NAT

for W being Subset of (Euclid n)

for a being Real

for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds

( P is connected & not W is bounded )

for W being Subset of (Euclid n)

for a being Real

for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds

( P is connected & not W is bounded )

proof end;

theorem Th70: :: JORDAN2C:70

for n being Element of NAT

for W being Subset of (Euclid n)

for a being Real

for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds

( P is connected & not W is bounded )

for W being Subset of (Euclid n)

for a being Real

for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds

( P is connected & not W is bounded )

proof end;

theorem Th71: :: JORDAN2C:71

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

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

proof end;

theorem Th72: :: JORDAN2C:72

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

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

proof end;

theorem Th73: :: JORDAN2C:73

proof end;

registration

let n be Element of NAT ;

cluster compact -> Bounded Element of bool the carrier of (TOP-REAL n);

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} is compact holds

b_{1} is Bounded
by Th73;

end;
cluster compact -> Bounded Element of bool the carrier of (TOP-REAL n);

coherence

for b

b

theorem Th74: :: JORDAN2C:74

for n being Element of NAT

for A being Subset of (TOP-REAL n) st 1 <= n & A is Bounded holds

A ` <> {}

for A being Subset of (TOP-REAL n) st 1 <= n & A is Bounded holds

A ` <> {}

proof end;

theorem Th75: :: JORDAN2C:75

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 ) )

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 ) )

proof end;

theorem Th76: :: JORDAN2C:76

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

for A being Subset of (TOP-REAL n) st n >= 2 & A is Bounded holds

UBD A is_outside_component_of A

proof end;

theorem Th77: :: JORDAN2C:77

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

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

proof end;

theorem Th78: :: JORDAN2C:78

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

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

proof end;

theorem :: JORDAN2C:79

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 connected by Th77, JORDAN1:9;

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 connected by Th77, JORDAN1:9;

theorem Th80: :: JORDAN2C:80

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) )

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) )

proof end;

theorem Th81: :: JORDAN2C:81

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)) )

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)) )

proof end;

theorem Th82: :: JORDAN2C:82

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 )

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 )

proof end;

theorem Th83: :: JORDAN2C:83

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

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

proof end;

theorem Th84: :: JORDAN2C:84

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

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

proof end;

theorem Th85: :: JORDAN2C:85

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

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

proof end;

theorem Th86: :: JORDAN2C:86

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

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

proof end;

theorem Th87: :: JORDAN2C:87

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 )

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 )

proof end;

theorem Th88: :: JORDAN2C:88

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 )

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 )

proof end;

theorem Th89: :: JORDAN2C:89

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

for B being non empty Subset of (TOP-REAL n) st B is open holds

(TOP-REAL n) | B is locally_connected

proof end;

theorem Th90: :: JORDAN2C:90

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

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

proof end;

theorem Th91: :: JORDAN2C:91

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

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

proof end;

theorem Th92: :: JORDAN2C:92

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 )

( ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) & f is continuous )

proof end;

theorem Th93: :: JORDAN2C:93

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 )

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 )

proof end;

theorem Th94: :: JORDAN2C:94

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

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

proof end;

theorem Th95: :: JORDAN2C:95

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

for r being Real

for q being Point of (TOP-REAL n) st q = <*r*> holds

|.q.| = abs r

proof end;

theorem :: JORDAN2C:96

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

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

proof end;

begin

theorem Th97: :: JORDAN2C:97

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) )

( 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) )

proof end;

theorem Th98: :: JORDAN2C:98

for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds not LeftComp (SpStSeq D) is Bounded

proof end;

theorem Th99: :: JORDAN2C:99

for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D))

proof end;

theorem Th100: :: JORDAN2C:100

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

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 Th101: :: JORDAN2C:101

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)

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)

proof end;

theorem Th102: :: JORDAN2C:102

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 )

( RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) & RightComp (SpStSeq D) is Bounded )

proof end;

theorem Th103: :: JORDAN2C:103

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)) )

( LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) & RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) )

proof end;

theorem Th104: :: JORDAN2C:104

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) )

( 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) )

proof end;

begin

theorem Th105: :: JORDAN2C:105

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 ) )

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 Th106: :: 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 & C2 is a_component ) ) ) )

( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st

( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ) ) )

proof end;

theorem Th107: :: JORDAN2C:107

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

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

proof end;

theorem Th108: :: JORDAN2C:108

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) )

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) )

proof end;

theorem Th109: :: JORDAN2C:109

proof end;

registration

let q1, q2 be Point of (TOP-REAL 2);

cluster LSeg (q1,q2) -> boundary ;

coherence

LSeg (q1,q2) is boundary by Th109;

end;
cluster LSeg (q1,q2) -> boundary ;

coherence

LSeg (q1,q2) is boundary by Th109;

theorem Th110: :: JORDAN2C:110

proof end;

registration

let f be FinSequence of (TOP-REAL 2);

cluster L~ f -> boundary ;

coherence

L~ f is boundary by Th110;

end;
cluster L~ f -> boundary ;

coherence

L~ f is boundary by Th110;

theorem Th111: :: JORDAN2C:111

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 )

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 )

proof end;

theorem :: JORDAN2C:112

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 )

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 )

proof end;

theorem Th113: :: JORDAN2C:113

proof end;

theorem Th114: :: JORDAN2C:114

for n being Element of NAT

for A being Subset of (TOP-REAL n) st A is Bounded holds

BDD A is Bounded

for A being Subset of (TOP-REAL n) st A is Bounded holds

BDD A is Bounded

proof end;

theorem Th115: :: JORDAN2C:115

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

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 Th116: :: 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

BDD A is_inside_component_of A

proof end;

theorem :: JORDAN2C:117

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 )

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 )

proof end;

begin

theorem :: JORDAN2C:118

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

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

proof end;

theorem :: JORDAN2C:119

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

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

proof end;

theorem :: JORDAN2C:120

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

for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `2 < S-bound (L~ f) holds

p in LeftComp f

proof end;

theorem :: JORDAN2C:121

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

for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `2 > N-bound (L~ f) holds

p in LeftComp f

proof end;

theorem :: JORDAN2C:122

proof end;

theorem :: JORDAN2C:123

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

for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds

B is connected

proof end;

theorem Th124: :: JORDAN2C:124

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

for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds

B is connected

proof end;

theorem :: JORDAN2C:125

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

for A, B being Subset of (TOP-REAL n) st B is_a_component_of A ` holds

A misses B

proof end;

theorem :: JORDAN2C:126

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

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

proof end;

theorem :: JORDAN2C:127

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

for A, B, P being Subset of (TOP-REAL n) st P is Bounded & A is_outside_component_of P & B is_outside_component_of P holds

A = B

proof end;

registration

let C be closed Subset of (TOP-REAL 2);

cluster BDD C -> open ;

coherence

BDD C is open

coherence

UBD C is open

end;
cluster BDD C -> open ;

coherence

BDD C is open

proof end;

cluster UBD C -> open ;coherence

UBD C is open

proof end;

registration

let C be compact Subset of (TOP-REAL 2);

cluster UBD C -> connected ;

coherence

UBD C is connected by Th76, Th124;

end;
cluster UBD C -> connected ;

coherence

UBD C is connected by Th76, Th124;

theorem Th128: :: JORDAN2C:128

proof end;

theorem Th129: :: JORDAN2C:129

proof end;

theorem Th130: :: JORDAN2C:130

proof end;

theorem Th131: :: JORDAN2C:131

proof end;

registration

let C be compact Subset of (TOP-REAL 2);

cluster UBD C -> non empty ;

coherence

not UBD C is empty

end;
cluster UBD C -> non empty ;

coherence

not UBD C is empty

proof end;

theorem Th132: :: JORDAN2C:132

proof end;

theorem Th133: :: JORDAN2C:133

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

for WH being connected Subset of (TOP-REAL 2) st not WH is Bounded & WH misses C holds

WH c= UBD C

proof end;

theorem :: JORDAN2C:134

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

for p being Point of (TOP-REAL 2) st west_halfline p misses C holds

west_halfline p c= UBD C

proof end;

theorem :: JORDAN2C:135

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

for p being Point of (TOP-REAL 2) st east_halfline p misses C holds

east_halfline p c= UBD C

proof end;

theorem :: JORDAN2C:136

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

for p being Point of (TOP-REAL 2) st south_halfline p misses C holds

south_halfline p c= UBD C

proof end;

theorem :: JORDAN2C:137

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

for p being Point of (TOP-REAL 2) st north_halfline p misses C holds

north_halfline p c= UBD C

proof end;