:: JORDAN22 semantic presentation
begin
Lm1: for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
proof
let r be real number ; ::_thesis: for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
let X be Subset of (TOP-REAL 2); ::_thesis: ( r in proj2 .: X implies ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) )
assume r in proj2 .: X ; ::_thesis: ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
then ex x being set st
( x in the carrier of (TOP-REAL 2) & x in X & proj2 . x = r ) by FUNCT_2:64;
hence ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) ; ::_thesis: verum
end;
theorem Th1: :: JORDAN22:1
for C being Simple_closed_curve
for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))
let i be Element of NAT ; ::_thesis: (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))
A1: Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) by JORDAN6:61;
A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46;
(Upper_Appr C) . i = Upper_Arc (L~ (Cage (C,i))) by JORDAN19:def_1;
hence (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by A1, A2, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th2: :: JORDAN22:2
for C being Simple_closed_curve
for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0)))
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0)))
let i be Element of NAT ; ::_thesis: (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0)))
A1: Lower_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) by JORDAN6:61;
A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46;
(Lower_Appr C) . i = Lower_Arc (L~ (Cage (C,i))) by JORDAN19:def_2;
hence (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) by A1, A2, XBOOLE_1:1; ::_thesis: verum
end;
registration
let C be Simple_closed_curve;
cluster Upper_Arc C -> connected ;
coherence
Upper_Arc C is connected
proof
Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def_8;
hence Upper_Arc C is connected by JORDAN6:10; ::_thesis: verum
end;
cluster Lower_Arc C -> connected ;
coherence
Lower_Arc C is connected
proof
Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def_9;
hence Lower_Arc C is connected by JORDAN6:10; ::_thesis: verum
end;
end;
theorem :: JORDAN22:3
for C being Simple_closed_curve
for i being Element of NAT holds
( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds
( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )
let i be Element of NAT ; ::_thesis: ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )
Upper_Arc (L~ (Cage (C,i))) is compact ;
hence (Upper_Appr C) . i is compact by JORDAN19:def_1; ::_thesis: (Upper_Appr C) . i is connected
Upper_Arc (L~ (Cage (C,i))) is connected ;
hence (Upper_Appr C) . i is connected by JORDAN19:def_1; ::_thesis: verum
end;
theorem :: JORDAN22:4
for C being Simple_closed_curve
for i being Element of NAT holds
( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds
( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
let i be Element of NAT ; ::_thesis: ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
Lower_Arc (L~ (Cage (C,i))) is compact ;
hence (Lower_Appr C) . i is compact by JORDAN19:def_2; ::_thesis: (Lower_Appr C) . i is connected
Lower_Arc (L~ (Cage (C,i))) is connected ;
hence (Lower_Appr C) . i is connected by JORDAN19:def_2; ::_thesis: verum
end;
registration
let C be Simple_closed_curve;
cluster North_Arc C -> compact ;
coherence
North_Arc C is compact
proof
for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th1;
then Lim_inf (Upper_Appr C) is compact by KURATO_2:26;
hence North_Arc C is compact by JORDAN19:def_3; ::_thesis: verum
end;
cluster South_Arc C -> compact ;
coherence
South_Arc C is compact
proof
for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th2;
then Lim_inf (Lower_Appr C) is compact by KURATO_2:26;
hence South_Arc C is compact by JORDAN19:def_4; ::_thesis: verum
end;
end;
Lm2: dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def_1;
Lm3: for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds 1 <= len (Gauge (R,n))
proof
let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds 1 <= len (Gauge (R,n))
let n be Element of NAT ; ::_thesis: 1 <= len (Gauge (R,n))
4 <= len (Gauge (R,n)) by JORDAN8:10;
hence 1 <= len (Gauge (R,n)) by XXREAL_0:2; ::_thesis: verum
end;
theorem Th5: :: JORDAN22:5
for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds [1,1] in Indices (Gauge (R,n))
proof
let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [1,1] in Indices (Gauge (R,n))
let n be Element of NAT ; ::_thesis: [1,1] in Indices (Gauge (R,n))
A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1;
1 <= len (Gauge (R,n)) by Lm3;
hence [1,1] in Indices (Gauge (R,n)) by A1, MATRIX_1:36; ::_thesis: verum
end;
theorem Th6: :: JORDAN22:6
for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds [1,2] in Indices (Gauge (R,n))
proof
let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [1,2] in Indices (Gauge (R,n))
let n be Element of NAT ; ::_thesis: [1,2] in Indices (Gauge (R,n))
A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1;
A2: 4 <= len (Gauge (R,n)) by JORDAN8:10;
then A3: 2 <= len (Gauge (R,n)) by XXREAL_0:2;
1 <= len (Gauge (R,n)) by A2, XXREAL_0:2;
hence [1,2] in Indices (Gauge (R,n)) by A1, A3, MATRIX_1:36; ::_thesis: verum
end;
theorem Th7: :: JORDAN22:7
for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds [2,1] in Indices (Gauge (R,n))
proof
let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [2,1] in Indices (Gauge (R,n))
let n be Element of NAT ; ::_thesis: [2,1] in Indices (Gauge (R,n))
A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1;
A2: 4 <= len (Gauge (R,n)) by JORDAN8:10;
then A3: 2 <= len (Gauge (R,n)) by XXREAL_0:2;
1 <= len (Gauge (R,n)) by A2, XXREAL_0:2;
hence [2,1] in Indices (Gauge (R,n)) by A1, A3, MATRIX_1:36; ::_thesis: verum
end;
theorem Th8: :: JORDAN22:8
for i, m, k, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds
dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))
proof
let i, m, k, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds
dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) implies dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) )
assume that
A1: m > k and
A2: [i,j] in Indices (Gauge (C,k)) and
A3: [i,(j + 1)] in Indices (Gauge (C,k)) ; ::_thesis: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))
A4: len (Gauge (C,k)) < len (Gauge (C,m)) by A1, JORDAN1A:29;
A5: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def_1;
A6: len (Gauge (C,k)) = width (Gauge (C,k)) by JORDAN8:def_1;
j <= width (Gauge (C,k)) by A2, MATRIX_1:38;
then A7: j <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2;
A8: (N-bound C) - (S-bound C) > 0 by SPRECT_1:32, XREAL_1:50;
i <= len (Gauge (C,k)) by A2, MATRIX_1:38;
then A9: i <= len (Gauge (C,m)) by A4, XXREAL_0:2;
j + 1 <= width (Gauge (C,k)) by A3, MATRIX_1:38;
then A10: j + 1 <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2;
A11: 1 <= i by A2, MATRIX_1:38;
1 <= j + 1 by NAT_1:11;
then A12: [i,(j + 1)] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_1:36;
1 <= j by A2, MATRIX_1:38;
then [i,j] in Indices (Gauge (C,m)) by A11, A9, A7, MATRIX_1:36;
then A13: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by A12, GOBRD14:9;
A14: 2 |^ k > 0 by NEWTON:83;
dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A2, A3, GOBRD14:9;
hence dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) by A1, A13, A14, A8, PEPIN:66, XREAL_1:76; ::_thesis: verum
end;
theorem Th9: :: JORDAN22:9
for m, k being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2)))
proof
let m, k be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2)))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k implies dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) )
assume A1: m > k ; ::_thesis: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2)))
[1,(1 + 1)] in Indices (Gauge (C,k)) by Th6;
hence dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A1, Th5, Th8; ::_thesis: verum
end;
theorem Th10: :: JORDAN22:10
for i, m, k, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds
dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j)))
proof
let i, m, k, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds
dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j)))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) implies dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) )
assume that
A1: m > k and
A2: [i,j] in Indices (Gauge (C,k)) and
A3: [(i + 1),j] in Indices (Gauge (C,k)) ; ::_thesis: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j)))
A4: len (Gauge (C,k)) < len (Gauge (C,m)) by A1, JORDAN1A:29;
i <= len (Gauge (C,k)) by A2, MATRIX_1:38;
then A5: i <= len (Gauge (C,m)) by A4, XXREAL_0:2;
A6: (E-bound C) - (W-bound C) > 0 by SPRECT_1:31, XREAL_1:50;
A7: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def_1;
A8: len (Gauge (C,k)) = width (Gauge (C,k)) by JORDAN8:def_1;
j <= width (Gauge (C,k)) by A2, MATRIX_1:38;
then A9: j <= width (Gauge (C,m)) by A8, A7, A4, XXREAL_0:2;
i + 1 <= len (Gauge (C,k)) by A3, MATRIX_1:38;
then A10: i + 1 <= len (Gauge (C,m)) by A4, XXREAL_0:2;
A11: 1 <= j by A2, MATRIX_1:38;
1 <= i + 1 by NAT_1:11;
then A12: [(i + 1),j] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_1:36;
1 <= i by A2, MATRIX_1:38;
then [i,j] in Indices (Gauge (C,m)) by A11, A5, A9, MATRIX_1:36;
then A13: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by A12, GOBRD14:10;
A14: 2 |^ k > 0 by NEWTON:83;
dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A2, A3, GOBRD14:10;
hence dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) by A1, A13, A14, A6, PEPIN:66, XREAL_1:76; ::_thesis: verum
end;
theorem Th11: :: JORDAN22:11
for m, k being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))
proof
let m, k be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k implies dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) )
assume A1: m > k ; ::_thesis: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))
[(1 + 1),1] in Indices (Gauge (C,k)) by Th7;
hence dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A1, Th5, Th10; ::_thesis: verum
end;
theorem :: JORDAN22:12
for C being Simple_closed_curve
for i being Element of NAT
for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT
for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
let i be Element of NAT ; ::_thesis: for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
let r, t be real number ; ::_thesis: ( r > 0 & t > 0 implies ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) )
assume that
A1: r > 0 and
A2: t > 0 ; ::_thesis: ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
consider n being Element of NAT such that
1 < n and
A3: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r and
A4: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t by A1, A2, GOBRD14:11;
percases ( i < n or i >= n ) ;
supposeA5: i < n ; ::_thesis: ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
take n ; ::_thesis: ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
thus ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) by A3, A4, A5; ::_thesis: verum
end;
supposeA6: i >= n ; ::_thesis: ex n being Element of NAT st
( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
take i + 1 ; ::_thesis: ( i < i + 1 & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t )
A7: ( i > n or i = n ) by A6, XXREAL_0:1;
then A8: dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) <= dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) by Th11;
A9: dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) <= dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) by A7, Th9;
thus A10: i < i + 1 by NAT_1:13; ::_thesis: ( dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t )
then dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) by Th9;
then A11: dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) by A9, XXREAL_0:2;
dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) by A10, Th11;
then dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) by A8, XXREAL_0:2;
hence ( dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t ) by A3, A4, A11, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem Th13: :: JORDAN22:13
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
let n be Element of NAT ; ::_thesis: ( 0 < n implies upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) )
set f = Cage (C,n);
set G = Gauge (C,n);
set c = Center (Gauge (C,n));
set Y = proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)));
set X = proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))));
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A2: 1 <= len (Gauge (C,n)) by Lm3;
assume 0 < n ; ::_thesis: upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
then A3: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, JORDAN1G:35
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33 ;
then A4: (Gauge (C,n)) * ((Center (Gauge (C,n))),1) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) ;
A5: proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is bounded_above by JORDAN21:13;
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31;
then LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63;
then A6: not (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) is empty by XBOOLE_0:def_7;
then A7: not proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is empty by Lm2, RELAT_1:119;
A8: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
1 <= Center (Gauge (C,n)) by JORDAN1B:11;
then A9: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `1 by A1, A2, A8, GOBOARD5:2;
then (Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A3;
then A10: ((L~ (Cage (C,n))) /\ (L~ (Cage (C,n)))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) c= (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) by A4, JORDAN1A:13, XBOOLE_1:26;
then A11: proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) c= proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) by RELAT_1:123;
then A12: for r being real number st r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) holds
r <= upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A5, SEQ_4:def_1;
A13: not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is empty by A11, A6, Lm2, RELAT_1:119, XBOOLE_1:3;
A14: for s being real number st 0 < s holds
ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
then consider r being real number such that
A15: r in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) and
A16: (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r by A5, A13, SEQ_4:def_1;
take r ; ::_thesis: ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
consider x being Point of (TOP-REAL 2) such that
A17: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) and
A18: proj2 . x = r by A15, Lm1;
A19: x in L~ (Cage (C,n)) by A17, XBOOLE_0:def_4;
x in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A17, XBOOLE_0:def_4;
then A20: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = x `1 by A3, JORDAN6:31;
A21: GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= x `2 by A8, A19, JORDAN1B:11, JORDAN5D:33;
x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A1, A8, A19, A21, JORDAN1B:11, JORDAN5D:34;
then x in LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) by A9, A20, A22, GOBOARD7:7;
then x in (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) by A19, XBOOLE_0:def_4;
hence r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) by A18, FUNCT_2:35; ::_thesis: (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r
thus (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r by A16; ::_thesis: verum
end;
proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is bounded_above by A10, A5, RELAT_1:123, XXREAL_2:43;
hence upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A7, A12, A14, SEQ_4:def_1; ::_thesis: verum
end;
theorem Th14: :: JORDAN22:14
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
let n be Element of NAT ; ::_thesis: ( 0 < n implies lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) )
set f = Cage (C,n);
set G = Gauge (C,n);
set c = Center (Gauge (C,n));
set Y = proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)));
set X = proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))));
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A2: 1 <= len (Gauge (C,n)) by Lm3;
assume 0 < n ; ::_thesis: lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
then A3: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, JORDAN1G:35
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33 ;
then A4: (Gauge (C,n)) * ((Center (Gauge (C,n))),1) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) ;
A5: proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is bounded_below by JORDAN21:13;
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31;
then LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63;
then A6: not (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) is empty by XBOOLE_0:def_7;
then A7: not proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is empty by Lm2, RELAT_1:119;
A8: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
1 <= Center (Gauge (C,n)) by JORDAN1B:11;
then A9: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `1 by A1, A2, A8, GOBOARD5:2;
then (Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A3;
then A10: ((L~ (Cage (C,n))) /\ (L~ (Cage (C,n)))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) c= (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) by A4, JORDAN1A:13, XBOOLE_1:26;
then A11: proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) c= proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) by RELAT_1:123;
then A12: for r being real number st r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) holds
lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) <= r by A5, SEQ_4:def_2;
A13: not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is empty by A11, A6, Lm2, RELAT_1:119, XBOOLE_1:3;
A14: for s being real number st 0 < s holds
ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s )
then consider r being real number such that
A15: r in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) and
A16: r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s by A5, A13, SEQ_4:def_2;
take r ; ::_thesis: ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s )
consider x being Point of (TOP-REAL 2) such that
A17: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) and
A18: proj2 . x = r by A15, Lm1;
A19: x in L~ (Cage (C,n)) by A17, XBOOLE_0:def_4;
x in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A17, XBOOLE_0:def_4;
then A20: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = x `1 by A3, JORDAN6:31;
A21: GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= x `2 by A8, A19, JORDAN1B:11, JORDAN5D:33;
x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A1, A8, A19, A21, JORDAN1B:11, JORDAN5D:34;
then x in LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) by A9, A20, A22, GOBOARD7:7;
then x in (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) by A19, XBOOLE_0:def_4;
hence r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) by A18, FUNCT_2:35; ::_thesis: r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s
thus r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s by A16; ::_thesis: verum
end;
proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is bounded_below by A10, A5, RELAT_1:123, XXREAL_2:44;
hence lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A7, A12, A14, SEQ_4:def_2; ::_thesis: verum
end;
theorem :: JORDAN22:15
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13;
theorem :: JORDAN22:16
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14;
theorem Th17: :: JORDAN22:17
for C being Simple_closed_curve
for n being Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2
let n be Element of NAT ; ::_thesis: (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2
set p = UMP (L~ (Cage (C,n)));
set u = UMP C;
set w = ((W-bound C) + (E-bound C)) / 2;
A1: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A2: UMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:30;
A3: UMP C = |[((UMP C) `1),((UMP C) `2)]| by EUCLID:53;
A4: UMP (L~ (Cage (C,n))) = |[((UMP (L~ (Cage (C,n)))) `1),((UMP (L~ (Cage (C,n)))) `2)]| by EUCLID:53;
A5: C misses L~ (Cage (C,n)) by JORDAN10:5;
A6: UMP C in C by JORDAN21:30;
A7: ((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33;
then A8: (UMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
assume A9: not (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
percases ( (UMP C) `2 = (UMP (L~ (Cage (C,n)))) `2 or (UMP C) `2 > (UMP (L~ (Cage (C,n)))) `2 ) by A9, XXREAL_0:1;
suppose (UMP C) `2 = (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
hence contradiction by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0:3; ::_thesis: verum
end;
supposeA10: (UMP C) `2 > (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
A11: ( not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above ) by A7, JORDAN21:12, JORDAN21:13;
A12: (UMP (L~ (Cage (C,n)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) by A7, EUCLID:52;
A13: (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} misses L~ (Cage (C,n))
proof
assume (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} meets L~ (Cage (C,n)) ; ::_thesis: contradiction
then consider x being set such that
A14: x in (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} and
A15: x in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A15;
A16: x in north_halfline (UMP (L~ (Cage (C,n)))) by A14, XBOOLE_0:def_5;
then A17: x `2 >= (UMP (L~ (Cage (C,n)))) `2 by TOPREAL1:def_10;
A18: x `1 = ((W-bound C) + (E-bound C)) / 2 by A8, A16, TOPREAL1:def_10;
then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) ;
then A19: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A15, XBOOLE_0:def_4;
proj2 . x = x `2 by PSCOMP_1:def_6;
then x `2 in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A19, FUNCT_2:35;
then A20: x `2 <= (UMP (L~ (Cage (C,n)))) `2 by A12, A11, SEQ_4:def_1;
not x in {(UMP (L~ (Cage (C,n))))} by A14, XBOOLE_0:def_5;
then x <> UMP (L~ (Cage (C,n))) by TARSKI:def_1;
then x `2 <> (UMP (L~ (Cage (C,n)))) `2 by A8, A18, TOPREAL3:6;
hence contradiction by A17, A20, XXREAL_0:1; ::_thesis: verum
end;
(north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is convex by JORDAN21:6;
then A21: ( (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} c= UBD (L~ (Cage (C,n))) or (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} c= BDD (L~ (Cage (C,n))) ) by A13, JORDAN1K:19;
A22: UBD (L~ (Cage (C,n))) c= UBD C by JORDAN10:13;
A23: not UMP C in {(UMP (L~ (Cage (C,n))))} by A10, TARSKI:def_1;
UMP C in north_halfline (UMP (L~ (Cage (C,n)))) by A1, A8, A10, TOPREAL1:def_10;
then A24: UMP C in (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} by A23, XBOOLE_0:def_5;
A25: UBD C misses C by JORDAN21:10;
not north_halfline (UMP (L~ (Cage (C,n)))) is bounded by JORDAN2C:122;
then A26: not (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is bounded by JORDAN21:1, TOPREAL6:90;
BDD (L~ (Cage (C,n))) is bounded by JORDAN2C:106;
then UMP C in UBD (L~ (Cage (C,n))) by A21, A26, A24, RLTOPSP1:42;
hence contradiction by A6, A22, A25, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
theorem Th18: :: JORDAN22:18
for C being Simple_closed_curve
for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
let n be Element of NAT ; ::_thesis: (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
set p = LMP (L~ (Cage (C,n)));
set u = LMP C;
set w = ((W-bound C) + (E-bound C)) / 2;
A1: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A2: LMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:31;
A3: LMP C = |[((LMP C) `1),((LMP C) `2)]| by EUCLID:53;
A4: LMP (L~ (Cage (C,n))) = |[((LMP (L~ (Cage (C,n)))) `1),((LMP (L~ (Cage (C,n)))) `2)]| by EUCLID:53;
A5: C misses L~ (Cage (C,n)) by JORDAN10:5;
A6: LMP C in C by JORDAN21:31;
A7: ((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33;
then A8: (LMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
assume A9: not (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
percases ( (LMP C) `2 = (LMP (L~ (Cage (C,n)))) `2 or (LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2 ) by A9, XXREAL_0:1;
suppose (LMP C) `2 = (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
hence contradiction by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0:3; ::_thesis: verum
end;
supposeA10: (LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction
A11: ( not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below ) by A7, JORDAN21:12, JORDAN21:13;
A12: (LMP (L~ (Cage (C,n)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) by A7, EUCLID:52;
A13: (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} misses L~ (Cage (C,n))
proof
assume (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} meets L~ (Cage (C,n)) ; ::_thesis: contradiction
then consider x being set such that
A14: x in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} and
A15: x in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A15;
A16: x in south_halfline (LMP (L~ (Cage (C,n)))) by A14, XBOOLE_0:def_5;
then A17: x `2 <= (LMP (L~ (Cage (C,n)))) `2 by TOPREAL1:def_12;
A18: x `1 = ((W-bound C) + (E-bound C)) / 2 by A8, A16, TOPREAL1:def_12;
then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) ;
then A19: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A15, XBOOLE_0:def_4;
proj2 . x = x `2 by PSCOMP_1:def_6;
then x `2 in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A19, FUNCT_2:35;
then A20: x `2 >= (LMP (L~ (Cage (C,n)))) `2 by A12, A11, SEQ_4:def_2;
not x in {(LMP (L~ (Cage (C,n))))} by A14, XBOOLE_0:def_5;
then x <> LMP (L~ (Cage (C,n))) by TARSKI:def_1;
then x `2 <> (LMP (L~ (Cage (C,n)))) `2 by A8, A18, TOPREAL3:6;
hence contradiction by A17, A20, XXREAL_0:1; ::_thesis: verum
end;
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is convex by JORDAN21:7;
then A21: ( (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= UBD (L~ (Cage (C,n))) or (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= BDD (L~ (Cage (C,n))) ) by A13, JORDAN1K:19;
A22: UBD (L~ (Cage (C,n))) c= UBD C by JORDAN10:13;
A23: not LMP C in {(LMP (L~ (Cage (C,n))))} by A10, TARSKI:def_1;
LMP C in south_halfline (LMP (L~ (Cage (C,n)))) by A1, A8, A10, TOPREAL1:def_12;
then A24: LMP C in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} by A23, XBOOLE_0:def_5;
A25: UBD C misses C by JORDAN21:10;
not south_halfline (LMP (L~ (Cage (C,n)))) is bounded by JORDAN2C:123;
then A26: not (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is bounded by JORDAN21:1, TOPREAL6:90;
BDD (L~ (Cage (C,n))) is bounded by JORDAN2C:106;
then LMP C in UBD (L~ (Cage (C,n))) by A21, A26, A24, RLTOPSP1:42;
hence contradiction by A6, A22, A25, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
theorem Th19: :: JORDAN22:19
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
let n be Element of NAT ; ::_thesis: ( 0 < n implies ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) )
set f = Cage (C,n);
set G = Gauge (C,n);
set w = Center (Gauge (C,n));
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31;
then A3: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63;
A4: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
assume A5: 0 < n ; ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
then UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13;
then A6: (UMP (L~ (Cage (C,n)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) by EUCLID:52;
A7: 1 <= len (Gauge (C,n)) by Lm3;
A8: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;
then A9: [(Center (Gauge (C,n))),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A7, A4, MATRIX_1:36;
[(Center (Gauge (C,n))),1] in Indices (Gauge (C,n)) by A2, A7, A8, A4, MATRIX_1:36;
then consider i being Element of NAT such that
A10: 1 <= i and
A11: i <= len (Gauge (C,n)) and
A12: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) /\ (L~ (Cage (C,n))))) by A1, A3, A7, A9, JORDAN1F:2;
A13: (UMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
thus ( 1 <= i & i <= len (Gauge (C,n)) ) by A10, A11; ::_thesis: UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i)
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A2, A10, A11, JORDAN1G:35;
then (UMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 by A13, JORDAN1G:33;
hence UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) by A12, A6, TOPREAL3:6; ::_thesis: verum
end;
theorem Th20: :: JORDAN22:20
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
let n be Element of NAT ; ::_thesis: ( 0 < n implies ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) )
set f = Cage (C,n);
set G = Gauge (C,n);
set w = Center (Gauge (C,n));
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31;
then A3: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63;
A4: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
assume A5: 0 < n ; ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
then LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14;
then A6: (LMP (L~ (Cage (C,n)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) by EUCLID:52;
A7: 1 <= len (Gauge (C,n)) by Lm3;
A8: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;
then A9: [(Center (Gauge (C,n))),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A7, A4, MATRIX_1:36;
[(Center (Gauge (C,n))),1] in Indices (Gauge (C,n)) by A2, A7, A8, A4, MATRIX_1:36;
then consider i being Element of NAT such that
A10: 1 <= i and
A11: i <= len (Gauge (C,n)) and
A12: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) /\ (L~ (Cage (C,n))))) by A1, A3, A7, A9, JORDAN1F:1;
A13: (LMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )
thus ( 1 <= i & i <= len (Gauge (C,n)) ) by A10, A11; ::_thesis: LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i)
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A2, A10, A11, JORDAN1G:35;
then (LMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 by A13, JORDAN1G:33;
hence LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) by A12, A6, TOPREAL3:6; ::_thesis: verum
end;
theorem Th21: :: JORDAN22:21
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))
let n be Element of NAT ; ::_thesis: ( 0 < n implies UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) )
set f = Cage (C,n);
set w = ((E-bound C) + (W-bound C)) / 2;
A1: Upper_Arc (L~ (Cage (C,n))) c= L~ (Cage (C,n)) by JORDAN6:61;
A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) by JORDAN1G:33;
A3: E-bound (L~ (Cage (C,n))) = E-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:18;
A4: W-bound (L~ (Cage (C,n))) = W-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:17;
assume A5: 0 < n ; ::_thesis: UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))
then A6: 0 + 1 <= n by NAT_1:13;
then A7: (n -' 1) + 1 = n by XREAL_1:235;
A8: now__::_thesis:_UMP_(L~_(Cage_(C,n)))_in_Upper_Arc_(L~_(Cage_(C,n)))
A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13;
A10: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
A11: (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) by JORDAN6:def_9;
assume A12: not UMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n))) ; ::_thesis: contradiction
UMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:30;
then A13: UMP (L~ (Cage (C,n))) in Lower_Arc (L~ (Cage (C,n))) by A12, A11, XBOOLE_0:def_3;
A14: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A15: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;
consider j being Element of NAT such that
A16: 1 <= j and
A17: j <= len (Gauge (C,n)) and
A18: UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j) by A5, Th19;
set a = (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))));
set b = (Gauge (C,n)) * ((Center (Gauge (C,n))),j);
set L = LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j)));
len (Gauge (C,1)) = width (Gauge (C,1)) by JORDAN8:def_1;
then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) meets Upper_Arc (L~ (Cage (C,n))) by A7, A13, A16, A17, A18, A14, JORDAN19:5;
then consider x being set such that
A19: x in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) and
A20: x in Upper_Arc (L~ (Cage (C,n))) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A19;
A21: (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) by RLTOPSP1:68;
A22: 1 <= len (Gauge (C,1)) by Lm3;
then A23: ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:38;
then A24: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A16, A17, A22, JORDAN1A:36;
then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) is vertical by A23, SPPOL_1:16;
then A25: x `1 = ((E-bound C) + (W-bound C)) / 2 by A19, A23, A21, SPPOL_1:def_3;
then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A26: x in (Upper_Arc (L~ (Cage (C,n)))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A20, XBOOLE_0:def_4;
then A27: (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 >= x `2 by A2, A4, A3, JORDAN21:28;
1 <= Center (Gauge (C,1)) by JORDAN1B:11;
then A28: ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A6, A15, A10, A9, JORDAN1A:40;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A16, A17, A15, A10, SPRECT_3:12;
then ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A28, XXREAL_0:2;
then A29: x `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A19, TOPREAL1:4;
(UMP (L~ (Cage (C,n)))) `2 >= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A26, JORDAN21:13, JORDAN21:43;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 >= x `2 by A18, A27, XXREAL_0:2;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 = x `2 by A29, XXREAL_0:1;
hence contradiction by A12, A18, A20, A24, A25, TOPREAL3:6; ::_thesis: verum
end;
proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above by A2, JORDAN21:13;
hence UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) by A1, A2, A4, A3, A8, JORDAN21:21, JORDAN21:45; ::_thesis: verum
end;
theorem Th22: :: JORDAN22:22
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n))))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n))))
let n be Element of NAT ; ::_thesis: ( 0 < n implies LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) )
set f = Cage (C,n);
set w = ((E-bound C) + (W-bound C)) / 2;
A1: Lower_Arc (L~ (Cage (C,n))) c= L~ (Cage (C,n)) by JORDAN6:61;
A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) by JORDAN1G:33;
A3: E-bound (L~ (Cage (C,n))) = E-bound (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:20;
A4: W-bound (L~ (Cage (C,n))) = W-bound (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:19;
assume A5: 0 < n ; ::_thesis: LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n))))
then A6: 0 + 1 <= n by NAT_1:13;
then A7: (n -' 1) + 1 = n by XREAL_1:235;
A8: now__::_thesis:_LMP_(L~_(Cage_(C,n)))_in_Lower_Arc_(L~_(Cage_(C,n)))
A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13;
A10: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A11: (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) by JORDAN6:def_9;
assume A12: not LMP (L~ (Cage (C,n))) in Lower_Arc (L~ (Cage (C,n))) ; ::_thesis: contradiction
consider j being Element of NAT such that
A13: 1 <= j and
A14: j <= len (Gauge (C,n)) and
A15: LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j) by A5, Th20;
set a = (Gauge (C,1)) * ((Center (Gauge (C,1))),1);
set b = (Gauge (C,n)) * ((Center (Gauge (C,n))),j);
set L = LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j)));
A16: (Gauge (C,1)) * ((Center (Gauge (C,1))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) by RLTOPSP1:68;
LMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:31;
then LMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n))) by A12, A11, XBOOLE_0:def_3;
then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) meets Lower_Arc (L~ (Cage (C,n))) by A7, A13, A14, A15, A10, JORDAN1J:62;
then consider x being set such that
A17: x in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) and
A18: x in Lower_Arc (L~ (Cage (C,n))) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A17;
A19: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;
A20: 1 <= len (Gauge (C,1)) by Lm3;
then A21: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:38;
then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A13, A14, A20, JORDAN1A:36;
then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) is vertical by A21, SPPOL_1:16;
then A23: x `1 = ((E-bound C) + (W-bound C)) / 2 by A17, A21, A16, SPPOL_1:def_3;
then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A24: x in (Lower_Arc (L~ (Cage (C,n)))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A18, XBOOLE_0:def_4;
then A25: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 <= x `2 by A2, A4, A3, JORDAN21:29;
A26: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13;
1 <= Center (Gauge (C,1)) by JORDAN1B:11;
then A27: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 by A6, A19, A26, A9, JORDAN1A:43;
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A13, A14, A10, A19, A26, SPRECT_3:12;
then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A27, XXREAL_0:2;
then A28: x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A17, TOPREAL1:4;
(LMP (L~ (Cage (C,n)))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A24, JORDAN21:13, JORDAN21:44;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 <= x `2 by A15, A25, XXREAL_0:2;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 = x `2 by A28, XXREAL_0:1;
hence contradiction by A12, A15, A18, A22, A23, TOPREAL3:6; ::_thesis: verum
end;
proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below by A2, JORDAN21:13;
hence LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) by A1, A2, A4, A3, A8, JORDAN21:22, JORDAN21:46; ::_thesis: verum
end;
theorem Th23: :: JORDAN22:23
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2
let n be Element of NAT ; ::_thesis: ( 0 < n implies (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 )
assume 0 < n ; ::_thesis: (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2
then UMP (Upper_Arc (L~ (Cage (C,n)))) = UMP (L~ (Cage (C,n))) by Th21;
hence (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by Th17; ::_thesis: verum
end;
theorem Th24: :: JORDAN22:24
for C being Simple_closed_curve
for n being Element of NAT st 0 < n holds
(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds
(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2
let n be Element of NAT ; ::_thesis: ( 0 < n implies (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 )
assume 0 < n ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2
then LMP (Lower_Arc (L~ (Cage (C,n)))) = LMP (L~ (Cage (C,n))) by Th22;
hence (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 by Th18; ::_thesis: verum
end;
theorem Th25: :: JORDAN22:25
for C being Simple_closed_curve
for i, j being Element of NAT st i <= j holds
(UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2
proof
let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st i <= j holds
(UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2
let i, j be Element of NAT ; ::_thesis: ( i <= j implies (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 )
set w = ((E-bound C) + (W-bound C)) / 2;
set ui = UMP (L~ (Cage (C,i)));
set uj = UMP (L~ (Cage (C,j)));
assume i <= j ; ::_thesis: (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2
then A1: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by JORDAN1H:47;
A2: (W-bound (L~ (Cage (C,j)))) + (E-bound (L~ (Cage (C,j)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A3: (UMP (L~ (Cage (C,j)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
assume (UMP (L~ (Cage (C,j)))) `2 > (UMP (L~ (Cage (C,i)))) `2 ; ::_thesis: contradiction
then A4: ((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2) > 0 by XREAL_1:50;
A5: (W-bound (L~ (Cage (C,i)))) + (E-bound (L~ (Cage (C,i)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A6: (UMP (L~ (Cage (C,i)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
A7: ( not proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A5, JORDAN21:12, JORDAN21:13;
( not proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A2, JORDAN21:12, JORDAN21:13;
then consider r being real number such that
A8: r in proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and
A9: (upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))))) - (((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2)) < r by A4, SEQ_4:def_1;
consider x being Point of (TOP-REAL 2) such that
A10: x in (L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) and
A11: proj2 . x = r by A8, Lm1;
A12: x `2 = r by A11, PSCOMP_1:def_6;
north_halfline x misses L~ (Cage (C,i))
proof
A13: x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by A10, XBOOLE_0:def_4;
assume north_halfline x meets L~ (Cage (C,i)) ; ::_thesis: contradiction
then consider y being set such that
A14: y in north_halfline x and
A15: y in L~ (Cage (C,i)) by XBOOLE_0:3;
reconsider y = y as Point of (TOP-REAL 2) by A15;
y `1 = x `1 by A14, TOPREAL1:def_10
.= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:31 ;
then y in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A16: y in (L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A15, XBOOLE_0:def_4;
proj2 . y = y `2 by PSCOMP_1:def_6;
then y `2 in proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:35;
then A17: y `2 <= (UMP (L~ (Cage (C,i)))) `2 by A6, A7, SEQ_4:def_1;
y `2 >= x `2 by A14, TOPREAL1:def_10;
hence contradiction by A3, A9, A12, A17, XXREAL_0:2; ::_thesis: verum
end;
then A18: north_halfline x c= UBD (L~ (Cage (C,i))) by JORDAN2C:129;
x in north_halfline x by TOPREAL1:38;
then x in UBD (L~ (Cage (C,i))) by A18;
then A19: x in LeftComp (Cage (C,i)) by GOBRD14:36;
x in L~ (Cage (C,j)) by A10, XBOOLE_0:def_4;
then LeftComp (Cage (C,j)) meets L~ (Cage (C,j)) by A1, A19, XBOOLE_0:3;
hence contradiction by SPRECT_3:26; ::_thesis: verum
end;
theorem Th26: :: JORDAN22:26
for C being Simple_closed_curve
for i, j being Element of NAT st i <= j holds
(LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2
proof
let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st i <= j holds
(LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2
let i, j be Element of NAT ; ::_thesis: ( i <= j implies (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 )
set w = ((E-bound C) + (W-bound C)) / 2;
set ui = LMP (L~ (Cage (C,i)));
set uj = LMP (L~ (Cage (C,j)));
assume i <= j ; ::_thesis: (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2
then A1: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by JORDAN1H:47;
A2: (W-bound (L~ (Cage (C,j)))) + (E-bound (L~ (Cage (C,j)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A3: (LMP (L~ (Cage (C,j)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
assume (LMP (L~ (Cage (C,i)))) `2 > (LMP (L~ (Cage (C,j)))) `2 ; ::_thesis: contradiction
then A4: ((LMP (L~ (Cage (C,i)))) `2) - ((LMP (L~ (Cage (C,j)))) `2) > 0 by XREAL_1:50;
A5: (W-bound (L~ (Cage (C,i)))) + (E-bound (L~ (Cage (C,i)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A6: (LMP (L~ (Cage (C,i)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
A7: ( not proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A5, JORDAN21:12, JORDAN21:13;
( not proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A2, JORDAN21:12, JORDAN21:13;
then consider r being real number such that
A8: r in proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and
A9: r < (lower_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))))) + (((LMP (L~ (Cage (C,i)))) `2) - ((LMP (L~ (Cage (C,j)))) `2)) by A4, SEQ_4:def_2;
consider x being Point of (TOP-REAL 2) such that
A10: x in (L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) and
A11: proj2 . x = r by A8, Lm1;
A12: x `2 = r by A11, PSCOMP_1:def_6;
south_halfline x misses L~ (Cage (C,i))
proof
A13: x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by A10, XBOOLE_0:def_4;
assume south_halfline x meets L~ (Cage (C,i)) ; ::_thesis: contradiction
then consider y being set such that
A14: y in south_halfline x and
A15: y in L~ (Cage (C,i)) by XBOOLE_0:3;
reconsider y = y as Point of (TOP-REAL 2) by A15;
y `1 = x `1 by A14, TOPREAL1:def_12
.= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:31 ;
then y in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A16: y in (L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A15, XBOOLE_0:def_4;
proj2 . y = y `2 by PSCOMP_1:def_6;
then y `2 in proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:35;
then A17: y `2 >= (LMP (L~ (Cage (C,i)))) `2 by A6, A7, SEQ_4:def_2;
y `2 <= x `2 by A14, TOPREAL1:def_12;
hence contradiction by A3, A9, A12, A17, XXREAL_0:2; ::_thesis: verum
end;
then A18: south_halfline x c= UBD (L~ (Cage (C,i))) by JORDAN2C:128;
x in south_halfline x by TOPREAL1:38;
then x in UBD (L~ (Cage (C,i))) by A18;
then A19: x in LeftComp (Cage (C,i)) by GOBRD14:36;
x in L~ (Cage (C,j)) by A10, XBOOLE_0:def_4;
then LeftComp (Cage (C,j)) meets L~ (Cage (C,j)) by A1, A19, XBOOLE_0:3;
hence contradiction by SPRECT_3:26; ::_thesis: verum
end;
theorem Th27: :: JORDAN22:27
for C being Simple_closed_curve
for i, j being Element of NAT st 0 < i & i <= j holds
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2
proof
let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st 0 < i & i <= j holds
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2
let i, j be Element of NAT ; ::_thesis: ( 0 < i & i <= j implies (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 )
assume that
A1: 0 < i and
A2: i <= j ; ::_thesis: (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2
A3: (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 = (UMP (L~ (Cage (C,i)))) `2 by A1, Th21;
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 = (UMP (L~ (Cage (C,j)))) `2 by A1, A2, Th21;
hence (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 by A2, A3, Th25; ::_thesis: verum
end;
theorem Th28: :: JORDAN22:28
for C being Simple_closed_curve
for i, j being Element of NAT st 0 < i & i <= j holds
(LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2
proof
let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st 0 < i & i <= j holds
(LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2
let i, j be Element of NAT ; ::_thesis: ( 0 < i & i <= j implies (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 )
assume that
A1: 0 < i and
A2: i <= j ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2
A3: (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 = (LMP (L~ (Cage (C,i)))) `2 by A1, Th22;
(LMP (Lower_Arc (L~ (Cage (C,j))))) `2 = (LMP (L~ (Cage (C,j)))) `2 by A1, A2, Th22;
hence (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 by A2, A3, Th26; ::_thesis: verum
end;
begin
theorem Th29: :: JORDAN22:29
for C being Simple_closed_curve holds W-min C in North_Arc C
proof
let C be Simple_closed_curve; ::_thesis: W-min C in North_Arc C
reconsider w = W-min C as Point of (Euclid 2) by EUCLID:67;
A1: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
then r / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
1 < k and
A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and
A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11;
take k ; ::_thesis: for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
let m be Element of NAT ; ::_thesis: ( m > k implies (Upper_Appr C) . m meets Ball (w,r) )
assume A4: m > k ; ::_thesis: (Upper_Appr C) . m meets Ball (w,r)
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9;
then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2;
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11;
then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2;
A7: 1 + 1 <= len (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A8: (left_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
reconsider p = W-min (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A9: W-min (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1;
then A10: Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
W-min (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:43;
then A11: W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Element of NAT such that
A12: [i,j] in Indices (Gauge (C,m)) and
A13: [i,(j + 1)] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,j) and
A15: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,(j + 1)) by A7, A10, JORDAN1I:21;
A16: 1 <= j by A12, MATRIX_1:38;
i < len (Gauge (C,m)) by A7, A10, A12, A13, A14, A15, JORDAN1I:14;
then A17: i + 1 <= len (Gauge (C,m)) by NAT_1:13;
A18: 1 <= i + 1 by NAT_1:11;
j <= width (Gauge (C,m)) by A12, MATRIX_1:38;
then A19: [(i + 1),j] in Indices (Gauge (C,m)) by A16, A18, A17, MATRIX_1:36;
[(1 + 1),1] in Indices (Gauge (C,m)) by Th7;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) by A12, A19, GOBRD14:10;
then A20: (((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2 by A12, A19, A6, GOBRD14:5;
[1,(1 + 1)] in Indices (Gauge (C,m)) by Th6;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) by A12, A13, GOBRD14:9;
then (((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2 by A12, A13, A5, GOBRD14:6;
then A21: ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) < (r / 2) + (r / 2) by A20, XREAL_1:8;
A22: 1 <= i by A12, MATRIX_1:38;
right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))))) by A7, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A23: right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),i,j) by A7, A10, A12, A13, A14, A15, GOBRD13:22;
A24: j + 1 <= width (Gauge (C,m)) by A13, MATRIX_1:38;
(Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A7, TOPREAL1:21;
then A25: W-min (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A11, A8, XBOOLE_0:def_4;
then A26: ((Gauge (C,m)) * (i,j)) `1 <= (W-min (L~ (Cage (C,m)))) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A27: W-min C in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by JORDAN1I:6;
then A28: (W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A29: ((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A30: (W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A31: (W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A32: (W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
A33: ((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:95;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) < r by A21, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def_1;
then A34: p in Ball (w,r) by METRIC_1:11;
(Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1;
hence (Upper_Appr C) . m meets Ball (w,r) by A9, A34, XBOOLE_0:3; ::_thesis: verum
end;
North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3;
hence W-min C in North_Arc C by A1, KURATO_2:14; ::_thesis: verum
end;
theorem Th30: :: JORDAN22:30
for C being Simple_closed_curve holds E-max C in North_Arc C
proof
let C be Simple_closed_curve; ::_thesis: E-max C in North_Arc C
reconsider w = E-max C as Point of (Euclid 2) by EUCLID:67;
A1: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
then r / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
1 < k and
A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and
A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11;
take k ; ::_thesis: for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
let m be Element of NAT ; ::_thesis: ( m > k implies (Upper_Appr C) . m meets Ball (w,r) )
assume A4: m > k ; ::_thesis: (Upper_Appr C) . m meets Ball (w,r)
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9;
then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2;
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11;
then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2;
reconsider p = E-max (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A7: E-max (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1;
A8: 1 + 1 <= len (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A9: (left_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1;
then A10: Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
E-max (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:46;
then A11: E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = E-max (L~ (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Element of NAT such that
A12: [i,(j + 1)] in Indices (Gauge (C,m)) and
A13: [i,j] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,(j + 1)) and
A15: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,j) by A8, A10, JORDAN1I:23;
A16: i <= len (Gauge (C,m)) by A12, MATRIX_1:38;
i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I:16;
then A17: i - 1 > 1 - 1 by XREAL_1:14;
then A18: i -' 1 = i - 1 by XREAL_0:def_2;
then A19: i -' 1 <= len (Gauge (C,m)) by A16, XREAL_1:146, XXREAL_0:2;
i - 1 is Element of NAT by A17, INT_1:3;
then A20: i - 1 >= 0 + 1 by A17, NAT_1:13;
then A21: (i -' 1) + 1 = i by NAT_D:43;
right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))))) by A8, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A22: right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),(i -' 1),j) by A8, A10, A12, A13, A14, A15, GOBRD13:28;
A23: j + 1 <= width (Gauge (C,m)) by A12, MATRIX_1:38;
1 <= j + 1 by NAT_1:11;
then A24: [(i -' 1),(j + 1)] in Indices (Gauge (C,m)) by A23, A20, A18, A19, MATRIX_1:36;
A25: 1 <= j by A13, MATRIX_1:38;
j <= width (Gauge (C,m)) by A13, MATRIX_1:38;
then A26: [(i -' 1),j] in Indices (Gauge (C,m)) by A25, A20, A18, A19, MATRIX_1:36;
[1,(1 + 1)] in Indices (Gauge (C,m)) by Th6;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * ((i -' 1),(j + 1)))) by A26, A24, GOBRD14:9;
then A27: (((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2 by A26, A24, A5, GOBRD14:6;
[(1 + 1),1] in Indices (Gauge (C,m)) by Th7;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * (((i -' 1) + 1),j))) by A13, A21, A26, GOBRD14:10;
then (((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2 by A13, A21, A26, A6, GOBRD14:5;
then A28: ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) < (r / 2) + (r / 2) by A27, XREAL_1:8;
A29: E-max C in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by JORDAN1I:7;
then A30: (E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
(Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A8, TOPREAL1:21;
then A31: E-max (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A11, A9, XBOOLE_0:def_4;
then A32: ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max (L~ (Cage (C,m)))) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
A33: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A34: (E-max (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A35: (E-max (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A36: (E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A37: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:95;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) < r by A28, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def_1;
then A38: p in Ball (w,r) by METRIC_1:11;
(Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1;
hence (Upper_Appr C) . m meets Ball (w,r) by A7, A38, XBOOLE_0:3; ::_thesis: verum
end;
North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3;
hence E-max C in North_Arc C by A1, KURATO_2:14; ::_thesis: verum
end;
theorem Th31: :: JORDAN22:31
for C being Simple_closed_curve holds W-min C in South_Arc C
proof
let C be Simple_closed_curve; ::_thesis: W-min C in South_Arc C
reconsider w = W-min C as Point of (Euclid 2) by EUCLID:67;
A1: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
then r / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
1 < k and
A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and
A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11;
take k ; ::_thesis: for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
let m be Element of NAT ; ::_thesis: ( m > k implies (Lower_Appr C) . m meets Ball (w,r) )
assume A4: m > k ; ::_thesis: (Lower_Appr C) . m meets Ball (w,r)
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9;
then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2;
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11;
then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2;
A7: 1 + 1 <= len (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A8: (left_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
reconsider p = W-min (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A9: W-min (L~ (Cage (C,m))) in Lower_Arc (L~ (Cage (C,m))) by JORDAN7:1;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1;
then A10: Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
W-min (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:43;
then A11: W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Element of NAT such that
A12: [i,j] in Indices (Gauge (C,m)) and
A13: [i,(j + 1)] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,j) and
A15: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,(j + 1)) by A7, A10, JORDAN1I:21;
A16: 1 <= j by A12, MATRIX_1:38;
i < len (Gauge (C,m)) by A7, A10, A12, A13, A14, A15, JORDAN1I:14;
then A17: i + 1 <= len (Gauge (C,m)) by NAT_1:13;
A18: 1 <= i + 1 by NAT_1:11;
j <= width (Gauge (C,m)) by A12, MATRIX_1:38;
then A19: [(i + 1),j] in Indices (Gauge (C,m)) by A16, A18, A17, MATRIX_1:36;
[(1 + 1),1] in Indices (Gauge (C,m)) by Th7;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) by A12, A19, GOBRD14:10;
then A20: (((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2 by A12, A19, A6, GOBRD14:5;
[1,(1 + 1)] in Indices (Gauge (C,m)) by Th6;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) by A12, A13, GOBRD14:9;
then (((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2 by A12, A13, A5, GOBRD14:6;
then A21: ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) < (r / 2) + (r / 2) by A20, XREAL_1:8;
A22: 1 <= i by A12, MATRIX_1:38;
right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))))) by A7, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A23: right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),i,j) by A7, A10, A12, A13, A14, A15, GOBRD13:22;
A24: j + 1 <= width (Gauge (C,m)) by A13, MATRIX_1:38;
(Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A7, TOPREAL1:21;
then A25: W-min (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A11, A8, XBOOLE_0:def_4;
then A26: ((Gauge (C,m)) * (i,j)) `1 <= (W-min (L~ (Cage (C,m)))) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A27: W-min C in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by JORDAN1I:6;
then A28: (W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A29: ((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A30: (W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A31: (W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A32: (W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
A33: ((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:95;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) < r by A21, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def_1;
then A34: p in Ball (w,r) by METRIC_1:11;
(Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2;
hence (Lower_Appr C) . m meets Ball (w,r) by A9, A34, XBOOLE_0:3; ::_thesis: verum
end;
South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4;
hence W-min C in South_Arc C by A1, KURATO_2:14; ::_thesis: verum
end;
theorem Th32: :: JORDAN22:32
for C being Simple_closed_curve holds E-max C in South_Arc C
proof
let C be Simple_closed_curve; ::_thesis: E-max C in South_Arc C
reconsider w = E-max C as Point of (Euclid 2) by EUCLID:67;
A1: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
then r / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
1 < k and
A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and
A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11;
take k ; ::_thesis: for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (w,r)
let m be Element of NAT ; ::_thesis: ( m > k implies (Lower_Appr C) . m meets Ball (w,r) )
assume A4: m > k ; ::_thesis: (Lower_Appr C) . m meets Ball (w,r)
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9;
then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2;
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11;
then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2;
reconsider p = E-max (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A7: E-max (L~ (Cage (C,m))) in Lower_Arc (L~ (Cage (C,m))) by JORDAN7:1;
A8: 1 + 1 <= len (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A9: (left_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1;
then A10: Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
E-max (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:46;
then A11: E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = E-max (L~ (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Element of NAT such that
A12: [i,(j + 1)] in Indices (Gauge (C,m)) and
A13: [i,j] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,(j + 1)) and
A15: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,j) by A8, A10, JORDAN1I:23;
A16: i <= len (Gauge (C,m)) by A12, MATRIX_1:38;
i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I:16;
then A17: i - 1 > 1 - 1 by XREAL_1:14;
then A18: i -' 1 = i - 1 by XREAL_0:def_2;
then A19: i -' 1 <= len (Gauge (C,m)) by A16, XREAL_1:146, XXREAL_0:2;
i - 1 is Element of NAT by A17, INT_1:3;
then A20: i - 1 >= 0 + 1 by A17, NAT_1:13;
then A21: (i -' 1) + 1 = i by NAT_D:43;
right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))))) by A8, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A22: right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),(i -' 1),j) by A8, A10, A12, A13, A14, A15, GOBRD13:28;
A23: j + 1 <= width (Gauge (C,m)) by A12, MATRIX_1:38;
1 <= j + 1 by NAT_1:11;
then A24: [(i -' 1),(j + 1)] in Indices (Gauge (C,m)) by A23, A20, A18, A19, MATRIX_1:36;
A25: 1 <= j by A13, MATRIX_1:38;
j <= width (Gauge (C,m)) by A13, MATRIX_1:38;
then A26: [(i -' 1),j] in Indices (Gauge (C,m)) by A25, A20, A18, A19, MATRIX_1:36;
[1,(1 + 1)] in Indices (Gauge (C,m)) by Th6;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * ((i -' 1),(j + 1)))) by A26, A24, GOBRD14:9;
then A27: (((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2 by A26, A24, A5, GOBRD14:6;
[(1 + 1),1] in Indices (Gauge (C,m)) by Th7;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * (((i -' 1) + 1),j))) by A13, A21, A26, GOBRD14:10;
then (((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2 by A13, A21, A26, A6, GOBRD14:5;
then A28: ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) < (r / 2) + (r / 2) by A27, XREAL_1:8;
A29: E-max C in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by JORDAN1I:7;
then A30: (E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
(Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A8, TOPREAL1:21;
then A31: E-max (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A11, A9, XBOOLE_0:def_4;
then A32: ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max (L~ (Cage (C,m)))) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
A33: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A34: (E-max (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A35: (E-max (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A36: (E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A37: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:95;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) < r by A28, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def_1;
then A38: p in Ball (w,r) by METRIC_1:11;
(Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2;
hence (Lower_Appr C) . m meets Ball (w,r) by A7, A38, XBOOLE_0:3; ::_thesis: verum
end;
South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4;
hence E-max C in South_Arc C by A1, KURATO_2:14; ::_thesis: verum
end;
Lm4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def_8;
theorem Th33: :: JORDAN22:33
for C being Simple_closed_curve holds UMP C in North_Arc C
proof
let C be Simple_closed_curve; ::_thesis: UMP C in North_Arc C
set w = ((W-bound C) + (E-bound C)) / 2;
set p = UMP C;
set U = { (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } ;
set n0 = N-bound (L~ (Cage (C,1)));
set H = LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|);
A1: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A2: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
{ (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } or x in the carrier of (TOP-REAL 2) )
assume x in { (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex n being Element of NAT st
( x = UMP (Upper_Arc (L~ (Cage (C,n)))) & 0 < n ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider U = { (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } as Subset of (TOP-REAL 2) ;
set q = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U));
set S = LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|);
A3: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
A4: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| `2 = N-bound (L~ (Cage (C,1))) by EUCLID:52;
A5: for n being Element of NAT holds (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let n be Element of NAT ; ::_thesis: (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
A6: (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
thus (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound (Upper_Arc (L~ (Cage (C,n))))) + (E-bound (Upper_Arc (L~ (Cage (C,n)))))) / 2 by EUCLID:52
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (Upper_Arc (L~ (Cage (C,n)))))) / 2 by JORDAN21:17
.= ((W-bound C) + (E-bound C)) / 2 by A6, JORDAN21:18 ; ::_thesis: verum
end;
A7: (UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 by Th23;
A8: (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) /\ C = {(UMP C)} by JORDAN21:34;
A9: (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 <= N-bound (L~ (Cage (C,1))) by JORDAN21:47;
(LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U is bounded by TOPREAL6:89;
then proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) is real-bounded by JCT_MISC:14;
then A10: proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) is bounded_below by XXREAL_2:def_11;
A11: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A12: for n being Element of NAT st 0 < n holds
(UMP (Upper_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)
proof
let n be Element of NAT ; ::_thesis: ( 0 < n implies (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) )
set f = Cage (C,n);
set s = UMP (Upper_Arc (L~ (Cage (C,n))));
assume A13: 0 < n ; ::_thesis: (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)
then A14: UMP (Upper_Arc (L~ (Cage (C,n)))) in U ;
0 + 1 <= n by A13, NAT_1:13;
then ( 1 < n or n = 1 ) by XXREAL_0:1;
then A15: N-bound (L~ (Cage (C,n))) <= N-bound (L~ (Cage (C,1))) by JORDAN10:7;
(UMP (Upper_Arc (L~ (Cage (C,n))))) `2 <= N-bound (L~ (Cage (C,n))) by JORDAN21:47;
then A16: (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 <= N-bound (L~ (Cage (C,1))) by A15, XXREAL_0:2;
A17: (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
(UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A13, Th23;
then UMP (Upper_Arc (L~ (Cage (C,n)))) in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) by A2, A4, A11, A16, A17, GOBOARD7:7;
then A18: UMP (Upper_Arc (L~ (Cage (C,n)))) in (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U by A14, XBOOLE_0:def_4;
(UMP (Upper_Arc (L~ (Cage (C,n))))) `2 = proj2 . (UMP (Upper_Arc (L~ (Cage (C,n))))) by PSCOMP_1:def_6;
hence (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) by A18, FUNCT_2:35; ::_thesis: verum
end;
then A19: (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) ;
then lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 by A10, SEQ_4:def_2;
then A20: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= N-bound (L~ (Cage (C,1))) by A9, XXREAL_0:2;
A21: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A22: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) is vertical by A2, SPPOL_1:16;
A23: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) by RLTOPSP1:68;
A24: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| `2 = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52;
percases ( UMP C <> |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| or UMP C = |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ) ;
supposeA25: UMP C <> |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: UMP C in North_Arc C
consider S9, C9 being Subset of (TopSpaceMetr (Euclid 2)) such that
A26: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) = S9 and
A27: C = C9 and
A28: dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C) = min_dist_min (S9,C9) by JORDAN1K:def_1;
A29: S9 is compact by A26, Lm4, COMPTS_1:23;
A30: C9 is compact by A27, Lm4, COMPTS_1:23;
A31: now__::_thesis:_not_(UMP_C)_`2_>=_lower_bound_(proj2_.:_((LSeg_((UMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_(L~_(Cage_(C,1))))]|))_/\_U))
assume A32: (UMP C) `2 >= lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
percases ( (UMP C) `2 = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) or (UMP C) `2 > lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) ) by A32, XXREAL_0:1;
suppose (UMP C) `2 = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
hence contradiction by A25, EUCLID:52; ::_thesis: verum
end;
suppose (UMP C) `2 > lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
then 0 < ((UMP C) `2) - (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) by XREAL_1:50;
then consider r being real number such that
A33: r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) and
A34: r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + (((UMP C) `2) - (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))) by A10, A19, SEQ_4:def_2;
consider t being Point of (TOP-REAL 2) such that
A35: t in (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U and
A36: proj2 . t = r by A33, Lm1;
A37: t in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) by A35, XBOOLE_0:def_4;
A38: (UMP C) `2 <= N-bound (L~ (Cage (C,1))) by A9, A7, XXREAL_0:2;
t `2 = r by A36, PSCOMP_1:def_6;
hence contradiction by A4, A34, A38, A37, TOPREAL1:4; ::_thesis: verum
end;
end;
end;
LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) misses C
proof
assume LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) meets C ; ::_thesis: contradiction
then consider x being set such that
A39: x in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) and
A40: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A39;
A41: x `2 <= N-bound C by A40, PSCOMP_1:24;
A42: x `1 = ((W-bound C) + (E-bound C)) / 2 by A21, A23, A22, A39, SPPOL_1:def_3;
A43: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= x `2 by A4, A24, A20, A39, TOPREAL1:4;
then (UMP C) `2 < x `2 by A31, XXREAL_0:2;
then x in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) by A1, A3, A11, A41, A42, GOBOARD7:7;
then x in {(UMP C)} by A8, A40, XBOOLE_0:def_4;
hence contradiction by A31, A43, TARSKI:def_1; ::_thesis: verum
end;
then dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C) > 0 by A26, A27, A28, A29, A30, JGRAPH_1:38;
then (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C)) / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
A44: 1 < k and
A45: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C)) / 2 and
A46: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C)) / 2 by GOBRD14:11;
set f = Cage (C,k);
set G = Gauge (C,k);
set s = UMP (Upper_Arc (L~ (Cage (C,k))));
A47: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= N-bound (L~ (Cage (C,k))) by JORDAN21:47;
A48: (dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * ((1 + 1),1)))) + (dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,(1 + 1))))) < ((dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C)) / 2) + ((dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)),C)) / 2) by A45, A46, XREAL_1:8;
N-bound (L~ (Cage (C,k))) <= N-bound (L~ (Cage (C,1))) by A44, JORDAN10:7;
then A49: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= N-bound (L~ (Cage (C,1))) by A47, XXREAL_0:2;
(UMP (Upper_Arc (L~ (Cage (C,k))))) `2 in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) by A12, A44;
then A50: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A10, SEQ_4:def_2;
[1,(1 + 1)] in Indices (Gauge (C,k)) by Th6;
then A51: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by Th5, GOBRD14:9;
[(1 + 1),1] in Indices (Gauge (C,k)) by Th7;
then A52: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by Th5, GOBRD14:10;
A53: UMP (Upper_Arc (L~ (Cage (C,k)))) in Upper_Arc (L~ (Cage (C,k))) by JORDAN21:30;
Upper_Arc (L~ (Cage (C,k))) c= L~ (Cage (C,k)) by JORDAN6:61;
then consider i being Element of NAT such that
A54: 1 <= i and
A55: i + 1 <= len (Cage (C,k)) and
A56: UMP (Upper_Arc (L~ (Cage (C,k)))) in LSeg ((Cage (C,k)),i) by A53, SPPOL_2:13;
A57: Cage (C,k) is_sequence_on Gauge (C,k) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A58: [i1,j1] in Indices (Gauge (C,k)) and
A59: (Cage (C,k)) /. i = (Gauge (C,k)) * (i1,j1) and
A60: [i2,j2] in Indices (Gauge (C,k)) and
A61: (Cage (C,k)) /. (i + 1) = (Gauge (C,k)) * (i2,j2) and
A62: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A54, A55, JORDAN8:3;
A63: 1 <= i1 by A58, MATRIX_1:38;
right_cell ((Cage (C,k)),i,(Gauge (C,k))) meets C by A54, A55, JORDAN9:31;
then consider c being set such that
A64: c in right_cell ((Cage (C,k)),i,(Gauge (C,k))) and
A65: c in C by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A65;
reconsider s9 = UMP (Upper_Arc (L~ (Cage (C,k)))), c9 = c as Point of (Euclid 2) by EUCLID:67;
(UMP (Upper_Arc (L~ (Cage (C,k))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then UMP (Upper_Arc (L~ (Cage (C,k)))) in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) by A2, A4, A21, A24, A49, A50, GOBOARD7:7;
then A66: min_dist_min (S9,C9) <= dist (s9,c9) by A26, A27, A29, A30, A65, WEIERSTR:34;
A67: dist (s9,c9) = dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) by TOPREAL6:def_1;
A68: 1 <= j2 by A60, MATRIX_1:38;
(left_cell ((Cage (C,k)),i,(Gauge (C,k)))) /\ (right_cell ((Cage (C,k)),i,(Gauge (C,k)))) = LSeg ((Cage (C,k)),i) by A54, A55, A57, GOBRD13:29;
then A69: UMP (Upper_Arc (L~ (Cage (C,k)))) in right_cell ((Cage (C,k)),i,(Gauge (C,k))) by A56, XBOOLE_0:def_4;
A70: j2 <= width (Gauge (C,k)) by A60, MATRIX_1:38;
A71: (j2 + 1) + 1 <> j2 ;
A72: 1 <= i2 by A60, MATRIX_1:38;
A73: j1 <= width (Gauge (C,k)) by A58, MATRIX_1:38;
A74: 1 <= j1 + 1 by NAT_1:11;
A75: i1 + 1 <> i1 + 0 ;
A76: i1 <= len (Gauge (C,k)) by A58, MATRIX_1:38;
A77: i2 <= len (Gauge (C,k)) by A60, MATRIX_1:38;
A78: (i2 + 1) + 1 <> i2 ;
A79: 1 <= j1 by A58, MATRIX_1:38;
A80: 1 <= i1 + 1 by NAT_1:11;
now__::_thesis:_contradiction
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A62;
supposeA81: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: contradiction
then A82: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * (i1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A60, GOBRD14:9;
A83: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * (i1,(j1 + 1)))) = (((Gauge (C,k)) * (i1,(j1 + 1))) `2) - (((Gauge (C,k)) * (i1,j1)) `2) by A58, A60, A81, GOBRD14:6;
i1 < len (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A81, JORDAN10:1;
then A84: i1 + 1 <= len (Gauge (C,k)) by NAT_1:13;
then A85: [(i1 + 1),j1] in Indices (Gauge (C,k)) by A79, A80, A73, MATRIX_1:36;
then A86: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * ((i1 + 1),j1))) = (((Gauge (C,k)) * ((i1 + 1),j1)) `1) - (((Gauge (C,k)) * (i1,j1)) `1) by A58, GOBRD14:5;
A87: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * ((i1 + 1),j1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A85, GOBRD14:10;
A88: j1 + 1 <= width (Gauge (C,k)) by A60, A81, MATRIX_1:38;
A89: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,j1) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A81, GOBRD13:def_2;
then A90: c `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A64, A63, A79, A88, A84, JORDAN9:17;
A91: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A92: ((Gauge (C,k)) * (i1,j1)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A93: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A94: ((Gauge (C,k)) * (i1,j1)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A95: c `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
A96: ((Gauge (C,k)) * (i1,j1)) `2 <= c `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
((Gauge (C,k)) * (i1,j1)) `1 <= c `1 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
then dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i1 + 1),j1)) `1) - (((Gauge (C,k)) * (i1,j1)) `1)) + ((((Gauge (C,k)) * (i1,(j1 + 1))) `2) - (((Gauge (C,k)) * (i1,j1)) `2)) by A90, A96, A95, A94, A93, A92, A91, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A86, A83, A82, A87, XXREAL_0:2; ::_thesis: verum
end;
supposeA97: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction
then 1 < j1 by A54, A55, A58, A59, A60, A61, JORDAN10:3;
then A98: 1 <= j1 -' 1 by NAT_D:49;
then A99: (j1 -' 1) + 1 = j1 by NAT_D:43;
A100: j1 -' 1 <= width (Gauge (C,k)) by A73, NAT_D:44;
then A101: [i1,(j1 -' 1)] in Indices (Gauge (C,k)) by A63, A76, A98, MATRIX_1:36;
then A102: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * (i1,((j1 -' 1) + 1)))) = (((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `2) by A58, A99, GOBRD14:6;
A103: [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,k)) by A72, A77, A97, A98, A100, MATRIX_1:36;
then A104: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * ((i1 + 1),(j1 -' 1)))) = (((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `1) by A101, GOBRD14:5;
A105: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * (i1,((j1 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A99, A101, GOBRD14:9;
A106: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * ((i1 + 1),(j1 -' 1)))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A101, A103, GOBRD14:10;
A107: i1 + 1 <= len (Gauge (C,k)) by A60, A97, MATRIX_1:38;
A108: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,(j1 -' 1)) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A97, GOBRD13:def_2;
then A109: c `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A64, A63, A73, A107, A98, A99, JORDAN9:17;
A110: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A111: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A112: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A113: ((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A114: c `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A115: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= c `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= c `1 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
then dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `1)) + ((((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `2)) by A109, A115, A114, A113, A112, A111, A110, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A104, A102, A105, A106, XXREAL_0:2; ::_thesis: verum
end;
supposeA116: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction
then A117: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * ((i2 + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A60, GOBRD14:10;
A118: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * ((i2 + 1),j2))) = (((Gauge (C,k)) * ((i2 + 1),j2)) `1) - (((Gauge (C,k)) * (i2,j2)) `1) by A58, A60, A116, GOBRD14:5;
A119: i2 + 1 <= len (Gauge (C,k)) by A58, A116, MATRIX_1:38;
j1 < width (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A116, JORDAN10:4;
then A120: j1 + 1 <= width (Gauge (C,k)) by NAT_1:13;
then A121: [i2,(j2 + 1)] in Indices (Gauge (C,k)) by A72, A74, A77, A116, MATRIX_1:36;
then A122: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * (i2,(j2 + 1)))) = (((Gauge (C,k)) * (i2,(j2 + 1))) `2) - (((Gauge (C,k)) * (i2,j2)) `2) by A60, GOBRD14:6;
A123: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i2,j2) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A116, GOBRD13:def_2;
then A124: c `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A64, A79, A72, A116, A119, A120, JORDAN9:17;
A125: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A126: ((Gauge (C,k)) * (i2,j2)) `2 <= c `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A127: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * (i2,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A60, A121, GOBRD14:9;
A128: ((Gauge (C,k)) * (i2,j2)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A129: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A130: ((Gauge (C,k)) * (i2,j2)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A131: c `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
((Gauge (C,k)) * (i2,j2)) `1 <= c `1 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
then dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i2 + 1),j2)) `1) - (((Gauge (C,k)) * (i2,j2)) `1)) + ((((Gauge (C,k)) * (i2,(j2 + 1))) `2) - (((Gauge (C,k)) * (i2,j2)) `2)) by A124, A126, A131, A130, A129, A128, A125, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A118, A122, A127, A117, XXREAL_0:2; ::_thesis: verum
end;
supposeA132: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: contradiction
then 1 < i1 by A54, A55, A58, A59, A60, A61, JORDAN10:2;
then A133: 1 <= i1 -' 1 by NAT_D:49;
A134: i1 -' 1 <= len (Gauge (C,k)) by A76, NAT_D:44;
then A135: [(i1 -' 1),j2] in Indices (Gauge (C,k)) by A68, A70, A133, MATRIX_1:36;
A136: [(i1 -' 1),(j2 + 1)] in Indices (Gauge (C,k)) by A79, A73, A132, A133, A134, MATRIX_1:36;
then A137: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * ((i1 -' 1),(j2 + 1)))) = (((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `2) by A135, GOBRD14:6;
A138: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * ((i1 -' 1),(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A135, A136, GOBRD14:9;
A139: j2 + 1 <= width (Gauge (C,k)) by A58, A132, MATRIX_1:38;
A140: (i1 -' 1) + 1 = i1 by A133, NAT_D:43;
then A141: [((i1 -' 1) + 1),j2] in Indices (Gauge (C,k)) by A63, A68, A76, A70, MATRIX_1:36;
then A142: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * (((i1 -' 1) + 1),j2))) = (((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `1) by A135, GOBRD14:5;
A143: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),(i1 -' 1),j2) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A132, GOBRD13:def_2;
then A144: c `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A64, A68, A76, A139, A133, A140, JORDAN9:17;
A145: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A146: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A147: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A148: ((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A149: c `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A150: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= c `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A151: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * (((i1 -' 1) + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A135, A141, GOBRD14:10;
((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= c `1 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
then dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `1)) + ((((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `2)) by A144, A150, A149, A148, A147, A146, A145, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A142, A137, A138, A151, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence UMP C in North_Arc C ; ::_thesis: verum
end;
suppose UMP C = |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: UMP C in North_Arc C
then A152: (UMP C) `2 = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52;
A153: ex S being Real_Sequence of 2 st
( S is convergent & ( for x being Element of NAT holds S . x in (Upper_Appr C) . x ) & UMP C = lim S )
proof
set R = { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } ;
{ ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } or x in REAL )
assume x in { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } ; ::_thesis: x in REAL
then ex n being Element of NAT st
( x = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider R = { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } as Subset of REAL ;
deffunc H1( Element of NAT ) -> Element of the carrier of (TOP-REAL 2) = UMP (Upper_Arc (L~ (Cage (C,$1))));
reconsider pp = UMP C as Element of REAL 2 by EUCLID:22;
reconsider p1 = UMP C as Element of (TOP-REAL 2) ;
A154: for x being Element of NAT holds H1(x) is Element of REAL 2 by EUCLID:22;
consider S being Function of NAT,(REAL 2) such that
A155: for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_9(A154);
the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
then reconsider SS = S as Real_Sequence of 2 ;
take SS ; ::_thesis: ( SS is convergent & ( for x being Element of NAT holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
A156: R is bounded_below
proof
take lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) ; :: according to XXREAL_2:def_9 ::_thesis: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) is LowerBound of R
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in R or lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r )
assume r in R ; ::_thesis: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r
then ex n being Element of NAT st
( r = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) by A12;
hence lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r by A10, SEQ_4:def_2; ::_thesis: verum
end;
A157: (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 in R ;
A158: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
proof
A159: for s being real number st 0 < s holds
ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s )
then consider r being real number such that
A160: r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) and
A161: r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s by A10, A19, SEQ_4:def_2;
take r ; ::_thesis: ( r in R & r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s )
consider x being Point of (TOP-REAL 2) such that
A162: x in (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U and
A163: proj2 . x = r by A160, Lm1;
x in U by A162, XBOOLE_0:def_4;
then consider n being Element of NAT such that
A164: x = UMP (Upper_Arc (L~ (Cage (C,n)))) and
A165: 0 < n ;
r = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A163, A164, PSCOMP_1:def_6;
hence ( r in R & r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s ) by A161, A165; ::_thesis: verum
end;
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
then consider v being real number such that
A166: v in R and
A167: v < (lower_bound R) + r by A157, A156, SEQ_4:def_2;
A168: v - (lower_bound R) < ((lower_bound R) + r) - (lower_bound R) by A167, XREAL_1:14;
consider n being Element of NAT such that
A169: v = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 and
A170: 0 < n by A166;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((S . m) - pp).| < r )
reconsider Sm = S . m as Element of (TOP-REAL 2) by EUCLID:22;
assume A171: n <= m ; ::_thesis: |.((S . m) - pp).| < r
then (UMP (Upper_Arc (L~ (Cage (C,m))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A170, Th27;
then Sm `2 <= v by A155, A169;
then A172: (Sm `2) - ((UMP C) `2) <= v - ((UMP C) `2) by XREAL_1:13;
reconsider SSm = Sm as Point of (TOP-REAL 2) ;
A173: SSm - p1 = (S . m) - pp ;
A174: S . m = UMP (Upper_Arc (L~ (Cage (C,m)))) by A155;
then Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then abs ((Sm `1) - ((UMP C) `1)) = 0 by A11, ABSVALUE:def_1;
then A175: |.((S . m) - pp).| <= 0 + (abs ((Sm `2) - ((UMP C) `2))) by A173, JGRAPH_1:32;
0 < (Sm `2) - ((UMP C) `2) by A170, A174, A171, Th23, XREAL_1:50;
then A176: |.((S . m) - pp).| <= (Sm `2) - ((UMP C) `2) by A175, ABSVALUE:def_1;
for r being real number st r in R holds
lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r
proof
let r be real number ; ::_thesis: ( r in R implies lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r )
assume r in R ; ::_thesis: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r
then ex n being Element of NAT st
( r = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) by A12;
hence lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r by A10, SEQ_4:def_2; ::_thesis: verum
end;
then lower_bound R = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) by A157, A156, A159, SEQ_4:def_2;
then (Sm `2) - ((UMP C) `2) < r by A152, A168, A172, XXREAL_0:2;
hence |.((S . m) - pp).| < r by A176, XXREAL_0:2; ::_thesis: verum
end;
thus A177: SS is convergent ::_thesis: ( ( for x being Element of NAT holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
proof
take UMP C ; :: according to TOPRNS_1:def_8 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((SS . b3) - (UMP C)).| ) )
let r be Real; ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| ) )
assume 0 < r ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| )
then consider n being Element of NAT such that
A178: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not r <= |.((SS . b1) - (UMP C)).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not r <= |.((SS . m) - (UMP C)).| )
assume n <= m ; ::_thesis: not r <= |.((SS . m) - (UMP C)).|
then |.((S . m) - pp).| < r by A178;
hence |.((SS . m) - (UMP C)).| < r ; ::_thesis: verum
end;
hereby ::_thesis: UMP C = lim SS
let x be Element of NAT ; ::_thesis: SS . x in (Upper_Appr C) . x
A179: (Upper_Appr C) . x = Upper_Arc (L~ (Cage (C,x))) by JORDAN19:def_1;
S . x = UMP (Upper_Arc (L~ (Cage (C,x)))) by A155;
hence SS . x in (Upper_Appr C) . x by A179, JORDAN21:30; ::_thesis: verum
end;
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
then consider n being Element of NAT such that
A180: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((SS . m) - (UMP C)).| < r )
assume n <= m ; ::_thesis: |.((SS . m) - (UMP C)).| < r
then |.((S . m) - pp).| < r by A180;
hence |.((SS . m) - (UMP C)).| < r ; ::_thesis: verum
end;
hence UMP C = lim SS by A177, TOPRNS_1:def_9; ::_thesis: verum
end;
North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3;
hence UMP C in North_Arc C by A153, KURATO_2:21; ::_thesis: verum
end;
end;
end;
theorem Th34: :: JORDAN22:34
for C being Simple_closed_curve holds LMP C in South_Arc C
proof
let C be Simple_closed_curve; ::_thesis: LMP C in South_Arc C
set w = ((W-bound C) + (E-bound C)) / 2;
set p = LMP C;
set U = { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } ;
set n0 = S-bound (L~ (Cage (C,1)));
set H = LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|);
A1: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A2: |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
{ (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } or x in the carrier of (TOP-REAL 2) )
assume x in { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex n being Element of NAT st
( x = LMP (Lower_Arc (L~ (Cage (C,n)))) & 0 < n ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider U = { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } as Subset of (TOP-REAL 2) ;
set q = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U));
set S = LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|);
A3: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
A4: |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| `2 = S-bound (L~ (Cage (C,1))) by EUCLID:52;
A5: for n being Element of NAT holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let n be Element of NAT ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
A6: (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
thus (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound (Lower_Arc (L~ (Cage (C,n))))) + (E-bound (Lower_Arc (L~ (Cage (C,n)))))) / 2 by EUCLID:52
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (Lower_Arc (L~ (Cage (C,n)))))) / 2 by JORDAN21:19
.= ((W-bound C) + (E-bound C)) / 2 by A6, JORDAN21:20 ; ::_thesis: verum
end;
A7: (LMP C) `2 >= (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 by Th24;
A8: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by JORDAN21:35;
A9: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 >= S-bound (L~ (Cage (C,1))) by JORDAN21:48;
(LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U is bounded by TOPREAL6:89;
then proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) is real-bounded by JCT_MISC:14;
then A10: proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) is bounded_above by XXREAL_2:def_11;
A11: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A12: for n being Element of NAT st 0 < n holds
(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)
proof
let n be Element of NAT ; ::_thesis: ( 0 < n implies (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) )
set f = Cage (C,n);
set s = LMP (Lower_Arc (L~ (Cage (C,n))));
assume A13: 0 < n ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)
then A14: LMP (Lower_Arc (L~ (Cage (C,n)))) in U ;
0 + 1 <= n by A13, NAT_1:13;
then ( n = 1 or n > 1 ) by XXREAL_0:1;
then A15: S-bound (L~ (Cage (C,n))) >= S-bound (L~ (Cage (C,1))) by JORDAN1A:69;
S-bound (L~ (Cage (C,n))) <= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by JORDAN21:48;
then A16: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 >= S-bound (L~ (Cage (C,1))) by A15, XXREAL_0:2;
A17: (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
(LMP C) `2 >= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A13, Th24;
then LMP (Lower_Arc (L~ (Cage (C,n)))) in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by A2, A4, A11, A16, A17, GOBOARD7:7;
then A18: LMP (Lower_Arc (L~ (Cage (C,n)))) in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U by A14, XBOOLE_0:def_4;
(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 = proj2 . (LMP (Lower_Arc (L~ (Cage (C,n))))) by PSCOMP_1:def_6;
hence (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A18, FUNCT_2:35; ::_thesis: verum
end;
then A19: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) ;
then upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 by A10, SEQ_4:def_1;
then A20: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= S-bound (L~ (Cage (C,1))) by A9, XXREAL_0:2;
A21: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A22: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) is vertical by A2, SPPOL_1:16;
A23: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by RLTOPSP1:68;
A24: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52;
percases ( LMP C <> |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| or LMP C = |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ) ;
supposeA25: LMP C <> |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: LMP C in South_Arc C
consider S9, C9 being Subset of (TopSpaceMetr (Euclid 2)) such that
A26: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) = S9 and
A27: C = C9 and
A28: dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C) = min_dist_min (S9,C9) by JORDAN1K:def_1;
A29: S9 is compact by A26, Lm4, COMPTS_1:23;
A30: C9 is compact by A27, Lm4, COMPTS_1:23;
A31: now__::_thesis:_not_(LMP_C)_`2_<=_upper_bound_(proj2_.:_((LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_(L~_(Cage_(C,1))))]|))_/\_U))
assume A32: (LMP C) `2 <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
percases ( (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) or (LMP C) `2 < upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ) by A32, XXREAL_0:1;
suppose (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
hence contradiction by A25, EUCLID:52; ::_thesis: verum
end;
suppose (LMP C) `2 < upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction
then 0 < (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((LMP C) `2) by XREAL_1:50;
then consider r being real number such that
A33: r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) and
A34: (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((LMP C) `2)) < r by A10, A19, SEQ_4:def_1;
consider t being Point of (TOP-REAL 2) such that
A35: t in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U and
A36: proj2 . t = r by A33, Lm1;
A37: t in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by A35, XBOOLE_0:def_4;
A38: (LMP C) `2 >= S-bound (L~ (Cage (C,1))) by A9, A7, XXREAL_0:2;
t `2 = r by A36, PSCOMP_1:def_6;
hence contradiction by A4, A34, A38, A37, TOPREAL1:4; ::_thesis: verum
end;
end;
end;
LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) misses C
proof
assume LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) meets C ; ::_thesis: contradiction
then consider x being set such that
A39: x in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) and
A40: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A39;
A41: x `2 >= S-bound C by A40, PSCOMP_1:24;
A42: x `1 = ((W-bound C) + (E-bound C)) / 2 by A21, A23, A22, A39, SPPOL_1:def_3;
A43: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= x `2 by A4, A24, A20, A39, TOPREAL1:4;
then (LMP C) `2 > x `2 by A31, XXREAL_0:2;
then x in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by A1, A3, A11, A41, A42, GOBOARD7:7;
then x in {(LMP C)} by A8, A40, XBOOLE_0:def_4;
hence contradiction by A31, A43, TARSKI:def_1; ::_thesis: verum
end;
then dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C) > 0 by A26, A27, A28, A29, A30, JGRAPH_1:38;
then (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2 > 0 by XREAL_1:215;
then consider k being Element of NAT such that
A44: 1 < k and
A45: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2 and
A46: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < (dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2 by GOBRD14:11;
set f = Cage (C,k);
set G = Gauge (C,k);
set s = LMP (Lower_Arc (L~ (Cage (C,k))));
A47: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 >= S-bound (L~ (Cage (C,k))) by JORDAN21:48;
A48: (dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * ((1 + 1),1)))) + (dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,(1 + 1))))) < ((dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2) + ((dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2) by A45, A46, XREAL_1:8;
S-bound (L~ (Cage (C,k))) >= S-bound (L~ (Cage (C,1))) by A44, JORDAN1A:69;
then A49: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 >= S-bound (L~ (Cage (C,1))) by A47, XXREAL_0:2;
(LMP (Lower_Arc (L~ (Cage (C,k))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12, A44;
then A50: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A10, SEQ_4:def_1;
[1,(1 + 1)] in Indices (Gauge (C,k)) by Th6;
then A51: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by Th5, GOBRD14:9;
[(1 + 1),1] in Indices (Gauge (C,k)) by Th7;
then A52: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by Th5, GOBRD14:10;
A53: LMP (Lower_Arc (L~ (Cage (C,k)))) in Lower_Arc (L~ (Cage (C,k))) by JORDAN21:31;
Lower_Arc (L~ (Cage (C,k))) c= L~ (Cage (C,k)) by JORDAN6:61;
then consider i being Element of NAT such that
A54: 1 <= i and
A55: i + 1 <= len (Cage (C,k)) and
A56: LMP (Lower_Arc (L~ (Cage (C,k)))) in LSeg ((Cage (C,k)),i) by A53, SPPOL_2:13;
A57: Cage (C,k) is_sequence_on Gauge (C,k) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A58: [i1,j1] in Indices (Gauge (C,k)) and
A59: (Cage (C,k)) /. i = (Gauge (C,k)) * (i1,j1) and
A60: [i2,j2] in Indices (Gauge (C,k)) and
A61: (Cage (C,k)) /. (i + 1) = (Gauge (C,k)) * (i2,j2) and
A62: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A54, A55, JORDAN8:3;
A63: 1 <= i1 by A58, MATRIX_1:38;
right_cell ((Cage (C,k)),i,(Gauge (C,k))) meets C by A54, A55, JORDAN9:31;
then consider c being set such that
A64: c in right_cell ((Cage (C,k)),i,(Gauge (C,k))) and
A65: c in C by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A65;
reconsider s9 = LMP (Lower_Arc (L~ (Cage (C,k)))), c9 = c as Point of (Euclid 2) by EUCLID:67;
(LMP (Lower_Arc (L~ (Cage (C,k))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then LMP (Lower_Arc (L~ (Cage (C,k)))) in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by A2, A4, A21, A24, A49, A50, GOBOARD7:7;
then A66: min_dist_min (S9,C9) <= dist (s9,c9) by A26, A27, A29, A30, A65, WEIERSTR:34;
A67: dist (s9,c9) = dist ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) by TOPREAL6:def_1;
A68: 1 <= j2 by A60, MATRIX_1:38;
(left_cell ((Cage (C,k)),i,(Gauge (C,k)))) /\ (right_cell ((Cage (C,k)),i,(Gauge (C,k)))) = LSeg ((Cage (C,k)),i) by A54, A55, A57, GOBRD13:29;
then A69: LMP (Lower_Arc (L~ (Cage (C,k)))) in right_cell ((Cage (C,k)),i,(Gauge (C,k))) by A56, XBOOLE_0:def_4;
A70: j2 <= width (Gauge (C,k)) by A60, MATRIX_1:38;
A71: (j2 + 1) + 1 <> j2 ;
A72: 1 <= i2 by A60, MATRIX_1:38;
A73: j1 <= width (Gauge (C,k)) by A58, MATRIX_1:38;
A74: 1 <= j1 + 1 by NAT_1:11;
A75: i1 + 1 <> i1 + 0 ;
A76: i1 <= len (Gauge (C,k)) by A58, MATRIX_1:38;
A77: i2 <= len (Gauge (C,k)) by A60, MATRIX_1:38;
A78: (i2 + 1) + 1 <> i2 ;
A79: 1 <= j1 by A58, MATRIX_1:38;
A80: 1 <= i1 + 1 by NAT_1:11;
now__::_thesis:_contradiction
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A62;
supposeA81: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: contradiction
then A82: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * (i1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A60, GOBRD14:9;
A83: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * (i1,(j1 + 1)))) = (((Gauge (C,k)) * (i1,(j1 + 1))) `2) - (((Gauge (C,k)) * (i1,j1)) `2) by A58, A60, A81, GOBRD14:6;
i1 < len (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A81, JORDAN10:1;
then A84: i1 + 1 <= len (Gauge (C,k)) by NAT_1:13;
then A85: [(i1 + 1),j1] in Indices (Gauge (C,k)) by A79, A80, A73, MATRIX_1:36;
then A86: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * ((i1 + 1),j1))) = (((Gauge (C,k)) * ((i1 + 1),j1)) `1) - (((Gauge (C,k)) * (i1,j1)) `1) by A58, GOBRD14:5;
A87: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * ((i1 + 1),j1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A85, GOBRD14:10;
A88: j1 + 1 <= width (Gauge (C,k)) by A60, A81, MATRIX_1:38;
A89: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,j1) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A81, GOBRD13:def_2;
then A90: c `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A64, A63, A79, A88, A84, JORDAN9:17;
A91: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A92: ((Gauge (C,k)) * (i1,j1)) `2 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A93: (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A94: ((Gauge (C,k)) * (i1,j1)) `1 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A95: c `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
A96: ((Gauge (C,k)) * (i1,j1)) `2 <= c `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
((Gauge (C,k)) * (i1,j1)) `1 <= c `1 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
then dist ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i1 + 1),j1)) `1) - (((Gauge (C,k)) * (i1,j1)) `1)) + ((((Gauge (C,k)) * (i1,(j1 + 1))) `2) - (((Gauge (C,k)) * (i1,j1)) `2)) by A90, A96, A95, A94, A93, A92, A91, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A86, A83, A82, A87, XXREAL_0:2; ::_thesis: verum
end;
supposeA97: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction
then 1 < j1 by A54, A55, A58, A59, A60, A61, JORDAN10:3;
then A98: 1 <= j1 -' 1 by NAT_D:49;
then A99: (j1 -' 1) + 1 = j1 by NAT_D:43;
A100: j1 -' 1 <= width (Gauge (C,k)) by A73, NAT_D:44;
then A101: [i1,(j1 -' 1)] in Indices (Gauge (C,k)) by A63, A76, A98, MATRIX_1:36;
then A102: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * (i1,((j1 -' 1) + 1)))) = (((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `2) by A58, A99, GOBRD14:6;
A103: [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,k)) by A72, A77, A97, A98, A100, MATRIX_1:36;
then A104: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * ((i1 + 1),(j1 -' 1)))) = (((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `1) by A101, GOBRD14:5;
A105: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * (i1,((j1 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A99, A101, GOBRD14:9;
A106: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * ((i1 + 1),(j1 -' 1)))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A101, A103, GOBRD14:10;
A107: i1 + 1 <= len (Gauge (C,k)) by A60, A97, MATRIX_1:38;
A108: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,(j1 -' 1)) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A97, GOBRD13:def_2;
then A109: c `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A64, A63, A73, A107, A98, A99, JORDAN9:17;
A110: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A111: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A112: (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A113: ((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A114: c `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A115: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= c `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= c `1 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
then dist ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `1)) + ((((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2) - (((Gauge (C,k)) * (i1,(j1 -' 1))) `2)) by A109, A115, A114, A113, A112, A111, A110, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A104, A102, A105, A106, XXREAL_0:2; ::_thesis: verum
end;
supposeA116: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction
then A117: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * ((i2 + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A60, GOBRD14:10;
A118: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * ((i2 + 1),j2))) = (((Gauge (C,k)) * ((i2 + 1),j2)) `1) - (((Gauge (C,k)) * (i2,j2)) `1) by A58, A60, A116, GOBRD14:5;
A119: i2 + 1 <= len (Gauge (C,k)) by A58, A116, MATRIX_1:38;
j1 < width (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A116, JORDAN10:4;
then A120: j1 + 1 <= width (Gauge (C,k)) by NAT_1:13;
then A121: [i2,(j2 + 1)] in Indices (Gauge (C,k)) by A72, A74, A77, A116, MATRIX_1:36;
then A122: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * (i2,(j2 + 1)))) = (((Gauge (C,k)) * (i2,(j2 + 1))) `2) - (((Gauge (C,k)) * (i2,j2)) `2) by A60, GOBRD14:6;
A123: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i2,j2) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A116, GOBRD13:def_2;
then A124: c `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A64, A79, A72, A116, A119, A120, JORDAN9:17;
A125: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A126: ((Gauge (C,k)) * (i2,j2)) `2 <= c `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A127: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * (i2,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A60, A121, GOBRD14:9;
A128: ((Gauge (C,k)) * (i2,j2)) `2 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A129: (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A130: ((Gauge (C,k)) * (i2,j2)) `1 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A131: c `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
((Gauge (C,k)) * (i2,j2)) `1 <= c `1 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
then dist ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * ((i2 + 1),j2)) `1) - (((Gauge (C,k)) * (i2,j2)) `1)) + ((((Gauge (C,k)) * (i2,(j2 + 1))) `2) - (((Gauge (C,k)) * (i2,j2)) `2)) by A124, A126, A131, A130, A129, A128, A125, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A118, A122, A127, A117, XXREAL_0:2; ::_thesis: verum
end;
supposeA132: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: contradiction
then 1 < i1 by A54, A55, A58, A59, A60, A61, JORDAN10:2;
then A133: 1 <= i1 -' 1 by NAT_D:49;
A134: i1 -' 1 <= len (Gauge (C,k)) by A76, NAT_D:44;
then A135: [(i1 -' 1),j2] in Indices (Gauge (C,k)) by A68, A70, A133, MATRIX_1:36;
A136: [(i1 -' 1),(j2 + 1)] in Indices (Gauge (C,k)) by A79, A73, A132, A133, A134, MATRIX_1:36;
then A137: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * ((i1 -' 1),(j2 + 1)))) = (((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `2) by A135, GOBRD14:6;
A138: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * ((i1 -' 1),(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A135, A136, GOBRD14:9;
A139: j2 + 1 <= width (Gauge (C,k)) by A58, A132, MATRIX_1:38;
A140: (i1 -' 1) + 1 = i1 by A133, NAT_D:43;
then A141: [((i1 -' 1) + 1),j2] in Indices (Gauge (C,k)) by A63, A68, A76, A70, MATRIX_1:36;
then A142: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * (((i1 -' 1) + 1),j2))) = (((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `1) by A135, GOBRD14:5;
A143: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),(i1 -' 1),j2) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A132, GOBRD13:def_2;
then A144: c `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A64, A68, A76, A139, A133, A140, JORDAN9:17;
A145: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A146: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A147: (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A148: ((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A149: c `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A150: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= c `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A151: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * (((i1 -' 1) + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A135, A141, GOBRD14:10;
((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= c `1 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
then dist ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) <= ((((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `1)) + ((((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2) - (((Gauge (C,k)) * ((i1 -' 1),j2)) `2)) by A144, A150, A149, A148, A147, A146, A145, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A142, A137, A138, A151, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence LMP C in South_Arc C ; ::_thesis: verum
end;
suppose LMP C = |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: LMP C in South_Arc C
then A152: (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52;
A153: ex S being Real_Sequence of 2 st
( S is convergent & ( for x being Element of NAT holds S . x in (Lower_Appr C) . x ) & LMP C = lim S )
proof
set R = { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } ;
{ ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } or x in REAL )
assume x in { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } ; ::_thesis: x in REAL
then ex n being Element of NAT st
( x = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider R = { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } as Subset of REAL ;
deffunc H1( Element of NAT ) -> Element of the carrier of (TOP-REAL 2) = LMP (Lower_Arc (L~ (Cage (C,$1))));
reconsider pp = LMP C as Element of REAL 2 by EUCLID:22;
A154: for x being Element of NAT holds H1(x) is Element of REAL 2 by EUCLID:22;
consider S being Function of NAT,(REAL 2) such that
A155: for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_9(A154);
the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
then reconsider SS = S as Real_Sequence of 2 ;
take SS ; ::_thesis: ( SS is convergent & ( for x being Element of NAT holds SS . x in (Lower_Appr C) . x ) & LMP C = lim SS )
A156: R is bounded_above
proof
take upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; :: according to XXREAL_2:def_10 ::_thesis: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) is UpperBound of R
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in R or r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) )
assume r in R ; ::_thesis: r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))
then ex n being Element of NAT st
( r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12;
hence r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by A10, SEQ_4:def_1; ::_thesis: verum
end;
A157: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 in R ;
A158: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
proof
A159: for s being real number st 0 < s holds
ex r being real number st
( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r )
then consider r being real number such that
A160: r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) and
A161: (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r by A10, A19, SEQ_4:def_1;
take r ; ::_thesis: ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r )
consider x being Point of (TOP-REAL 2) such that
A162: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U and
A163: proj2 . x = r by A160, Lm1;
x in U by A162, XBOOLE_0:def_4;
then consider n being Element of NAT such that
A164: x = LMP (Lower_Arc (L~ (Cage (C,n)))) and
A165: 0 < n ;
r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A163, A164, PSCOMP_1:def_6;
hence ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) by A161, A165; ::_thesis: verum
end;
reconsider p1 = LMP C as Element of (TOP-REAL 2) ;
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
then consider v being real number such that
A166: v in R and
A167: (upper_bound R) - r < v by A157, A156, SEQ_4:def_1;
consider n being Element of NAT such that
A168: v = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 and
A169: 0 < n by A166;
((upper_bound R) - r) + r < v + r by A167, XREAL_1:6;
then A170: (upper_bound R) - v < (v + r) - v by XREAL_1:14;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((S . m) - pp).| < r )
reconsider Sm = S . m as Point of (TOP-REAL 2) by EUCLID:22;
assume A171: n <= m ; ::_thesis: |.((S . m) - pp).| < r
then (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,m))))) `2 by A169, Th28;
then Sm `2 >= v by A155, A168;
then A172: ((LMP C) `2) - (Sm `2) <= ((LMP C) `2) - v by XREAL_1:13;
reconsider SSm = Sm as Point of (TOP-REAL 2) ;
A173: SSm - p1 = (S . m) - pp ;
A174: S . m = LMP (Lower_Arc (L~ (Cage (C,m)))) by A155;
then Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then abs ((Sm `1) - ((LMP C) `1)) = 0 by A11, ABSVALUE:def_1;
then A175: |.((S . m) - pp).| <= 0 + (abs ((Sm `2) - ((LMP C) `2))) by A173, JGRAPH_1:32;
0 > (Sm `2) - ((LMP C) `2) by A169, A174, A171, Th24, XREAL_1:49;
then A176: |.((S . m) - pp).| <= - ((Sm `2) - ((LMP C) `2)) by A175, ABSVALUE:def_1;
for r being real number st r in R holds
upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r
proof
let r be real number ; ::_thesis: ( r in R implies upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r )
assume r in R ; ::_thesis: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r
then ex n being Element of NAT st
( r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12;
hence upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r by A10, SEQ_4:def_1; ::_thesis: verum
end;
then upper_bound R = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by A157, A156, A159, SEQ_4:def_1;
then ((LMP C) `2) - (Sm `2) < r by A152, A170, A172, XXREAL_0:2;
hence |.((S . m) - pp).| < r by A176, XXREAL_0:2; ::_thesis: verum
end;
thus A177: SS is convergent ::_thesis: ( ( for x being Element of NAT holds SS . x in (Lower_Appr C) . x ) & LMP C = lim SS )
proof
take LMP C ; :: according to TOPRNS_1:def_8 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((SS . b3) - (LMP C)).| ) )
let r be Real; ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (LMP C)).| ) )
assume 0 < r ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (LMP C)).| )
then consider n being Element of NAT such that
A178: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not r <= |.((SS . b1) - (LMP C)).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not r <= |.((SS . m) - (LMP C)).| )
assume n <= m ; ::_thesis: not r <= |.((SS . m) - (LMP C)).|
then |.((S . m) - pp).| < r by A178;
hence |.((SS . m) - (LMP C)).| < r ; ::_thesis: verum
end;
hereby ::_thesis: LMP C = lim SS
let x be Element of NAT ; ::_thesis: SS . x in (Lower_Appr C) . x
A179: (Lower_Appr C) . x = Lower_Arc (L~ (Cage (C,x))) by JORDAN19:def_2;
S . x = LMP (Lower_Arc (L~ (Cage (C,x)))) by A155;
hence SS . x in (Lower_Appr C) . x by A179, JORDAN21:31; ::_thesis: verum
end;
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (LMP C)).| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (LMP C)).| < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (LMP C)).| < r
then consider n being Element of NAT such that
A180: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((SS . m) - (LMP C)).| < r
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((SS . m) - (LMP C)).| < r )
assume n <= m ; ::_thesis: |.((SS . m) - (LMP C)).| < r
then |.((S . m) - pp).| < r by A180;
hence |.((SS . m) - (LMP C)).| < r ; ::_thesis: verum
end;
hence LMP C = lim SS by A177, TOPRNS_1:def_9; ::_thesis: verum
end;
South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4;
hence LMP C in South_Arc C by A153, KURATO_2:21; ::_thesis: verum
end;
end;
end;
theorem Th35: :: JORDAN22:35
for C being Simple_closed_curve holds North_Arc C c= C
proof
let C be Simple_closed_curve; ::_thesis: North_Arc C c= C
A1: North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3;
reconsider OO = BDD C as Subset of (TopSpaceMetr (Euclid 2)) by Lm4;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in North_Arc C or x in C )
assume A2: x in North_Arc C ; ::_thesis: x in C
assume A3: not x in C ; ::_thesis: contradiction
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x in C ` by A3, SUBSET_1:29;
A5: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27;
reconsider e = x as Point of (Euclid 2) by EUCLID:67;
percases ( x in BDD C or x in UBD C ) by A4, A5, XBOOLE_0:def_3;
supposeA6: x in BDD C ; ::_thesis: contradiction
OO is open by Lm4, PRE_TOPC:30;
then consider r being real number such that
A7: r > 0 and
A8: Ball (e,r) c= BDD C by A6, TOPMETR:15;
consider k being Element of NAT such that
A9: for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (e,r) by A2, A1, A7, KURATO_2:14;
A10: Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61;
A11: (Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_1;
A12: k + 0 < k + 1 by XREAL_1:8;
Ball (e,r) misses L~ (Cage (C,(k + 1))) by A8, JORDAN10:19, XBOOLE_1:63;
hence contradiction by A9, A12, A11, A10, XBOOLE_1:63; ::_thesis: verum
end;
supposeA13: x in UBD C ; ::_thesis: contradiction
union (UBD-Family C) = UBD C by JORDAN10:14;
then consider A being set such that
A14: x in A and
A15: A in UBD-Family C by A13, TARSKI:def_4;
UBD-Family C = { (UBD (L~ (Cage (C,m)))) where m is Element of NAT : verum } by JORDAN10:def_1;
then consider m being Element of NAT such that
A16: A = UBD (L~ (Cage (C,m))) by A15;
reconsider OO = LeftComp (Cage (C,m)) as Subset of (TopSpaceMetr (Euclid 2)) by Lm4;
A17: OO is open by Lm4, PRE_TOPC:30;
x in LeftComp (Cage (C,m)) by A14, A16, GOBRD14:36;
then consider r being real number such that
A18: r > 0 and
A19: Ball (e,r) c= LeftComp (Cage (C,m)) by A17, TOPMETR:15;
consider k being Element of NAT such that
A20: for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball (e,r) by A2, A1, A18, KURATO_2:14;
thus contradiction ::_thesis: verum
proof
percases ( m > k or m <= k ) ;
supposeA21: m > k ; ::_thesis: contradiction
A22: (Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1;
A23: Upper_Arc (L~ (Cage (C,m))) c= L~ (Cage (C,m)) by JORDAN6:61;
Ball (e,r) misses L~ (Cage (C,m)) by A19, SPRECT_3:26, XBOOLE_1:63;
hence contradiction by A20, A21, A22, A23, XBOOLE_1:63; ::_thesis: verum
end;
suppose m <= k ; ::_thesis: contradiction
then LeftComp (Cage (C,m)) c= LeftComp (Cage (C,k)) by JORDAN1H:47;
then A24: Ball (e,r) c= LeftComp (Cage (C,k)) by A19, XBOOLE_1:1;
A25: k + 0 < k + 1 by XREAL_1:8;
then LeftComp (Cage (C,k)) c= LeftComp (Cage (C,(k + 1))) by JORDAN1H:47;
then Ball (e,r) c= LeftComp (Cage (C,(k + 1))) by A24, XBOOLE_1:1;
then A26: Ball (e,r) misses L~ (Cage (C,(k + 1))) by SPRECT_3:26, XBOOLE_1:63;
A27: Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61;
(Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_1;
hence contradiction by A20, A25, A26, A27, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;
end;
end;
end;
theorem Th36: :: JORDAN22:36
for C being Simple_closed_curve holds South_Arc C c= C
proof
let C be Simple_closed_curve; ::_thesis: South_Arc C c= C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in South_Arc C or x in C )
assume A1: x in South_Arc C ; ::_thesis: x in C
assume A2: not x in C ; ::_thesis: contradiction
reconsider x = x as Point of (TOP-REAL 2) by A1;
A3: x in C ` by A2, SUBSET_1:29;
reconsider e = x as Point of (Euclid 2) by EUCLID:67;
A4: South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4;
A5: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27;
percases ( x in BDD C or x in UBD C ) by A3, A5, XBOOLE_0:def_3;
supposeA6: x in BDD C ; ::_thesis: contradiction
reconsider OO = BDD C as Subset of (TopSpaceMetr (Euclid 2)) by Lm4;
OO is open by Lm4, PRE_TOPC:30;
then consider r being real number such that
A7: r > 0 and
A8: Ball (e,r) c= BDD C by A6, TOPMETR:15;
consider k being Element of NAT such that
A9: for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (e,r) by A1, A4, A7, KURATO_2:14;
A10: Lower_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61;
A11: (Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_2;
A12: k + 0 < k + 1 by XREAL_1:8;
Ball (e,r) misses L~ (Cage (C,(k + 1))) by A8, JORDAN10:19, XBOOLE_1:63;
hence contradiction by A9, A12, A11, A10, XBOOLE_1:63; ::_thesis: verum
end;
supposeA13: x in UBD C ; ::_thesis: contradiction
union (UBD-Family C) = UBD C by JORDAN10:14;
then consider A being set such that
A14: x in A and
A15: A in UBD-Family C by A13, TARSKI:def_4;
UBD-Family C = { (UBD (L~ (Cage (C,m)))) where m is Element of NAT : verum } by JORDAN10:def_1;
then consider m being Element of NAT such that
A16: A = UBD (L~ (Cage (C,m))) by A15;
reconsider OO = LeftComp (Cage (C,m)) as Subset of (TopSpaceMetr (Euclid 2)) by Lm4;
A17: OO is open by Lm4, PRE_TOPC:30;
x in LeftComp (Cage (C,m)) by A14, A16, GOBRD14:36;
then consider r being real number such that
A18: r > 0 and
A19: Ball (e,r) c= LeftComp (Cage (C,m)) by A17, TOPMETR:15;
consider k being Element of NAT such that
A20: for m being Element of NAT st m > k holds
(Lower_Appr C) . m meets Ball (e,r) by A1, A4, A18, KURATO_2:14;
thus contradiction ::_thesis: verum
proof
percases ( m > k or m <= k ) ;
supposeA21: m > k ; ::_thesis: contradiction
A22: (Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2;
A23: Lower_Arc (L~ (Cage (C,m))) c= L~ (Cage (C,m)) by JORDAN6:61;
Ball (e,r) misses L~ (Cage (C,m)) by A19, SPRECT_3:26, XBOOLE_1:63;
hence contradiction by A20, A21, A22, A23, XBOOLE_1:63; ::_thesis: verum
end;
suppose m <= k ; ::_thesis: contradiction
then LeftComp (Cage (C,m)) c= LeftComp (Cage (C,k)) by JORDAN1H:47;
then A24: Ball (e,r) c= LeftComp (Cage (C,k)) by A19, XBOOLE_1:1;
A25: k + 0 < k + 1 by XREAL_1:8;
then LeftComp (Cage (C,k)) c= LeftComp (Cage (C,(k + 1))) by JORDAN1H:47;
then Ball (e,r) c= LeftComp (Cage (C,(k + 1))) by A24, XBOOLE_1:1;
then A26: Ball (e,r) misses L~ (Cage (C,(k + 1))) by SPRECT_3:26, XBOOLE_1:63;
A27: Lower_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61;
(Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_2;
hence contradiction by A20, A25, A26, A27, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;
end;
end;
end;
theorem :: JORDAN22:37
for C being Simple_closed_curve holds
( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) )
proof
let C be Simple_closed_curve; ::_thesis: ( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) )
A1: LMP C in South_Arc C by Th34;
A2: North_Arc C c= C by Th35;
A3: UMP C in North_Arc C by Th33;
A4: South_Arc C c= C by Th36;
now__::_thesis:_(_(_LE_LMP_C,_UMP_C,C_&_UMP_C_in_Lower_Arc_C_&_LMP_C_in_Upper_Arc_C_)_or_(_LE_UMP_C,_LMP_C,C_&_LMP_C_in_Lower_Arc_C_&_UMP_C_in_Upper_Arc_C_)_)
percases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A4, A1, A2, A3, JORDAN16:7;
case LE LMP C, UMP C,C ; ::_thesis: ( UMP C in Lower_Arc C & LMP C in Upper_Arc C )
then ( ( LMP C in Upper_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def_10;
hence ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) by JORDAN21:49, JORDAN21:50; ::_thesis: verum
end;
case LE UMP C, LMP C,C ; ::_thesis: ( LMP C in Lower_Arc C & UMP C in Upper_Arc C )
then ( ( UMP C in Upper_Arc C & LMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def_10;
hence ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) by JORDAN21:49, JORDAN21:50; ::_thesis: verum
end;
end;
end;
hence ( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) ) ; ::_thesis: verum
end;
theorem :: JORDAN22:38
for C being Simple_closed_curve holds W-bound C = W-bound (North_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (North_Arc C)
A1: W-min C in North_Arc C by Th29;
North_Arc C c= C by Th35;
hence W-bound C = W-bound (North_Arc C) by A1, JORDAN1J:65; ::_thesis: verum
end;
theorem :: JORDAN22:39
for C being Simple_closed_curve holds E-bound C = E-bound (North_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (North_Arc C)
A1: E-max C in North_Arc C by Th30;
North_Arc C c= C by Th35;
hence E-bound C = E-bound (North_Arc C) by A1, JORDAN1J:66; ::_thesis: verum
end;
theorem :: JORDAN22:40
for C being Simple_closed_curve holds W-bound C = W-bound (South_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (South_Arc C)
A1: W-min C in South_Arc C by Th31;
South_Arc C c= C by Th36;
hence W-bound C = W-bound (South_Arc C) by A1, JORDAN1J:65; ::_thesis: verum
end;
theorem :: JORDAN22:41
for C being Simple_closed_curve holds E-bound C = E-bound (South_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (South_Arc C)
A1: E-max C in South_Arc C by Th32;
South_Arc C c= C by Th36;
hence E-bound C = E-bound (South_Arc C) by A1, JORDAN1J:66; ::_thesis: verum
end;