begin
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:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
Lm4:
for p being Point of
for C being Simple_closed_curve
for U being Subset of 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:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
theorem
theorem Th29:
theorem Th30:
Lm7:
for T being non empty TopSpace
for a, b being Point of
for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
Lm8:
for T being non empty TopSpace
for a, b, c, d, e being Point of
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
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
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
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:
theorem Th42:
theorem Th43:
theorem Th44:
begin
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
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:
theorem Th51:
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:
theorem
theorem
theorem
theorem
theorem Th57:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
for
P being
Subset of 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
begin
:: 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:
for
x being
Point of 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 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 holds b1 . x = ((x `1 ) `1 ) - ((x `2 ) `1 ) ) & ( for x being Point of 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:
for
x being
Point of 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 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 holds b1 . x = ((x `1 ) `2 ) - ((x `2 ) `2 ) ) & ( for x being Point of 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:
for
x being
Point of holds
it . x = (x `2 ) `1 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of 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 holds b1 . x = (x `2 ) `1 ) & ( for x being Point of holds b2 . x = (x `2 ) `1 ) holds
b1 = b2
func Proj2_2 -> RealMap of
[:(TOP-REAL 2),(TOP-REAL 2):] means :
Def6:
for
x being
Point of holds
it . x = (x `2 ) `2 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of 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 holds b1 . x = (x `2 ) `2 ) & ( for x being Point of 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:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of ;
let r be
positive real number ;
assume A1:
p is
Point of
;
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:
for
x being
Point of ex
y being
Point of 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 ex y being Point of 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 ex y being Point of st
( x = y & b1 . x = HC p,y,o,r ) ) & ( for x being Point of ex y being Point of st
( x = y & b2 . x = HC p,y,o,r ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines DiskProj JORDAN:def 7 :
theorem Th64:
theorem Th65:
definition
let n be non
empty Element of
NAT ;
let o,
p be
Point of ;
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:
for
x being
Point of ex
y being
Point of 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 ex y being Point of 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 ex y being Point of st
( x = y & b1 . x = HC y,p,o,r ) ) & ( for x being Point of ex y being Point of 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
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 ex
y being
Point of st
(
x = y &
b5 . x = HC y,
p,
o,
r ) );
theorem Th66:
theorem Th67:
begin
theorem Th68:
theorem Th69:
Lm12:
for p1, p2, p being Point of
for A being Subset of
for r being non negative real number st A is_an_arc_of p1,p2 & A is Subset of 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
for C being Simple_closed_curve
for A, P, B being Subset of
for U being Subset of
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 holds
( ( x in Cl P implies g . x = f . x ) & ( x in P ` implies g . x = x ) ) ) )
Lm14:
for p being Point of
for C being Simple_closed_curve
for P, B being Subset of
for U, V being Subset of
for A being non empty Subset of 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 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
for U being Subset of 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 : ( ( 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:
theorem Th71:
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 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 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:
theorem Th73:
theorem Th74:
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
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
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
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
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:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
Lm87:
for P being Subset of 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 st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P holds
|[0 ,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem
theorem Th93:
Lm89:
for p being Point of 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
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 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:
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 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 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 st
V is_inside_component_of C holds
V = Ux ) )
theorem Th96:
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 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
theorem
theorem