:: Jordan's Curve Theorem
:: by Artur Korni{\l}owicz
::
:: Received September 15, 2005
:: Copyright (c) 2005 Association of Mizar Users
set T2 = TOP-REAL 2;
Lm1:
for A, B, C, Z being set st A c= Z & B c= Z & C c= Z holds
(A \/ B) \/ C c= Z
Lm2:
for A, B, C, D, Z being set st A c= Z & B c= Z & C c= Z & D c= Z holds
((A \/ B) \/ C) \/ D c= Z
Lm3:
for A, B, C, D, Z being set st A misses Z & B misses Z & C misses Z & D misses Z holds
((A \/ B) \/ C) \/ D misses Z
theorem Th1: :: JORDAN:1
theorem Th2: :: JORDAN:2
theorem Th3: :: JORDAN:3
theorem Th4: :: JORDAN:4
theorem :: JORDAN:5
theorem :: JORDAN:6
theorem :: JORDAN:7
theorem Th8: :: JORDAN:8
theorem :: JORDAN:9
theorem Th10: :: JORDAN:10
theorem Th11: :: JORDAN:11
theorem Th12: :: JORDAN:12
theorem Th13: :: JORDAN:13
theorem Th14: :: JORDAN:14
theorem :: JORDAN:15
Lm4:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C ` )) st p in C holds
{p} misses U
set C0 = Closed-Interval-TSpace 0 ,1;
set C1 = Closed-Interval-TSpace (- 1),1;
set l0 = (#) (- 1),1;
set l1 = (- 1),1 (#) ;
set h1 = L[01] ((#) (- 1),1),((- 1),1 (#) );
Lm5:
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] = [:the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2):]
by BORSUK_1:def 5;
theorem Th16: :: JORDAN:16
theorem Th17: :: JORDAN:17
theorem Th18: :: JORDAN:18
theorem Th19: :: JORDAN:19
theorem Th20: :: JORDAN:20
theorem Th21: :: JORDAN:21
theorem Th22: :: JORDAN:22
theorem Th23: :: JORDAN:23
theorem Th24: :: JORDAN:24
theorem Th25: :: JORDAN:25
theorem Th26: :: JORDAN:26
theorem :: JORDAN:27
theorem :: JORDAN:28
theorem Th29: :: JORDAN:29
theorem Th30: :: JORDAN:30
Lm7:
for T being non empty TopSpace
for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)
theorem Th31: :: JORDAN:31
theorem Th32: :: JORDAN:32
theorem Th33: :: JORDAN:33
theorem :: JORDAN:34
theorem Th35: :: JORDAN:35
theorem :: JORDAN:36
theorem Th37: :: JORDAN:37
theorem :: JORDAN:38
theorem Th39: :: JORDAN:39
theorem Th40: :: JORDAN:40
Lm8:
for T being non empty TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)
Lm9:
for T being non empty arcwise_connected TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e holds rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)
Lm10:
for T being non empty TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected holds
rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
Lm11:
for T being non empty arcwise_connected TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
theorem Th41: :: JORDAN:41
theorem Th42: :: JORDAN:42
theorem Th43: :: JORDAN:43
theorem Th44: :: JORDAN:44
theorem Th45: :: JORDAN:45
theorem Th46: :: JORDAN:46
theorem Th47: :: JORDAN:47
theorem Th48: :: JORDAN:48
theorem Th49: :: JORDAN:49
for
a,
b,
c,
d being
real number holds
(closed_inside_of_rectangle a,b,c,d) /\ (inside_of_rectangle a,b,c,d) = inside_of_rectangle a,
b,
c,
d
theorem Th50: :: JORDAN:50
theorem Th51: :: JORDAN:51
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) = rectangle a,
b,
c,
d
theorem Th52: :: JORDAN:52
theorem :: JORDAN:53
theorem :: JORDAN:54
theorem :: JORDAN:55
theorem :: JORDAN:56
theorem Th57: :: JORDAN:57
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) for
P being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 in closed_inside_of_rectangle a,
b,
c,
d & not
p2 in closed_inside_of_rectangle a,
b,
c,
d &
P is_an_arc_of p1,
p2 holds
Segment P,
p1,
p2,
p1,
(First_Point P,p1,p2,(rectangle a,b,c,d)) c= closed_inside_of_rectangle a,
b,
c,
d
definition
let o be
Point of
(TOP-REAL 2);
func diffX2_1 o -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def1:
:: JORDAN:def 1
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `2 ) `1 ) - (o `1 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2 ) `1 ) - (o `1 )
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2 ) `1 ) - (o `1 ) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2 ) `1 ) - (o `1 ) ) holds
b1 = b2
func diffX2_2 o -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def2:
:: JORDAN:def 2
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `2 ) `2 ) - (o `2 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2 ) `2 ) - (o `2 )
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2 ) `2 ) - (o `2 ) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2 ) `2 ) - (o `2 ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines diffX2_1 JORDAN:def 1 :
:: deftheorem Def2 defines diffX2_2 JORDAN:def 2 :
definition
func diffX1_X2_1 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def3:
:: JORDAN:def 3
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `1 ) `1 ) - ((x `2 ) `1 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1 ) `1 ) - ((x `2 ) `1 )
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1 ) `1 ) - ((x `2 ) `1 ) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1 ) `1 ) - ((x `2 ) `1 ) ) holds
b1 = b2
func diffX1_X2_2 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def4:
:: JORDAN:def 4
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = ((x `1 ) `2 ) - ((x `2 ) `2 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1 ) `2 ) - ((x `2 ) `2 )
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1 ) `2 ) - ((x `2 ) `2 ) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1 ) `2 ) - ((x `2 ) `2 ) ) holds
b1 = b2
func Proj2_1 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def5:
:: JORDAN:def 5
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = (x `2 ) `1 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2 ) `1
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2 ) `1 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2 ) `1 ) holds
b1 = b2
func Proj2_2 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def6:
:: JORDAN:def 6
for
x being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] holds
it . x = (x `2 ) `2 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2 ) `2
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2 ) `2 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2 ) `2 ) holds
b1 = b2
end;
:: deftheorem Def3 defines diffX1_X2_1 JORDAN:def 3 :
:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def 4 :
:: deftheorem Def5 defines Proj2_1 JORDAN:def 5 :
:: deftheorem Def6 defines Proj2_2 JORDAN:def 6 :
theorem Th58: :: JORDAN:58
theorem Th59: :: JORDAN:59
theorem Th60: :: JORDAN:60
theorem Th61: :: JORDAN:61
theorem Th62: :: JORDAN:62
theorem Th63: :: JORDAN:63
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of
(TOP-REAL n);
let r be
positive real number ;
assume A1:
p is
Point of
(Tdisk o,r)
;
set X =
(TOP-REAL n) | ((cl_Ball o,r) \ {p});
func DiskProj o,
r,
p -> Function of
((TOP-REAL n) | ((cl_Ball o,r) \ {p})),
(Tcircle o,r) means :
Def7:
:: JORDAN:def 7
for
x being
Point of
((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
it . x = HC p,
y,
o,
r );
existence
ex b1 being Function of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})),(Tcircle o,r) st
for x being Point of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC p,y,o,r )
uniqueness
for b1, b2 being Function of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})),(Tcircle o,r) st ( for x being Point of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC p,y,o,r ) ) & ( for x being Point of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b2 . x = HC p,y,o,r ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines DiskProj JORDAN:def 7 :
for
n being non
empty Element of
NAT for
o,
p being
Point of
(TOP-REAL n) for
r being
positive real number st
p is
Point of
(Tdisk o,r) holds
for
b5 being
Function of
((TOP-REAL n) | ((cl_Ball o,r) \ {p})),
(Tcircle o,r) holds
(
b5 = DiskProj o,
r,
p iff for
x being
Point of
((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
b5 . x = HC p,
y,
o,
r ) );
theorem Th64: :: JORDAN:64
theorem Th65: :: JORDAN:65
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of
(TOP-REAL n);
let r be
positive real number ;
assume A1:
p in Ball o,
r
;
set X =
Tcircle o,
r;
func RotateCircle o,
r,
p -> Function of
(Tcircle o,r),
(Tcircle o,r) means :
Def8:
:: JORDAN:def 8
for
x being
Point of
(Tcircle o,r) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
it . x = HC y,
p,
o,
r );
existence
ex b1 being Function of (Tcircle o,r),(Tcircle o,r) st
for x being Point of (Tcircle o,r) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC y,p,o,r )
uniqueness
for b1, b2 being Function of (Tcircle o,r),(Tcircle o,r) st ( for x being Point of (Tcircle o,r) ex y being Point of (TOP-REAL n) st
( x = y & b1 . x = HC y,p,o,r ) ) & ( for x being Point of (Tcircle o,r) ex y being Point of (TOP-REAL n) st
( x = y & b2 . x = HC y,p,o,r ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :
for
n being non
empty Element of
NAT for
o,
p being
Point of
(TOP-REAL n) for
r being
positive real number st
p in Ball o,
r holds
for
b5 being
Function of
(Tcircle o,r),
(Tcircle o,r) holds
(
b5 = RotateCircle o,
r,
p iff for
x being
Point of
(Tcircle o,r) ex
y being
Point of
(TOP-REAL n) st
(
x = y &
b5 . x = HC y,
p,
o,
r ) );
theorem Th66: :: JORDAN:66
theorem Th67: :: JORDAN:67
theorem Th68: :: JORDAN:68
theorem Th69: :: JORDAN:69
Lm12:
for p1, p2, p being Point of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2)
for r being non negative real number st A is_an_arc_of p1,p2 & A is Subset of (Tdisk p,r) holds
ex f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )
Lm13:
for p1, p2, p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for A, P, B being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` ))
for r being positive real number st A is_an_arc_of p1,p2 & A c= C & C c= Ball p,r & p in U & (Cl P) /\ (P ` ) c= A & P c= Ball p,r holds
for f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & B = (cl_Ball p,r) \ {p} holds
ex g being Function of (Tdisk p,r),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies g . x = f . x ) & ( x in P ` implies g . x = x ) ) ) )
Lm14:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for P, B being Subset of (TOP-REAL 2)
for U, V being Subset of ((TOP-REAL 2) | (C ` ))
for A being non empty Subset of (TOP-REAL 2) st U <> V holds
for r being positive real number st A c= C & C c= Ball p,r & p in V & (Cl P) /\ (P ` ) c= A & Ball p,r meets P holds
for f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & B = (cl_Ball p,r) \ {p} holds
ex g being Function of (Tdisk p,r),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies g . x = x ) & ( x in P ` implies g . x = f . x ) ) ) )
Lm15:
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` )) st not BDD C is empty & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P
set rp = 1;
set rl = - 1;
set rg = 3;
set rd = - 3;
set a = |[(- 1),0 ]|;
set b = |[1,0 ]|;
set c = |[0 ,3]|;
set d = |[0 ,(- 3)]|;
set lg = |[(- 1),3]|;
set pg = |[1,3]|;
set ld = |[(- 1),(- 3)]|;
set pd = |[1,(- 3)]|;
set R = closed_inside_of_rectangle (- 1),1,(- 3),3;
set dR = rectangle (- 1),1,(- 3),3;
set TR = Trectangle (- 1),1,(- 3),3;
Lm16:
|[(- 1),0 ]| `1 = - 1
by EUCLID:56;
Lm17:
|[1,0 ]| `1 = 1
by EUCLID:56;
Lm18:
|[(- 1),0 ]| `2 = 0
by EUCLID:56;
Lm19:
|[1,0 ]| `2 = 0
by EUCLID:56;
Lm20:
|[0 ,3]| `1 = 0
by EUCLID:56;
Lm21:
|[0 ,3]| `2 = 3
by EUCLID:56;
Lm22:
|[0 ,(- 3)]| `1 = 0
by EUCLID:56;
Lm23:
|[0 ,(- 3)]| `2 = - 3
by EUCLID:56;
Lm24:
|[(- 1),3]| `1 = - 1
by EUCLID:56;
Lm25:
|[(- 1),3]| `2 = 3
by EUCLID:56;
Lm26:
|[(- 1),(- 3)]| `1 = - 1
by EUCLID:56;
Lm27:
|[(- 1),(- 3)]| `2 = - 3
by EUCLID:56;
Lm28:
|[1,3]| `1 = 1
by EUCLID:56;
Lm29:
|[1,3]| `2 = 3
by EUCLID:56;
Lm30:
|[1,(- 3)]| `1 = 1
by EUCLID:56;
Lm31:
|[1,(- 3)]| `2 = - 3
by EUCLID:56;
Lm32:
|[(- 1),(- 3)]| = |[(|[(- 1),(- 3)]| `1 ),(|[(- 1),(- 3)]| `2 )]|
by EUCLID:57;
Lm33:
|[(- 1),3]| = |[(|[(- 1),3]| `1 ),(|[(- 1),3]| `2 )]|
by EUCLID:57;
Lm34:
|[1,(- 3)]| = |[(|[1,(- 3)]| `1 ),(|[1,(- 3)]| `2 )]|
by EUCLID:57;
Lm35:
|[1,3]| = |[(|[1,3]| `1 ),(|[1,3]| `2 )]|
by EUCLID:57;
Lm36:
rectangle (- 1),1,(- 3),3 = ((LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|)) \/ ((LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|))
by SPPOL_2:def 3;
Lm37:
LSeg |[(- 1),(- 3)]|,|[(- 1),3]| c= (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|)
by XBOOLE_1:7;
(LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) c= rectangle (- 1),1,(- 3),3
by Lm36, XBOOLE_1:7;
then Lm38:
LSeg |[(- 1),(- 3)]|,|[(- 1),3]| c= rectangle (- 1),1,(- 3),3
by Lm37, XBOOLE_1:1;
Lm39:
LSeg |[(- 1),3]|,|[1,3]| c= (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|)
by XBOOLE_1:7;
(LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) c= rectangle (- 1),1,(- 3),3
by Lm36, XBOOLE_1:7;
then Lm40:
LSeg |[(- 1),3]|,|[1,3]| c= rectangle (- 1),1,(- 3),3
by Lm39, XBOOLE_1:1;
Lm41:
LSeg |[1,3]|,|[1,(- 3)]| c= (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|)
by XBOOLE_1:7;
(LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) c= rectangle (- 1),1,(- 3),3
by Lm36, XBOOLE_1:7;
then Lm42:
LSeg |[1,3]|,|[1,(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm41, XBOOLE_1:1;
Lm43:
LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| c= (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|)
by XBOOLE_1:7;
(LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) c= rectangle (- 1),1,(- 3),3
by Lm36, XBOOLE_1:7;
then Lm44:
LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm43, XBOOLE_1:1;
Lm45:
LSeg |[(- 1),(- 3)]|,|[(- 1),3]| is vertical
by Lm24, Lm26, SPPOL_1:37;
Lm46:
LSeg |[1,(- 3)]|,|[1,3]| is vertical
by Lm28, Lm30, SPPOL_1:37;
Lm47:
LSeg |[(- 1),0 ]|,|[(- 1),3]| is vertical
by Lm16, Lm24, SPPOL_1:37;
Lm48:
LSeg |[(- 1),0 ]|,|[(- 1),(- 3)]| is vertical
by Lm16, Lm26, SPPOL_1:37;
Lm49:
LSeg |[1,0 ]|,|[1,3]| is vertical
by Lm17, Lm28, SPPOL_1:37;
Lm50:
LSeg |[1,0 ]|,|[1,(- 3)]| is vertical
by Lm17, Lm30, SPPOL_1:37;
Lm51:
LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| is horizontal
by Lm23, Lm27, SPPOL_1:36;
Lm52:
LSeg |[1,(- 3)]|,|[0 ,(- 3)]| is horizontal
by Lm23, Lm31, SPPOL_1:36;
Lm53:
LSeg |[(- 1),3]|,|[0 ,3]| is horizontal
by Lm21, Lm25, SPPOL_1:36;
Lm54:
LSeg |[1,3]|,|[0 ,3]| is horizontal
by Lm21, Lm29, SPPOL_1:36;
Lm55:
LSeg |[(- 1),3]|,|[1,3]| is horizontal
by Lm25, Lm29, SPPOL_1:36;
Lm56:
LSeg |[(- 1),(- 3)]|,|[1,(- 3)]| is horizontal
by Lm27, Lm31, SPPOL_1:36;
Lm57:
LSeg |[(- 1),0 ]|,|[(- 1),3]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lm16, Lm18, Lm25, Lm26, Lm27, Lm45, Lm47, GOBOARD7:65;
Lm58:
LSeg |[(- 1),0 ]|,|[(- 1),(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lm18, Lm25, Lm26, Lm27, Lm45, Lm48, GOBOARD7:65;
Lm59:
LSeg |[1,0 ]|,|[1,3]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lm17, Lm19, Lm29, Lm30, Lm31, Lm46, Lm49, GOBOARD7:65;
Lm60:
LSeg |[1,0 ]|,|[1,(- 3)]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lm19, Lm29, Lm30, Lm31, Lm46, Lm50, GOBOARD7:65;
Lm61:
rectangle (- 1),1,(- 3),3 = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & p `2 <= 3 & p `2 >= - 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = - 3 ) or ( p `1 = 1 & p `2 <= 3 & p `2 >= - 3 ) ) }
by SPPOL_2:58;
then Lm62:
|[0 ,3]| in rectangle (- 1),1,(- 3),3
by Lm20, Lm21;
Lm63:
|[0 ,(- 3)]| in rectangle (- 1),1,(- 3),3
by Lm22, Lm23, Lm61;
Lm64:
(2 + 1) ^2 = (4 + 4) + 1
;
then Lm65:
sqrt 9 = 3
by SQUARE_1:def 4;
Lm66: dist |[(- 1),0 ]|,|[1,0 ]| =
sqrt ((((|[(- 1),0 ]| `1 ) - (|[1,0 ]| `1 )) ^2 ) + (((|[(- 1),0 ]| `2 ) - (|[1,0 ]| `2 )) ^2 ))
by TOPREAL6:101
.=
- (- 2)
by Lm16, Lm17, Lm18, Lm19, SQUARE_1:90
;
theorem Th70: :: JORDAN:70
theorem Th71: :: JORDAN:71
Lm67:
rectangle (- 1),1,(- 3),3 c= closed_inside_of_rectangle (- 1),1,(- 3),3
by Th45;
Lm68:
|[(- 1),3]| `2 = |[(- 1),3]| `2
;
Lm69:
|[(- 1),3]| `1 <= |[0 ,3]| `1
by Lm24, EUCLID:56;
|[0 ,3]| `1 <= |[1,3]| `1
by Lm28, EUCLID:56;
then
LSeg |[(- 1),3]|,|[0 ,3]| c= LSeg |[(- 1),3]|,|[1,3]|
by Lm53, Lm55, Lm68, Lm69, GOBOARD7:66;
then Lm70:
LSeg |[(- 1),3]|,|[0 ,3]| c= rectangle (- 1),1,(- 3),3
by Lm40, XBOOLE_1:1;
LSeg |[1,3]|,|[0 ,3]| c= LSeg |[(- 1),3]|,|[1,3]|
by Lm20, Lm21, Lm24, Lm25, Lm28, Lm54, Lm55, GOBOARD7:66;
then Lm71:
LSeg |[1,3]|,|[0 ,3]| c= rectangle (- 1),1,(- 3),3
by Lm40, XBOOLE_1:1;
Lm72:
|[(- 1),(- 3)]| `2 = |[(- 1),(- 3)]| `2
;
Lm73:
|[(- 1),(- 3)]| `1 <= |[0 ,(- 3)]| `1
by Lm26, EUCLID:56;
|[0 ,(- 3)]| `1 <= |[1,(- 3)]| `1
by Lm30, EUCLID:56;
then
LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
by Lm51, Lm56, Lm72, Lm73, GOBOARD7:66;
then Lm74:
LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm44, XBOOLE_1:1;
LSeg |[1,(- 3)]|,|[0 ,(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
by Lm22, Lm23, Lm26, Lm27, Lm30, Lm52, Lm56, GOBOARD7:66;
then Lm75:
LSeg |[1,(- 3)]|,|[0 ,(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm44, XBOOLE_1:1;
Lm76:
for p being Point of (TOP-REAL 2) st 0 <= p `2 & p in rectangle (- 1),1,(- 3),3 & not p in LSeg |[(- 1),0 ]|,|[(- 1),3]| & not p in LSeg |[(- 1),3]|,|[0 ,3]| & not p in LSeg |[0 ,3]|,|[1,3]| holds
p in LSeg |[1,3]|,|[1,0 ]|
Lm77:
for p being Point of (TOP-REAL 2) st p `2 <= 0 & p in rectangle (- 1),1,(- 3),3 & not p in LSeg |[(- 1),0 ]|,|[(- 1),(- 3)]| & not p in LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| & not p in LSeg |[0 ,(- 3)]|,|[1,(- 3)]| holds
p in LSeg |[1,(- 3)]|,|[1,0 ]|
theorem Th72: :: JORDAN:72
theorem Th73: :: JORDAN:73
theorem Th74: :: JORDAN:74
Lm78:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
LSeg |[(- 1),3]|,|[0 ,3]| misses C
Lm79:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
LSeg |[1,3]|,|[0 ,3]| misses C
Lm80:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| misses C
Lm81:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
LSeg |[1,(- 3)]|,|[0 ,(- 3)]| misses C
Lm82:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C & p in C ` & p in LSeg |[(- 1),0 ]|,|[(- 1),3]| holds
LSeg p,|[(- 1),3]| misses C
Lm83:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C & p in C ` & p in LSeg |[1,0 ]|,|[1,3]| holds
LSeg p,|[1,3]| misses C
Lm84:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C & p in C ` & p in LSeg |[(- 1),0 ]|,|[(- 1),(- 3)]| holds
LSeg p,|[(- 1),(- 3)]| misses C
Lm85:
for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C & p in C ` & p in LSeg |[1,0 ]|,|[1,(- 3)]| holds
LSeg p,|[1,(- 3)]| misses C
Lm86:
for r being real number holds
( not |[0 ,r]| in rectangle (- 1),1,(- 3),3 or r = - 3 or r = 3 )
theorem Th75: :: JORDAN:75
theorem Th76: :: JORDAN:76
theorem Th77: :: JORDAN:77
theorem Th78: :: JORDAN:78
theorem Th79: :: JORDAN:79
theorem Th80: :: JORDAN:80
Lm87:
for P being Subset of (TOP-REAL 2) st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P holds
|[0 ,3]| `1 = ((W-bound P) + (E-bound P)) / 2
Lm88:
for P being Subset of (TOP-REAL 2) st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P holds
|[0 ,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2
theorem Th81: :: JORDAN:81
theorem Th82: :: JORDAN:82
theorem Th83: :: JORDAN:83
theorem Th84: :: JORDAN:84
theorem Th85: :: JORDAN:85
theorem Th86: :: JORDAN:86
theorem Th87: :: JORDAN:87
theorem Th88: :: JORDAN:88
theorem Th89: :: JORDAN:89
theorem Th90: :: JORDAN:90
theorem Th91: :: JORDAN:91
theorem :: JORDAN:92
theorem Th93: :: JORDAN:93
Lm89:
for p being Point of (TOP-REAL 2) st p in closed_inside_of_rectangle (- 1),1,(- 3),3 holds
closed_inside_of_rectangle (- 1),1,(- 3),3 c= Ball p,10
theorem :: JORDAN:94
Lm90:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
ex Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Jc is_an_arc_of |[(- 1),0 ]|,|[1,0 ]| & Jd is_an_arc_of |[(- 1),0 ]|,|[1,0 ]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0 ]|,|[1,0 ]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc )
theorem Th95: :: JORDAN:95
for
C being
Simple_closed_curve st
|[(- 1),0 ]|,
|[1,0 ]| realize-max-dist-in C holds
for
Jc,
Jd being
compact with_the_max_arc Subset of
(TOP-REAL 2) st
Jc is_an_arc_of |[(- 1),0 ]|,
|[1,0 ]| &
Jd is_an_arc_of |[(- 1),0 ]|,
|[1,0 ]| &
C = Jc \/ Jd &
Jc /\ Jd = {|[(- 1),0 ]|,|[1,0 ]|} &
UMP C in Jc &
LMP C in Jd &
W-bound C = W-bound Jc &
E-bound C = E-bound Jc holds
for
Ux being
Subset of
(TOP-REAL 2) st
Ux = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) holds
(
Ux is_inside_component_of C & ( for
V being
Subset of
(TOP-REAL 2) st
V is_inside_component_of C holds
V = Ux ) )
theorem Th96: :: JORDAN:96
for
C being
Simple_closed_curve st
|[(- 1),0 ]|,
|[1,0 ]| realize-max-dist-in C holds
for
Jc,
Jd being
compact with_the_max_arc Subset of
(TOP-REAL 2) st
Jc is_an_arc_of |[(- 1),0 ]|,
|[1,0 ]| &
Jd is_an_arc_of |[(- 1),0 ]|,
|[1,0 ]| &
C = Jc \/ Jd &
Jc /\ Jd = {|[(- 1),0 ]|,|[1,0 ]|} &
UMP C in Jc &
LMP C in Jd &
W-bound C = W-bound Jc &
E-bound C = E-bound Jc holds
BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` ))
Lm91:
for C being Simple_closed_curve st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C holds
C is Jordan
Lm92:
for C being Simple_closed_curve holds C is Jordan
theorem :: JORDAN:97
theorem :: JORDAN:98
theorem :: JORDAN:99