:: On Some Points of a Simple Closed Curve. {P}art {II}
:: by Artur Korni{\l}owicz and Adam Grabowski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TOPREAL2, SUBSET_1, EUCLID, RELAT_1, PRE_TOPC, FUNCT_1,
STRUCT_0, JORDAN19, TARSKI, GOBOARD9, JORDAN9, CARD_1, JORDAN6, TOPREAL1,
RELAT_2, PSCOMP_1, RCOMP_1, KURATO_2, XBOOLE_0, XXREAL_0, FINSEQ_1,
JORDAN8, MATRIX_1, TREES_1, SPPOL_1, ARYTM_3, METRIC_1, ARYTM_1, NEWTON,
ORDINAL2, RLTOPSP1, JORDAN1A, MCART_1, XXREAL_2, SEQ_4, GOBOARD2,
JORDAN21, JORDAN2C, GOBOARD1, FINSEQ_6, GOBOARD5, PARTFUN1, PCOMPS_1,
WEIERSTR, SEQ_1, SEQ_2, REAL_1, COMPLEX1, JORDAN10, JORDAN3, CONVEX1,
NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, RELSET_1, PARTFUN1,
FUNCT_2, XXREAL_2, SEQ_4, NEWTON, FINSEQ_1, MATRIX_0, DOMAIN_1, STRUCT_0,
PRE_TOPC, COMPTS_1, FINSEQ_6, CONNSP_1, METRIC_1, PCOMPS_1, PSCOMP_1,
RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD2,
WEIERSTR, SPPOL_1, GOBOARD5, TOPRNS_1, JORDAN2C, JORDAN6, GOBOARD9,
JORDAN8, JORDAN9, GOBRD13, TOPREAL6, JORDAN10, JORDAN1K, JORDAN1A,
KURATO_2, JORDAN19, JORDAN21;
constructors REAL_1, RCOMP_1, NEWTON, BINARITH, CONNSP_1, MONOID_0, TOPRNS_1,
TOPREAL4, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C,
TOPREAL6, JORDAN1K, JORDAN21, JORDAN8, GOBRD13, JORDAN9, JORDAN10,
JORDAN1A, KURATO_2, JORDAN19, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, JORDAN11;
registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2,
GOBOARD2, SPPOL_2, TOPREAL5, SPRECT_2, JORDAN6, SPRECT_3, JORDAN2C,
REVROT_1, TOPREAL6, JORDAN21, JORDAN8, JORDAN10, VALUED_0, FUNCT_1,
ORDINAL1, RLTOPSP1, JORDAN1, XCMPLX_0, NEWTON;
requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
definitions TARSKI, TOPRNS_1, XXREAL_2;
equalities JORDAN6, JORDAN21;
expansions TARSKI, JORDAN6, XXREAL_2;
theorems XBOOLE_1, JORDAN1A, JORDAN6, XBOOLE_0, JORDAN1K, EUCLID, TOPREAL1,
TARSKI, JORDAN16, METRIC_1, SPRECT_3, TOPMETR, JORDAN7, GOBRD14,
JORDAN1I, INT_1, GOBOARD5, FINSEQ_6, REVROT_1, SPRECT_2, GOBOARD7,
JGRAPH_1, JORDAN1H, JORDAN9, GOBRD13, NAT_1, JORDAN8, SUBSET_1, JORDAN2C,
JORDAN10, PSCOMP_1, SPPOL_2, SPPOL_1, SEQ_4, FUNCT_2, WEIERSTR, JORDAN1G,
TOPRNS_1, ABSVALUE, JORDAN19, KURATO_2, JORDAN21, XREAL_1, JORDAN1J,
JORDAN1B, RELAT_1, JORDAN5D, TOPREAL3, JORDAN1F, NEWTON, SPRECT_1,
XXREAL_0, PEPIN, TOPREAL6, JCT_MISC, MATRIX_0, XXREAL_2, NAT_D, XREAL_0,
COMPTS_1, PRE_TOPC, RLTOPSP1, ORDINAL1;
schemes FUNCT_2;
begin :: Properties of the Approximations
reserve C for Simple_closed_curve,
i for Nat;
Lm1: for r being Real, X being Subset of TOP-REAL 2 st r in proj2.:X ex
x being Point of TOP-REAL 2 st x in X & proj2.x = r
proof
let r be Real, X be Subset of TOP-REAL 2;
assume r in proj2.:X;
then
ex x being object st x in the carrier of TOP-REAL 2 & x in X & proj2.x = r
by FUNCT_2:64;
hence thesis;
end;
theorem Th1:
(Upper_Appr C).i c= Cl RightComp Cage(C,0)
proof
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 thesis by A1,A2;
end;
theorem Th2:
(Lower_Appr C).i c= Cl RightComp Cage(C,0)
proof
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 thesis by A1,A2;
end;
registration
let C be Simple_closed_curve;
cluster Upper_Arc C -> connected;
coherence
proof
Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
hence thesis by JORDAN6:10;
end;
cluster Lower_Arc C -> connected;
coherence
proof
Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
hence thesis by JORDAN6:10;
end;
end;
theorem
(Upper_Appr C).i is compact connected
proof
Upper_Arc L~Cage(C,i) is compact;
hence (Upper_Appr C).i is compact by JORDAN19:def 1;
Upper_Arc L~Cage(C,i) is connected;
hence thesis by JORDAN19:def 1;
end;
theorem
(Lower_Appr C).i is compact connected
proof
Lower_Arc L~Cage(C,i) is compact;
hence (Lower_Appr C).i is compact by JORDAN19:def 2;
Lower_Arc L~Cage(C,i) is connected;
hence thesis by JORDAN19:def 2;
end;
registration
let C be Simple_closed_curve;
cluster North_Arc C -> compact;
coherence
proof
for i being 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 thesis by JORDAN19:def 3;
end;
cluster South_Arc C -> compact;
coherence
proof
for i being 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 thesis by JORDAN19:def 4;
end;
end;
:: Moved from JORDAN21, AK, 22.02.2006
reserve R for non empty Subset of TOP-REAL 2,
j, k, m, n for Nat;
Lm2: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
Lm3: 1 <= len Gauge(R,n)
proof
4 <= len Gauge(R,n) by JORDAN8:10;
hence thesis by XXREAL_0:2;
end;
theorem Th5:
[1,1] in Indices Gauge(R,n)
proof
A1: len Gauge(R,n) = width Gauge(R,n) by JORDAN8:def 1;
1 <= len Gauge(R,n) by Lm3;
hence thesis by A1,MATRIX_0:30;
end;
theorem Th6:
[1,2] in Indices Gauge(R,n)
proof
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 thesis by A1,A3,MATRIX_0:30;
end;
theorem Th7:
[2,1] in Indices Gauge(R,n)
proof
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 thesis by A1,A3,MATRIX_0:30;
end;
theorem Th8:
for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds 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))
proof
let C be non vertical non horizontal compact Subset of TOP-REAL 2;
assume that
A1: m > k and
A2: [i,j] in Indices Gauge(C,k) and
A3: [i,j+1] in Indices Gauge(C,k);
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_0:32;
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_0:32;
then
A9: i <= len Gauge(C,m) by A4,XXREAL_0:2;
j+1 <= width Gauge(C,k) by A3,MATRIX_0:32;
then
A10: j+1 <= width Gauge(C,m) by A6,A5,A4,XXREAL_0:2;
A11: 1 <= i by A2,MATRIX_0:32;
1 <= j+1 by NAT_1:11;
then
A12: [i,j+1] in Indices Gauge(C,m) by A11,A9,A10,MATRIX_0:30;
1 <= j by A2,MATRIX_0:32;
then [i,j] in Indices Gauge(C,m) by A11,A9,A7,MATRIX_0:30;
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 thesis by A1,A13,A14,A8,PEPIN:66,XREAL_1:76;
end;
theorem Th9:
for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds 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))
proof
let C be non vertical non horizontal compact Subset of TOP-REAL 2;
assume
A1: m > k;
[1,1+1] in Indices Gauge(C,k) by Th6;
hence thesis by A1,Th5,Th8;
end;
theorem Th10:
for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds 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))
proof
let C be non vertical non horizontal compact Subset of TOP-REAL 2;
assume that
A1: m > k and
A2: [i,j] in Indices Gauge(C,k) and
A3: [i+1,j] in Indices Gauge(C,k);
A4: len Gauge(C,k) < len Gauge(C,m) by A1,JORDAN1A:29;
i <= len Gauge(C,k) by A2,MATRIX_0:32;
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_0:32;
then
A9: j <= width Gauge(C,m) by A8,A7,A4,XXREAL_0:2;
i+1 <= len Gauge(C,k) by A3,MATRIX_0:32;
then
A10: i+1 <= len Gauge(C,m) by A4,XXREAL_0:2;
A11: 1 <= j by A2,MATRIX_0:32;
1 <= i+1 by NAT_1:11;
then
A12: [i+1,j] in Indices Gauge(C,m) by A11,A9,A10,MATRIX_0:30;
1 <= i by A2,MATRIX_0:32;
then [i,j] in Indices Gauge(C,m) by A11,A5,A9,MATRIX_0:30;
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 thesis by A1,A13,A14,A6,PEPIN:66,XREAL_1:76;
end;
theorem Th11:
for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds 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))
proof
let C be non vertical non horizontal compact Subset of TOP-REAL 2;
assume
A1: m > k;
[1+1,1] in Indices Gauge(C,k) by Th7;
hence thesis by A1,Th5,Th10;
end;
theorem
for r, t being Real holds r > 0 & t > 0 implies ex n being
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 r, t be Real;
assume that
A1: r > 0 and
A2: t > 0;
consider n being 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;
per cases;
suppose
A5: i < n;
take n;
thus thesis by A3,A4,A5;
end;
suppose
A6: i >= n;
take i+1;
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;
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 thesis by A3,A4,A11,XXREAL_0:2;
end;
end;
theorem Th13:
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)))
proof
set f = Cage(C,n), G = Gauge(C,n), c = Center G;
set Y = proj2.:(L~f /\ Vertical_Line ((E-bound L~f + W-bound L~f) / 2));
set X = proj2.:(L~f /\ LSeg(G*(c,1),G*(c,len G)));
A1: len G = width G by JORDAN8:def 1;
A2: 1 <= len G by Lm3;
assume 0 < n;
then
A3: G*(c,1)`1 = (W-bound C + E-bound C) / 2 by A1,A2,JORDAN1G:35
.= (W-bound L~f + E-bound L~f) / 2 by JORDAN1G:33;
then
A4: G*(c,1) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2);
A5: Y is bounded_above by JORDAN21:13;
LSeg(G*(c,1),G*(c,len G)) meets Upper_Arc L~f by JORDAN1B:31;
then LSeg(G*(c,1),G*(c,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
then
A6: L~f /\ LSeg(G*(c,1),G*(c,len G)) is non empty by XBOOLE_0:def 7;
then
A7: X is non empty by Lm2,RELAT_1:119;
A8: c <= len G by JORDAN1B:13;
1 <= c by JORDAN1B:11;
then
A9: G*(c,1)`1 = G*(c,len G)`1 by A1,A2,A8,GOBOARD5:2;
then G*(c,len G) in Vertical_Line ((E-bound L~f + W-bound L~f) / 2) by A3;
then
A10: L~f /\ L~f /\ LSeg(G*(c,1),G*(c,len G)) c= L~f /\ Vertical_Line ((
E-bound L~f + W-bound L~f) / 2) by A4,JORDAN1A:13,XBOOLE_1:26;
then
A11: X c= Y by RELAT_1:123;
then
A12: for r being Real st r in X holds r<=upper_bound Y
by A5,SEQ_4:def 1;
A13: Y is non empty by A11,A6,Lm2,RELAT_1:119,XBOOLE_1:3;
A14: for s being Real st 0~~ p`2;
A11: proj2.:(L~Cage(C,n) /\ Vertical_Line w) is non empty bounded_above by A7,
JORDAN21:12,13;
A12: p`2 = upper_bound (proj2.:(L~Cage(C,n) /\ Vertical_Line w))
by A7,EUCLID:52;
A13: north_halfline p \ {p} misses L~Cage(C,n)
proof
assume north_halfline p \ {p} meets L~Cage(C,n);
then consider x being object such that
A14: x in north_halfline p \ {p} and
A15: x in L~Cage(C,n) by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A15;
A16: x in north_halfline p by A14,XBOOLE_0:def 5;
then
A17: x`2 >= p`2 by TOPREAL1:def 10;
A18: x`1 = w by A8,A16,TOPREAL1:def 10;
then x in Vertical_Line w;
then
A19: x in L~Cage(C,n) /\ Vertical_Line w 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) by A19,FUNCT_2:35;
then
A20: x`2 <= p`2 by A12,A11,SEQ_4:def 1;
not x in {p} by A14,XBOOLE_0:def 5;
then x <> p by TARSKI:def 1;
then x`2 <> p`2 by A8,A18,TOPREAL3:6;
hence contradiction by A17,A20,XXREAL_0:1;
end;
north_halfline p \ {p} is convex by JORDAN21:6;
then
A21: north_halfline p \ {p} c= UBD L~Cage(C,n) or north_halfline p \ {p}
c= BDD L~Cage(C,n) by A13,JORDAN1K:19;
A22: UBD L~Cage(C,n) c= UBD C by JORDAN10:13;
A23: not u in {p} by A10,TARSKI:def 1;
u in north_halfline p by A1,A8,A10,TOPREAL1:def 10;
then
A24: u in north_halfline p \ {p} by A23,XBOOLE_0:def 5;
A25: UBD C misses C by JORDAN21:10;
north_halfline p is not bounded by JORDAN2C:122;
then
A26: north_halfline p \ {p} is not bounded by JORDAN21:1,TOPREAL6:90;
BDD L~Cage(C,n) is bounded by JORDAN2C:106;
then u in UBD L~Cage(C,n) by A21,A26,A24,RLTOPSP1:42;
hence thesis by A6,A22,A25,XBOOLE_0:3;
end;
end;
theorem Th18:
(LMP C)`2 > (LMP L~Cage(C,n))`2
proof
set p = LMP L~Cage(C,n), u = LMP C, w = (W-bound C + E-bound C) / 2;
A1: u`1 = w by EUCLID:52;
A2: p in L~Cage(C,n) by JORDAN21:31;
A3: u = |[u`1,u`2]| by EUCLID:53;
A4: p = |[p`1,p`2]| by EUCLID:53;
A5: C misses L~Cage(C,n) by JORDAN10:5;
A6: u in C by JORDAN21:31;
A7: w = (W-bound L~Cage(C,n) + E-bound L~Cage(C,n)) / 2 by JORDAN1G:33;
then
A8: p`1 = w by EUCLID:52;
assume
A9: not thesis;
per cases by A9,XXREAL_0:1;
suppose
u`2 = p`2;
hence thesis by A1,A8,A4,A3,A5,A6,A2,XBOOLE_0:3;
end;
suppose
A10: u`2 < p`2;
A11: proj2.:(L~Cage(C,n) /\ Vertical_Line w) is non empty bounded_below by A7,
JORDAN21:12,13;
A12: p`2 = lower_bound (proj2.:(L~Cage(C,n) /\ Vertical_Line w))
by A7,EUCLID:52;
A13: south_halfline p \ {p} misses L~Cage(C,n)
proof
assume south_halfline p \ {p} meets L~Cage(C,n);
then consider x being object such that
A14: x in south_halfline p \ {p} and
A15: x in L~Cage(C,n) by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A15;
A16: x in south_halfline p by A14,XBOOLE_0:def 5;
then
A17: x`2 <= p`2 by TOPREAL1:def 12;
A18: x`1 = w by A8,A16,TOPREAL1:def 12;
then x in Vertical_Line w;
then
A19: x in L~Cage(C,n) /\ Vertical_Line w 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) by A19,FUNCT_2:35;
then
A20: x`2 >= p`2 by A12,A11,SEQ_4:def 2;
not x in {p} by A14,XBOOLE_0:def 5;
then x <> p by TARSKI:def 1;
then x`2 <> p`2 by A8,A18,TOPREAL3:6;
hence contradiction by A17,A20,XXREAL_0:1;
end;
south_halfline p \ {p} is convex by JORDAN21:7;
then
A21: south_halfline p \ {p} c= UBD L~Cage(C,n) or south_halfline p \ {p}
c= BDD L~Cage(C,n) by A13,JORDAN1K:19;
A22: UBD L~Cage(C,n) c= UBD C by JORDAN10:13;
A23: not u in {p} by A10,TARSKI:def 1;
u in south_halfline p by A1,A8,A10,TOPREAL1:def 12;
then
A24: u in south_halfline p \ {p} by A23,XBOOLE_0:def 5;
A25: UBD C misses C by JORDAN21:10;
south_halfline p is not bounded by JORDAN2C:123;
then
A26: south_halfline p \ {p} is not bounded by JORDAN21:1,TOPREAL6:90;
BDD L~Cage(C,n) is bounded by JORDAN2C:106;
then u in UBD L~Cage(C,n) by A21,A26,A24,RLTOPSP1:42;
hence thesis by A6,A22,A25,XBOOLE_0:3;
end;
end;
theorem Th19:
0 < n implies ex i being Nat st 1 <= i & i <= len
Gauge(C,n) & UMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i)
proof
set f = Cage(C,n), G = Gauge(C,n), w = Center G;
A1: f is_sequence_on G by JORDAN9:def 1;
A2: len G = width G by JORDAN8:def 1;
LSeg(G*(w,1),G*(w,len G)) meets Upper_Arc L~f by JORDAN1B:31;
then
A3: LSeg(G*(w,1),G*(w,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
A4: w <= len G by JORDAN1B:13;
assume
A5: 0 < n;
then
UMP L~f = |[ (E-bound L~f + W-bound L~f) / 2,
upper_bound (proj2.:(L~f /\ LSeg(G
*(w,1),G*(w,len G)))) ]| by Th13;
then
A6: (UMP L~f)`2 = upper_bound (proj2.:(L~f /\ LSeg(G*(w,1),G*(w,len G))))
by EUCLID:52;
A7: 1 <= len G by Lm3;
A8: 1 <= w by JORDAN1B:11;
then
A9: [w,len G] in Indices G by A2,A7,A4,MATRIX_0:30;
[w,1] in Indices G by A2,A7,A8,A4,MATRIX_0:30;
then consider i such that
A10: 1 <= i and
A11: i <= len G and
A12: G*(w,i)`2 = upper_bound(proj2.:(LSeg(G*(w,1),G*(w,len G)) /\ L~f))
by A1,A3,A7,A9,JORDAN1F:2;
A13: (UMP L~f)`1 = (E-bound L~f + W-bound L~f) / 2 by EUCLID:52;
take i;
thus 1 <= i & i <= len G by A10,A11;
G*(w,i)`1 = (W-bound C + E-bound C) / 2 by A5,A2,A10,A11,JORDAN1G:35;
then (UMP L~f)`1 = G*(w,i)`1 by A13,JORDAN1G:33;
hence thesis by A12,A6,TOPREAL3:6;
end;
theorem Th20:
0 < n implies ex i being Nat st 1 <= i & i <= len
Gauge(C,n) & LMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i)
proof
set f = Cage(C,n), G = Gauge(C,n), w = Center G;
A1: f is_sequence_on G by JORDAN9:def 1;
A2: len G = width G by JORDAN8:def 1;
LSeg(G*(w,1),G*(w,len G)) meets Upper_Arc L~f by JORDAN1B:31;
then
A3: LSeg(G*(w,1),G*(w,len G)) meets L~f by JORDAN6:61,XBOOLE_1:63;
A4: w <= len G by JORDAN1B:13;
assume
A5: 0 < n;
then
LMP L~f = |[ (E-bound L~f + W-bound L~f) / 2,
lower_bound (proj2.:(L~f /\ LSeg(G
*(w,1),G*(w,len G)))) ]| by Th14;
then
A6: (LMP L~f)`2 = lower_bound (proj2.:(L~f /\ LSeg(G*(w,1),G*(w,len G))))
by EUCLID:52;
A7: 1 <= len G by Lm3;
A8: 1 <= w by JORDAN1B:11;
then
A9: [w,len G] in Indices G by A2,A7,A4,MATRIX_0:30;
[w,1] in Indices G by A2,A7,A8,A4,MATRIX_0:30;
then consider i such that
A10: 1 <= i and
A11: i <= len G and
A12: G*(w,i)`2 = lower_bound(proj2.:(LSeg(G*(w,1),G*(w,len G)) /\ L~f))
by A1,A3,A7,A9,JORDAN1F:1;
A13: (LMP L~f)`1 = (E-bound L~f + W-bound L~f) / 2 by EUCLID:52;
take i;
thus 1 <= i & i <= len G by A10,A11;
G*(w,i)`1 = (W-bound C + E-bound C) / 2 by A5,A2,A10,A11,JORDAN1G:35;
then (LMP L~f)`1 = G*(w,i)`1 by A13,JORDAN1G:33;
hence thesis by A12,A6,TOPREAL3:6;
end;
theorem Th21:
0 < n implies UMP L~Cage(C,n) = UMP Upper_Arc L~Cage(C,n)
proof
set f = Cage(C,n);
set w = (E-bound C + W-bound C) / 2;
A1: Upper_Arc L~f c= L~f by JORDAN6:61;
A2: W-bound C + E-bound C = W-bound L~f + E-bound L~f by JORDAN1G:33;
A3: E-bound L~f = E-bound Upper_Arc L~f by JORDAN21:18;
A4: W-bound L~f = W-bound Upper_Arc L~f by JORDAN21:17;
assume
A5: 0 < n;
then
A6: 0+1 <= n by NAT_1:13;
then
A7: n-'1+1 = n by XREAL_1:235;
A8: now
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~f \/ Lower_Arc L~f = L~f by JORDAN6:def 9;
assume
A12: not UMP L~f in Upper_Arc L~f;
UMP L~f in L~f by JORDAN21:30;
then
A13: UMP L~f in Lower_Arc L~f 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 Nat such that
A16: 1 <= j and
A17: j <= len Gauge(C,n) and
A18: UMP L~f = Gauge(C,n)*(Center Gauge(C,n),j) by A5,Th19;
set a = Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1)), b = Gauge(C,n)*(
Center Gauge(C,n),j), L = LSeg(a,b);
len Gauge(C,1) = width Gauge(C,1) by JORDAN8:def 1;
then L meets Upper_Arc L~f by A7,A13,A16,A17,A18,A14,JORDAN19:5;
then consider x being object such that
A19: x in L and
A20: x in Upper_Arc L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A19;
A21: a in L by RLTOPSP1:68;
A22: 1 <= len Gauge(C,1) by Lm3;
then
A23: a`1 = w by JORDAN1A:38;
then
A24: b`1 = w by A5,A16,A17,A22,JORDAN1A:36;
then L is vertical by A23,SPPOL_1:16;
then
A25: x`1 = w by A19,A23,A21,SPPOL_1:def 3;
then x in Vertical_Line w;
then
A26: x in Upper_Arc L~f /\ Vertical_Line w by A20,XBOOLE_0:def 4;
then
A27: (UMP Upper_Arc L~f)`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 a`2 >= b`2 by A28,XXREAL_0:2;
then
A29: x`2 >= b`2 by A19,TOPREAL1:4;
(UMP L~f)`2 >= (UMP Upper_Arc L~f)`2 by A1,A2,A4,A3,A26,JORDAN21:13,43;
then b`2 >= x`2 by A18,A27,XXREAL_0:2;
then b`2 = x`2 by A29,XXREAL_0:1;
hence contradiction by A12,A18,A20,A24,A25,TOPREAL3:6;
end;
proj2.:(L~f /\ Vertical_Line w) is bounded_above by A2,JORDAN21:13;
hence thesis by A1,A2,A4,A3,A8,JORDAN21:21,45;
end;
theorem Th22:
0 < n implies LMP L~Cage(C,n) = LMP Lower_Arc L~Cage(C,n)
proof
set f = Cage(C,n);
set w = (E-bound C + W-bound C) / 2;
A1: Lower_Arc L~f c= L~f by JORDAN6:61;
A2: W-bound C + E-bound C = W-bound L~f + E-bound L~f by JORDAN1G:33;
A3: E-bound L~f = E-bound Lower_Arc L~f by JORDAN21:20;
A4: W-bound L~f = W-bound Lower_Arc L~f by JORDAN21:19;
assume
A5: 0 < n;
then
A6: 0+1 <= n by NAT_1:13;
then
A7: n-'1+1 = n by XREAL_1:235;
A8: now
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~f \/ Lower_Arc L~f = L~f by JORDAN6:def 9;
assume
A12: not LMP L~f in Lower_Arc L~f;
consider j being Nat such that
A13: 1 <= j and
A14: j <= len Gauge(C,n) and
A15: LMP L~f = Gauge(C,n)*(Center Gauge(C,n),j) by A5,Th20;
set a = Gauge(C,1)*(Center Gauge(C,1),1), b = Gauge(C,n)*(Center Gauge(C,n
),j), L = LSeg(a,b);
A16: a in L by RLTOPSP1:68;
LMP L~f in L~f by JORDAN21:31;
then LMP L~f in Upper_Arc L~f by A12,A11,XBOOLE_0:def 3;
then L meets Lower_Arc L~f by A7,A13,A14,A15,A10,JORDAN1J:62;
then consider x being object such that
A17: x in L and
A18: x in Lower_Arc L~f by XBOOLE_0:3;
reconsider 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: a`1 = w by JORDAN1A:38;
then
A22: b`1 = w by A5,A13,A14,A20,JORDAN1A:36;
then L is vertical by A21,SPPOL_1:16;
then
A23: x`1 = w by A17,A21,A16,SPPOL_1:def 3;
then x in Vertical_Line w;
then
A24: x in Lower_Arc L~f /\ Vertical_Line w by A18,XBOOLE_0:def 4;
then
A25: (LMP Lower_Arc L~f)`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 a`2 <= b`2 by A27,XXREAL_0:2;
then
A28: x`2 <= b`2 by A17,TOPREAL1:4;
(LMP L~f)`2 <= (LMP Lower_Arc L~f)`2 by A1,A2,A4,A3,A24,JORDAN21:13,44;
then b`2 <= x`2 by A15,A25,XXREAL_0:2;
then b`2 = x`2 by A28,XXREAL_0:1;
hence contradiction by A12,A15,A18,A22,A23,TOPREAL3:6;
end;
proj2.:(L~f /\ Vertical_Line w) is bounded_below by A2,JORDAN21:13;
hence thesis by A1,A2,A4,A3,A8,JORDAN21:22,46;
end;
theorem Th23:
0 < n implies (UMP C)`2 < (UMP Upper_Arc L~Cage(C,n))`2
proof
assume 0 < n;
then UMP Upper_Arc L~Cage(C,n) = UMP L~Cage(C,n) by Th21;
hence thesis by Th17;
end;
theorem Th24:
0 < n implies (LMP Lower_Arc L~Cage(C,n))`2 < (LMP C)`2
proof
assume 0 < n;
then LMP Lower_Arc L~Cage(C,n) = LMP L~Cage(C,n) by Th22;
hence thesis by Th18;
end;
theorem Th25:
i <= j implies (UMP L~Cage(C,j))`2 <= (UMP L~Cage(C,i))`2
proof
set w = (E-bound C + W-bound C) / 2, ui = UMP L~Cage(C,i), uj = UMP L~Cage(C
,j);
assume i <= j;
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: uj`2 = upper_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) by EUCLID:52;
assume (UMP L~Cage(C,j))`2 > (UMP L~Cage(C,i))`2;
then
A4: uj`2 - ui`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: ui`2 = upper_bound (proj2.:(L~Cage(C,i) /\ Vertical_Line w)) by EUCLID:52;
A7: proj2.:(L~Cage(C,i) /\ Vertical_Line w) is non empty bounded_above by A5,
JORDAN21:12,13;
proj2.:(L~Cage(C,j) /\ Vertical_Line w) is non empty bounded_above by A2,
JORDAN21:12,13;
then consider r being Real such that
A8: r in proj2.:(L~Cage(C,j) /\ Vertical_Line w) and
A9: upper_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) - (uj`2 - ui`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 w 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 w by A10,XBOOLE_0:def 4;
assume north_halfline x meets L~Cage(C,i);
then consider y being object such that
A14: y in north_halfline x and
A15: y in L~Cage(C,i) by XBOOLE_0:3;
reconsider y as Point of TOP-REAL 2 by A15;
y`1 = x`1 by A14,TOPREAL1:def 10
.= w by A13,JORDAN6:31;
then y in Vertical_Line w;
then
A16: y in L~Cage(C,i) /\ Vertical_Line w 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 w) by A16,FUNCT_2:35;
then
A17: y`2 <= ui`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;
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 thesis by SPRECT_3:26;
end;
theorem Th26:
i <= j implies (LMP L~Cage(C,i))`2 <= (LMP L~Cage(C,j))`2
proof
set w = (E-bound C + W-bound C) / 2, ui = LMP L~Cage(C,i), uj = LMP L~Cage(C
,j);
assume i <= j;
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: uj`2 = lower_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) by EUCLID:52;
assume (LMP L~Cage(C,i))`2 > (LMP L~Cage(C,j))`2;
then
A4: ui`2 - uj`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: ui`2 = lower_bound (proj2.:(L~Cage(C,i) /\ Vertical_Line w)) by EUCLID:52;
A7: proj2.:(L~Cage(C,i) /\ Vertical_Line w) is non empty bounded_below by A5,
JORDAN21:12,13;
proj2.:(L~Cage(C,j) /\ Vertical_Line w) is non empty bounded_below by A2,
JORDAN21:12,13;
then consider r being Real such that
A8: r in proj2.:(L~Cage(C,j) /\ Vertical_Line w) and
A9: r < lower_bound (proj2.:(L~Cage(C,j) /\ Vertical_Line w)) + (ui`2 - uj`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 w 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 w by A10,XBOOLE_0:def 4;
assume south_halfline x meets L~Cage(C,i);
then consider y being object such that
A14: y in south_halfline x and
A15: y in L~Cage(C,i) by XBOOLE_0:3;
reconsider y as Point of TOP-REAL 2 by A15;
y`1 = x`1 by A14,TOPREAL1:def 12
.= w by A13,JORDAN6:31;
then y in Vertical_Line w;
then
A16: y in L~Cage(C,i) /\ Vertical_Line w 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 w) by A16,FUNCT_2:35;
then
A17: y`2 >= ui`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;
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 thesis by SPRECT_3:26;
end;
theorem Th27:
0 < i & i <= j implies (UMP Upper_Arc L~Cage(C,j))`2 <= (UMP
Upper_Arc L~Cage(C,i))`2
proof
assume that
A1: 0 < i and
A2: i <= j;
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 thesis by A2,A3,Th25;
end;
theorem Th28:
0 < i & i <= j implies (LMP Lower_Arc L~Cage(C,i))`2 <= (LMP
Lower_Arc L~Cage(C,j))`2
proof
assume that
A1: 0 < i and
A2: i <= j;
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 thesis by A2,A3,Th26;
end;
begin :: On Special Points of Approximations
theorem Th29:
W-min C in North_Arc C
proof
reconsider w = W-min C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0 ex k being Nat st
for m being Nat st m > k holds (Upper_Appr C).m meets Ball(w,r)
proof
let r be Real;
assume r > 0;
then r/2 > 0;
then consider k being 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;
reconsider k as Nat;
take k;
let m be Nat such that
A4: m > k;
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 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_0:32;
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_0:32;
then
A19: [i+1,j] in Indices Gauge(C,m) by A16,A18,A17,MATRIX_0:30;
[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_0:32;
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_0:32;
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 thesis by A9,A34,XBOOLE_0:3;
end;
North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
hence thesis by A1,KURATO_2:14;
end;
theorem Th30:
E-max C in North_Arc C
proof
reconsider w = E-max C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0
ex k being Nat st
for m being Nat st m > k
holds (Upper_Appr C).m meets Ball(w,r)
proof
let r be Real;
assume r > 0;
then r/2 > 0;
then consider k being 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;
reconsider k as Nat;
take k;
let m be Nat such that
A4: m > k;
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 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_0:32;
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 in 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_0:32;
1 <= j+1 by NAT_1:11;
then
A24: [i-'1,j+1] in Indices Gauge(C,m) by A23,A20,A18,A19,MATRIX_0:30;
A25: 1 <= j by A13,MATRIX_0:32;
j <= width Gauge(C,m) by A13,MATRIX_0:32;
then
A26: [i-'1,j] in Indices Gauge(C,m) by A25,A20,A18,A19,MATRIX_0:30;
[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 thesis by A7,A38,XBOOLE_0:3;
end;
North_Arc C = Lim_inf Upper_Appr C by JORDAN19:def 3;
hence thesis by A1,KURATO_2:14;
end;
theorem Th31:
W-min C in South_Arc C
proof
reconsider w = W-min C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0
ex k being Nat st for m
being Nat st m > k holds (Lower_Appr C).m meets Ball(w,r)
proof
let r be Real;
assume r > 0;
then r/2 > 0;
then consider k being 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;
reconsider k as Nat;
take k;
let m be Nat such that
A4: m > k;
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 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_0:32;
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_0:32;
then
A19: [i+1,j] in Indices Gauge(C,m) by A16,A18,A17,MATRIX_0:30;
[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_0:32;
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_0:32;
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 thesis by A9,A34,XBOOLE_0:3;
end;
South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
hence thesis by A1,KURATO_2:14;
end;
theorem Th32:
E-max C in South_Arc C
proof
reconsider w = E-max C as Point of Euclid 2 by EUCLID:67;
A1: for r being Real st r > 0 ex k being Nat st for m
being Nat st m > k holds (Lower_Appr C).m meets Ball(w,r)
proof
let r be Real;
assume r > 0;
then r/2 > 0;
then consider k being 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;
let m be Nat such that
A4: m > k;
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 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_0:32;
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 in 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_0:32;
1 <= j+1 by NAT_1:11;
then
A24: [i-'1,j+1] in Indices Gauge(C,m) by A23,A20,A18,A19,MATRIX_0:30;
A25: 1 <= j by A13,MATRIX_0:32;
j <= width Gauge(C,m) by A13,MATRIX_0:32;
then
A26: [i-'1,j] in Indices Gauge(C,m) by A25,A20,A18,A19,MATRIX_0:30;
[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 thesis by A7,A38,XBOOLE_0:3;
end;
South_Arc C = Lim_inf Lower_Appr C by JORDAN19:def 4;
hence thesis by A1,KURATO_2:14;
end;
Lm4: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
theorem Th33:
UMP C in North_Arc C
proof
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 Nat: 0 < n};
set n0 = N-bound L~Cage(C,1);
set H = LSeg(p,|[w,n0]|);
A1: |[w,N-bound C]|`1 = w by EUCLID:52;
A2: |[w,n0]|`1 = w by EUCLID:52;
{UMP Upper_Arc L~Cage(C,n) where n is Nat: 0 < n} c= the
carrier of TOP-REAL 2
proof
let x be object;
assume x in {UMP Upper_Arc L~Cage(C,n) where n is Nat: 0 < n};
then ex n being Nat st x = UMP Upper_Arc L~Cage(C,n) & 0 < n;
hence thesis;
end;
then reconsider U as Subset of TOP-REAL 2;
set q = lower_bound(proj2.:(H /\ U));
set S = LSeg(|[w,q]|, |[w,n0]|);
A3: |[w,N-bound C]|`2 = N-bound C by EUCLID:52;
A4: |[w,n0]|`2 = n0 by EUCLID:52;
A5: for n being Nat holds (UMP Upper_Arc L~Cage(C,n))`1 = w
proof
let n be Nat;
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 by A6,JORDAN21:18;
end;
A7: p`2 <= (UMP Upper_Arc L~Cage(C,1))`2 by Th23;
A8: LSeg(p, |[w, N-bound C]|) /\ C = {p} by JORDAN21:34;
A9: (UMP Upper_Arc L~Cage(C,1))`2 <= n0 by JORDAN21:47;
H /\ U is bounded by TOPREAL6:89;
then proj2.:(H /\ U) is real-bounded by JCT_MISC:14;
then
A10: proj2.:(H /\ U) is bounded_below;
A11: p`1 = w by EUCLID:52;
A12: for n being Nat st 0 < n holds (UMP Upper_Arc L~Cage(C,n))`2
in proj2.:(H /\ U)
proof
let n be Nat;
set f = Cage(C,n);
set s = UMP Upper_Arc L~f;
assume
A13: 0 < n;
then
A14: s 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;
s`2 <= N-bound L~f by JORDAN21:47;
then
A16: s`2 <= n0 by A15,XXREAL_0:2;
A17: s`1 = w by A5;
p`2 <= s`2 by A13,Th23;
then s in H by A2,A4,A11,A16,A17,GOBOARD7:7;
then
A18: s in H /\ U by A14,XBOOLE_0:def 4;
s`2 = proj2.s by PSCOMP_1:def 6;
hence thesis by A18,FUNCT_2:35;
end;
then
A19: (UMP Upper_Arc L~Cage(C,1))`2 in proj2.:(H /\ U);
then q <= (UMP Upper_Arc L~Cage(C,1))`2 by A10,SEQ_4:def 2;
then
A20: q <= n0 by A9,XXREAL_0:2;
A21: |[w,q]|`1 = w by EUCLID:52;
then
A22: S is vertical by A2,SPPOL_1:16;
A23: |[w,q]| in S by RLTOPSP1:68;
A24: |[w,q]|`2 = q by EUCLID:52;
per cases;
suppose
A25: p <> |[w,q]|;
consider S9,C9 being Subset of TopSpaceMetr Euclid 2 such that
A26: S = S9 and
A27: C = C9 and
A28: dist_min(S,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
assume
A32: p`2 >= q;
per cases by A32,XXREAL_0:1;
suppose
p`2 = q;
hence contradiction by A25,EUCLID:52;
end;
suppose
p`2 > q;
then 0 < p`2 - q by XREAL_1:50;
then consider r being Real such that
A33: r in proj2.:(H /\ U) and
A34: r < q+(p`2 - q) by A10,A19,SEQ_4:def 2;
consider t being Point of TOP-REAL 2 such that
A35: t in H /\ U and
A36: proj2.t = r by A33,Lm1;
A37: t in H by A35,XBOOLE_0:def 4;
A38: p`2 <= n0 by A9,A7,XXREAL_0:2;
t`2 = r by A36,PSCOMP_1:def 6;
hence contradiction by A4,A34,A38,A37,TOPREAL1:4;
end;
end;
S misses C
proof
assume S meets C;
then consider x being object such that
A39: x in S and
A40: x in C by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A39;
A41: x`2 <= N-bound C by A40,PSCOMP_1:24;
A42: x`1 = w by A21,A23,A22,A39,SPPOL_1:def 3;
A43: q <= x`2 by A4,A24,A20,A39,TOPREAL1:4;
then p`2 < x`2 by A31,XXREAL_0:2;
then x in LSeg(p, |[w, N-bound C]|) by A1,A3,A11,A41,A42,GOBOARD7:7;
then x in {p} by A8,A40,XBOOLE_0:def 4;
hence contradiction by A31,A43,TARSKI:def 1;
end;
then dist_min(S,C) > 0 by A26,A27,A28,A29,A30,JGRAPH_1:38;
then dist_min(S,C)/2 > 0;
then consider k being Nat such that
A44: 1 < k and
A45: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < dist_min(S,C)/2 and
A46: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < dist_min(S,C)/2 by GOBRD14:11;
set f = Cage(C,k), G = Gauge(C,k);
set s = UMP Upper_Arc L~f;
A47: s`2 <= N-bound L~f by JORDAN21:47;
A48: dist(G*(1,1),G*(1+1,1)) + dist(G*(1,1),G*(1,1+1)) < dist_min(S,C)/2 +
dist_min(S,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: s`2 <= n0 by A47,XXREAL_0:2;
s`2 in proj2.:(H /\ U) by A12,A44;
then
A50: q <= s`2 by A10,SEQ_4:def 2;
[1,1+1] in Indices G by Th6;
then
A51: dist(G*(1,1),G*(1,1+1)) = (N-bound C - S-bound C)/2|^k by Th5,GOBRD14:9;
[1+1,1] in Indices G by Th7;
then
A52: dist(G*(1,1),G*(1+1,1)) = (E-bound C - W-bound C)/2|^k by Th5,GOBRD14:10;
A53: s in Upper_Arc L~f by JORDAN21:30;
Upper_Arc L~f c= L~f by JORDAN6:61;
then consider i being Nat such that
A54: 1 <= i and
A55: i+1 <= len f and
A56: s in LSeg(f,i) by A53,SPPOL_2:13;
A57: f is_sequence_on G by JORDAN9:def 1;
then consider i1,j1,i2,j2 being Nat such that
A58: [i1,j1] in Indices G and
A59: f/.i = G*(i1,j1) and
A60: [i2,j2] in Indices G and
A61: f/.(i+1) = G*(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_0:32;
right_cell(f,i,G) meets C by A54,A55,JORDAN9:31;
then consider c being object such that
A64: c in right_cell(f,i,G) and
A65: c in C by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A65;
reconsider s9 = s, c9 = c as Point of Euclid 2 by EUCLID:67;
s`1 = w by A5;
then s in S 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(s,c) by TOPREAL6:def 1;
A68: 1 <= j2 by A60,MATRIX_0:32;
left_cell(f,i,G) /\ right_cell(f,i,G) = LSeg(f,i) by A54,A55,A57,GOBRD13:29
;
then
A69: s in right_cell(f,i,G) by A56,XBOOLE_0:def 4;
A70: j2 <= width G by A60,MATRIX_0:32;
A71: j2+1+1<>j2;
A72: 1 <= i2 by A60,MATRIX_0:32;
A73: j1 <= width G by A58,MATRIX_0:32;
A74: 1 <= j1+1 by NAT_1:11;
A75: i1+1<>i1+0;
A76: i1 <= len G by A58,MATRIX_0:32;
A77: i2 <= len G by A60,MATRIX_0:32;
A78: i2+1+1<>i2;
A79: 1 <= j1 by A58,MATRIX_0:32;
A80: 1 <= i1+1 by NAT_1:11;
now
per cases by A62;
suppose
A81: i1 = i2 & j1+1 = j2;
then
A82: dist(G*(i1,j1),G*(i1,j1+1)) = (N-bound C - S-bound C)/2|^k by A58,A60,
GOBRD14:9;
A83: dist(G*(i1,j1),G*(i1,j1+1)) = G*(i1,j1+1)`2 - G*(i1,j1)`2 by A58,A60
,A81,GOBRD14:6;
i1 < len G by A54,A55,A58,A59,A60,A61,A81,JORDAN10:1;
then
A84: i1+1 <= len G by NAT_1:13;
then
A85: [i1+1,j1] in Indices G by A79,A80,A73,MATRIX_0:30;
then
A86: dist(G*(i1,j1),G*(i1+1,j1)) = G*(i1+1,j1)`1 - G*(i1,j1)`1 by A58,
GOBRD14:5;
A87: dist(G*(i1,j1),G*(i1+1,j1)) = (E-bound C - W-bound C)/2|^k by A58,A85,
GOBRD14:10;
A88: j1+1 <= width G by A60,A81,MATRIX_0:32;
A89: right_cell(f,i,G) = cell(G,i1,j1) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A81,GOBRD13:def 2;
then
A90: c`1 <= G*(i1+1,j1)`1 by A64,A63,A79,A88,A84,JORDAN9:17;
A91: s`2 <= G*(i1,j1+1)`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A92: G*(i1,j1)`2 <= s`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A93: s`1 <= G*(i1+1,j1)`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A94: G*(i1,j1)`1 <= s`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A95: c`2 <= G*(i1,j1+1)`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
A96: G*(i1,j1)`2 <= c`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
G*(i1,j1)`1 <= c`1 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
then dist(s,c) <= (G*(i1+1,j1)`1-G*(i1,j1)`1) + (G*(i1,j1+1)`2- G*(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;
end;
suppose
A97: i1+1 = i2 & j1 = j2;
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 G by A73,NAT_D:44;
then
A101: [i1,j1-'1] in Indices G by A63,A76,A98,MATRIX_0:30;
then
A102: dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = G*(i1,j1-'1+1)`2 - G*(i1,j1
-'1)`2 by A58,A99,GOBRD14:6;
A103: [i1+1,j1-'1] in Indices G by A72,A77,A97,A98,A100,MATRIX_0:30;
then
A104: dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = G*(i1+1,j1-'1)`1 - G*( i1,
j1-'1)`1 by A101,GOBRD14:5;
A105: dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = (N-bound C - S-bound C)/2|^k
by A58,A99,A101,GOBRD14:9;
A106: dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = (E-bound C - W-bound C)/2|^k
by A101,A103,GOBRD14:10;
A107: i1+1 <= len G by A60,A97,MATRIX_0:32;
A108: right_cell(f,i,G) = cell(G,i1,j1-'1) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A97,GOBRD13:def 2;
then
A109: c`1 <= G*(i1+1,j1-'1)`1 by A64,A63,A73,A107,A98,A99,JORDAN9:17;
A110: s`2 <= G*(i1,j1-'1+1)`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A111: G*(i1,j1-'1)`2 <= s`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A112: s`1 <= G*(i1+1,j1-'1)`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A113: G*(i1,j1-'1)`1 <= s`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A114: c`2 <= G*(i1,j1-'1+1)`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A115: G*(i1,j1-'1)`2 <= c`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
G*(i1,j1-'1)`1 <= c`1 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
then dist(s,c) <= (G*(i1+1,j1-'1)`1-G*(i1,j1-'1)`1) + (G*(i1,j1-'1+1)
`2-G*(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;
end;
suppose
A116: i1 = i2+1 & j1 = j2;
then
A117: dist(G*(i2,j2),G*(i2+1,j2)) = (E-bound C - W-bound C)/2|^k by A58,A60,
GOBRD14:10;
A118: dist(G*(i2,j2),G*(i2+1,j2)) = G*(i2+1,j2)`1 - G*(i2,j2)`1 by A58,A60
,A116,GOBRD14:5;
A119: i2+1 <= len G by A58,A116,MATRIX_0:32;
j1 < width G by A54,A55,A58,A59,A60,A61,A116,JORDAN10:4;
then
A120: j1+1 <= width G by NAT_1:13;
then
A121: [i2,j2+1] in Indices G by A72,A74,A77,A116,MATRIX_0:30;
then
A122: dist(G*(i2,j2),G*(i2,j2+1)) = G*(i2,j2+1)`2 - G*(i2,j2)`2 by A60,
GOBRD14:6;
A123: right_cell(f,i,G) = cell(G,i2,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A116,GOBRD13:def 2;
then
A124: c`1 <= G*(i2+1,j2)`1 by A64,A79,A72,A116,A119,A120,JORDAN9:17;
A125: s`2 <= G*(i2,j2+1)`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A126: G*(i2,j2)`2 <= c`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A127: dist(G*(i2,j2),G*(i2,j2+1)) = (N-bound C - S-bound C)/2|^k by A60,A121,
GOBRD14:9;
A128: G*(i2,j2)`2 <= s`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A129: s`1 <= G*(i2+1,j2)`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A130: G*(i2,j2)`1 <= s`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A131: c`2 <= G*(i2,j2+1)`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
G*(i2,j2)`1 <= c`1 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
then dist(s,c) <= (G*(i2+1,j2)`1-G*(i2,j2)`1) + (G*(i2,j2+1)`2- G*(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;
end;
suppose
A132: i1 = i2 & j1 = j2+1;
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 G by A76,NAT_D:44;
then
A135: [i1-'1,j2] in Indices G by A68,A70,A133,MATRIX_0:30;
A136: [i1-'1,j2+1] in Indices G by A79,A73,A132,A133,A134,MATRIX_0:30;
then
A137: dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = G*(i1-'1,j2+1)`2 - G*( i1 -'
1,j2)`2 by A135,GOBRD14:6;
A138: dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = (N-bound C - S-bound C)/2|^k
by A135,A136,GOBRD14:9;
A139: j2+1 <= width G by A58,A132,MATRIX_0:32;
A140: i1-'1+1 = i1 by A133,NAT_D:43;
then
A141: [i1-'1+1,j2] in Indices G by A63,A68,A76,A70,MATRIX_0:30;
then
A142: dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = G*(i1-'1+1,j2)`1 - G*( i1 -'
1,j2)`1 by A135,GOBRD14:5;
A143: right_cell(f,i,G) = cell(G,i1-'1,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A132,GOBRD13:def 2;
then
A144: c`1 <= G*(i1-'1+1,j2)`1 by A64,A68,A76,A139,A133,A140,JORDAN9:17;
A145: s`2 <= G*(i1-'1,j2+1)`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A146: G*(i1-'1,j2)`2 <= s`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A147: s`1 <= G*(i1-'1+1,j2)`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A148: G*(i1-'1,j2)`1 <= s`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A149: c`2 <= G*(i1-'1,j2+1)`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A150: G*(i1-'1,j2)`2 <= c`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A151: dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = (E-bound C - W-bound C)/2|^k
by A135,A141,GOBRD14:10;
G*(i1-'1,j2)`1 <= c`1 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
then dist(s,c) <= (G*(i1-'1+1,j2)`1-G*(i1-'1,j2)`1) + (G*(i1-'1,j2+1)
`2-G*(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;
end;
end;
hence thesis;
end;
suppose
p = |[w,q]|;
then
A152: p`2 = q by EUCLID:52;
A153: ex S being Real_Sequence of 2 st S is convergent & (for x being
Nat holds S.x in (Upper_Appr C).x) & p = lim S
proof
set R = {(UMP Upper_Arc L~Cage(C,n))`2 where n is Nat: 0 < n};
R c= REAL
proof
let x be object;
assume x in R;
then ex n being Nat st x = (UMP Upper_Arc L~Cage(C,n))`2 &
0 < n;
hence thesis by XREAL_0:def 1;
end;
then reconsider R as Subset of REAL;
deffunc f(Nat) = UMP Upper_Arc L~Cage(C,$1);
reconsider pp=p as Element of REAL 2 by EUCLID:22;
reconsider p1=p as Element of TOP-REAL 2;
A154: for x being Element of NAT holds f(x) is Element of REAL 2 by EUCLID:22;
consider S being sequence of REAL 2 such that
A155: for n being Element of NAT holds S.n = f(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;
A156: R is bounded_below
proof
take q;
let r be ExtReal;
assume r in R;
then ex n being Nat st r = (UMP Upper_Arc L~Cage(C,n))`2 &
0 < n;
then r in proj2.:(H /\ U) by A12;
hence thesis by A10,SEQ_4:def 2;
end;
A157: (UMP Upper_Arc L~Cage(C,1))`2 in R;
A158: for r being Real st 0= (LMP Lower_Arc L~Cage(C,1))`2 by Th24;
A8: LSeg(p, |[w, S-bound C]|) /\ C = {p} by JORDAN21:35;
A9: (LMP Lower_Arc L~Cage(C,1))`2 >= n0 by JORDAN21:48;
H /\ U is bounded by TOPREAL6:89;
then proj2.:(H /\ U) is real-bounded by JCT_MISC:14;
then
A10: proj2.:(H /\ U) is bounded_above;
A11: p`1 = w by EUCLID:52;
A12: for n being Nat st 0 < n holds (LMP Lower_Arc L~Cage(C,n))`2
in proj2.:(H /\ U)
proof
let n be Nat;
set f = Cage(C,n);
set s = LMP Lower_Arc L~f;
assume
A13: 0 < n;
then
A14: s 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~f <= s`2 by JORDAN21:48;
then
A16: s`2 >= n0 by A15,XXREAL_0:2;
A17: s`1 = w by A5;
p`2 >= s`2 by A13,Th24;
then s in H by A2,A4,A11,A16,A17,GOBOARD7:7;
then
A18: s in H /\ U by A14,XBOOLE_0:def 4;
s`2 = proj2.s by PSCOMP_1:def 6;
hence thesis by A18,FUNCT_2:35;
end;
then
A19: (LMP Lower_Arc L~Cage(C,1))`2 in proj2.:(H /\ U);
then q >= (LMP Lower_Arc L~Cage(C,1))`2 by A10,SEQ_4:def 1;
then
A20: q >= n0 by A9,XXREAL_0:2;
A21: |[w,q]|`1 = w by EUCLID:52;
then
A22: S is vertical by A2,SPPOL_1:16;
A23: |[w,q]| in S by RLTOPSP1:68;
A24: |[w,q]|`2 = q by EUCLID:52;
per cases;
suppose
A25: p <> |[w,q]|;
consider S9,C9 being Subset of TopSpaceMetr Euclid 2 such that
A26: S = S9 and
A27: C = C9 and
A28: dist_min(S,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
assume
A32: p`2 <= q;
per cases by A32,XXREAL_0:1;
suppose
p`2 = q;
hence contradiction by A25,EUCLID:52;
end;
suppose
p`2 < q;
then 0 < q - p`2 by XREAL_1:50;
then consider r being Real such that
A33: r in proj2.:(H /\ U) and
A34: q-(q-p`2) < r by A10,A19,SEQ_4:def 1;
consider t being Point of TOP-REAL 2 such that
A35: t in H /\ U and
A36: proj2.t = r by A33,Lm1;
A37: t in H by A35,XBOOLE_0:def 4;
A38: p`2 >= n0 by A9,A7,XXREAL_0:2;
t`2 = r by A36,PSCOMP_1:def 6;
hence contradiction by A4,A34,A38,A37,TOPREAL1:4;
end;
end;
S misses C
proof
assume S meets C;
then consider x being object such that
A39: x in S and
A40: x in C by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A39;
A41: x`2 >= S-bound C by A40,PSCOMP_1:24;
A42: x`1 = w by A21,A23,A22,A39,SPPOL_1:def 3;
A43: q >= x`2 by A4,A24,A20,A39,TOPREAL1:4;
then p`2 > x`2 by A31,XXREAL_0:2;
then x in LSeg(p, |[w, S-bound C]|) by A1,A3,A11,A41,A42,GOBOARD7:7;
then x in {p} by A8,A40,XBOOLE_0:def 4;
hence contradiction by A31,A43,TARSKI:def 1;
end;
then dist_min(S,C) > 0 by A26,A27,A28,A29,A30,JGRAPH_1:38;
then dist_min(S,C)/2 > 0;
then consider k being Nat such that
A44: 1 < k and
A45: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(1,2)) < dist_min(S,C)/2 and
A46: dist(Gauge(C,k)*(1,1),Gauge(C,k)*(2,1)) < dist_min(S,C)/2 by GOBRD14:11;
set f = Cage(C,k), G = Gauge(C,k);
set s = LMP Lower_Arc L~f;
A47: s`2 >= S-bound L~f by JORDAN21:48;
A48: dist(G*(1,1),G*(1+1,1)) + dist(G*(1,1),G*(1,1+1)) < dist_min(S,C)/2 +
dist_min(S,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: s`2 >= n0 by A47,XXREAL_0:2;
s`2 in proj2.:(H /\ U) by A12,A44;
then
A50: q >= s`2 by A10,SEQ_4:def 1;
[1,1+1] in Indices G by Th6;
then
A51: dist(G*(1,1),G*(1,1+1)) = (N-bound C - S-bound C)/2|^k by Th5,GOBRD14:9;
[1+1,1] in Indices G by Th7;
then
A52: dist(G*(1,1),G*(1+1,1)) = (E-bound C - W-bound C)/2|^k by Th5,GOBRD14:10;
A53: s in Lower_Arc L~f by JORDAN21:31;
Lower_Arc L~f c= L~f by JORDAN6:61;
then consider i being Nat such that
A54: 1 <= i and
A55: i+1 <= len f and
A56: s in LSeg(f,i) by A53,SPPOL_2:13;
A57: f is_sequence_on G by JORDAN9:def 1;
then consider i1,j1,i2,j2 being Nat such that
A58: [i1,j1] in Indices G and
A59: f/.i = G*(i1,j1) and
A60: [i2,j2] in Indices G and
A61: f/.(i+1) = G*(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_0:32;
right_cell(f,i,G) meets C by A54,A55,JORDAN9:31;
then consider c being object such that
A64: c in right_cell(f,i,G) and
A65: c in C by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A65;
reconsider s9 = s, c9 = c as Point of Euclid 2 by EUCLID:67;
s`1 = w by A5;
then s in S 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(s,c) by TOPREAL6:def 1;
A68: 1 <= j2 by A60,MATRIX_0:32;
left_cell(f,i,G) /\ right_cell(f,i,G) = LSeg(f,i) by A54,A55,A57,GOBRD13:29
;
then
A69: s in right_cell(f,i,G) by A56,XBOOLE_0:def 4;
A70: j2 <= width G by A60,MATRIX_0:32;
A71: j2+1+1<>j2;
A72: 1 <= i2 by A60,MATRIX_0:32;
A73: j1 <= width G by A58,MATRIX_0:32;
A74: 1 <= j1+1 by NAT_1:11;
A75: i1+1<>i1+0;
A76: i1 <= len G by A58,MATRIX_0:32;
A77: i2 <= len G by A60,MATRIX_0:32;
A78: i2+1+1<>i2;
A79: 1 <= j1 by A58,MATRIX_0:32;
A80: 1 <= i1+1 by NAT_1:11;
now
per cases by A62;
suppose
A81: i1 = i2 & j1+1 = j2;
then
A82: dist(G*(i1,j1),G*(i1,j1+1)) = (N-bound C - S-bound C)/2|^k by A58,A60,
GOBRD14:9;
A83: dist(G*(i1,j1),G*(i1,j1+1)) = G*(i1,j1+1)`2 - G*(i1,j1)`2 by A58,A60
,A81,GOBRD14:6;
i1 < len G by A54,A55,A58,A59,A60,A61,A81,JORDAN10:1;
then
A84: i1+1 <= len G by NAT_1:13;
then
A85: [i1+1,j1] in Indices G by A79,A80,A73,MATRIX_0:30;
then
A86: dist(G*(i1,j1),G*(i1+1,j1)) = G*(i1+1,j1)`1 - G*(i1,j1)`1 by A58,
GOBRD14:5;
A87: dist(G*(i1,j1),G*(i1+1,j1)) = (E-bound C - W-bound C)/2|^k by A58,A85,
GOBRD14:10;
A88: j1+1 <= width G by A60,A81,MATRIX_0:32;
A89: right_cell(f,i,G) = cell(G,i1,j1) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A81,GOBRD13:def 2;
then
A90: c`1 <= G*(i1+1,j1)`1 by A64,A63,A79,A88,A84,JORDAN9:17;
A91: s`2 <= G*(i1,j1+1)`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A92: G*(i1,j1)`2 <= s`2 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A93: s`1 <= G*(i1+1,j1)`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A94: G*(i1,j1)`1 <= s`1 by A69,A63,A79,A88,A84,A89,JORDAN9:17;
A95: c`2 <= G*(i1,j1+1)`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
A96: G*(i1,j1)`2 <= c`2 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
G*(i1,j1)`1 <= c`1 by A64,A63,A79,A88,A84,A89,JORDAN9:17;
then dist(s,c) <= (G*(i1+1,j1)`1-G*(i1,j1)`1) + (G*(i1,j1+1)`2- G*(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;
end;
suppose
A97: i1+1 = i2 & j1 = j2;
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 G by A73,NAT_D:44;
then
A101: [i1,j1-'1] in Indices G by A63,A76,A98,MATRIX_0:30;
then
A102: dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = G*(i1,j1-'1+1)`2 - G*(i1,j1
-'1)`2 by A58,A99,GOBRD14:6;
A103: [i1+1,j1-'1] in Indices G by A72,A77,A97,A98,A100,MATRIX_0:30;
then
A104: dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = G*(i1+1,j1-'1)`1 - G*( i1,
j1-'1)`1 by A101,GOBRD14:5;
A105: dist(G*(i1,j1-'1),G*(i1,j1-'1+1)) = (N-bound C - S-bound C)/2|^k
by A58,A99,A101,GOBRD14:9;
A106: dist(G*(i1,j1-'1),G*(i1+1,j1-'1)) = (E-bound C - W-bound C)/2|^k
by A101,A103,GOBRD14:10;
A107: i1+1 <= len G by A60,A97,MATRIX_0:32;
A108: right_cell(f,i,G) = cell(G,i1,j1-'1) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A97,GOBRD13:def 2;
then
A109: c`1 <= G*(i1+1,j1-'1)`1 by A64,A63,A73,A107,A98,A99,JORDAN9:17;
A110: s`2 <= G*(i1,j1-'1+1)`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A111: G*(i1,j1-'1)`2 <= s`2 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A112: s`1 <= G*(i1+1,j1-'1)`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A113: G*(i1,j1-'1)`1 <= s`1 by A69,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A114: c`2 <= G*(i1,j1-'1+1)`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
A115: G*(i1,j1-'1)`2 <= c`2 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
G*(i1,j1-'1)`1 <= c`1 by A64,A63,A73,A107,A98,A99,A108,JORDAN9:17;
then dist(s,c) <= (G*(i1+1,j1-'1)`1-G*(i1,j1-'1)`1) + (G*(i1,j1-'1+1)
`2-G*(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;
end;
suppose
A116: i1 = i2+1 & j1 = j2;
then
A117: dist(G*(i2,j2),G*(i2+1,j2)) = (E-bound C - W-bound C)/2|^k by A58,A60,
GOBRD14:10;
A118: dist(G*(i2,j2),G*(i2+1,j2)) = G*(i2+1,j2)`1 - G*(i2,j2)`1 by A58,A60
,A116,GOBRD14:5;
A119: i2+1 <= len G by A58,A116,MATRIX_0:32;
j1 < width G by A54,A55,A58,A59,A60,A61,A116,JORDAN10:4;
then
A120: j1+1 <= width G by NAT_1:13;
then
A121: [i2,j2+1] in Indices G by A72,A74,A77,A116,MATRIX_0:30;
then
A122: dist(G*(i2,j2),G*(i2,j2+1)) = G*(i2,j2+1)`2 - G*(i2,j2)`2 by A60,
GOBRD14:6;
A123: right_cell(f,i,G) = cell(G,i2,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A78,A116,GOBRD13:def 2;
then
A124: c`1 <= G*(i2+1,j2)`1 by A64,A79,A72,A116,A119,A120,JORDAN9:17;
A125: s`2 <= G*(i2,j2+1)`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A126: G*(i2,j2)`2 <= c`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A127: dist(G*(i2,j2),G*(i2,j2+1)) = (N-bound C - S-bound C)/2|^k by A60,A121,
GOBRD14:9;
A128: G*(i2,j2)`2 <= s`2 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A129: s`1 <= G*(i2+1,j2)`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A130: G*(i2,j2)`1 <= s`1 by A69,A79,A72,A116,A119,A120,A123,JORDAN9:17;
A131: c`2 <= G*(i2,j2+1)`2 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
G*(i2,j2)`1 <= c`1 by A64,A79,A72,A116,A119,A120,A123,JORDAN9:17;
then dist(s,c) <= (G*(i2+1,j2)`1-G*(i2,j2)`1) + (G*(i2,j2+1)`2- G*(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;
end;
suppose
A132: i1 = i2 & j1 = j2+1;
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 G by A76,NAT_D:44;
then
A135: [i1-'1,j2] in Indices G by A68,A70,A133,MATRIX_0:30;
A136: [i1-'1,j2+1] in Indices G by A79,A73,A132,A133,A134,MATRIX_0:30;
then
A137: dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = G*(i1-'1,j2+1)`2 - G*( i1 -'
1,j2)`2 by A135,GOBRD14:6;
A138: dist(G*(i1-'1,j2),G*(i1-'1,j2+1)) = (N-bound C - S-bound C)/2|^k
by A135,A136,GOBRD14:9;
A139: j2+1 <= width G by A58,A132,MATRIX_0:32;
A140: i1-'1+1 = i1 by A133,NAT_D:43;
then
A141: [i1-'1+1,j2] in Indices G by A63,A68,A76,A70,MATRIX_0:30;
then
A142: dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = G*(i1-'1+1,j2)`1 - G*( i1 -'
1,j2)`1 by A135,GOBRD14:5;
A143: right_cell(f,i,G) = cell(G,i1-'1,j2) by A54,A55,A57,A58,A59,A60,A61,A75
,A71,A132,GOBRD13:def 2;
then
A144: c`1 <= G*(i1-'1+1,j2)`1 by A64,A68,A76,A139,A133,A140,JORDAN9:17;
A145: s`2 <= G*(i1-'1,j2+1)`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A146: G*(i1-'1,j2)`2 <= s`2 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A147: s`1 <= G*(i1-'1+1,j2)`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A148: G*(i1-'1,j2)`1 <= s`1 by A69,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A149: c`2 <= G*(i1-'1,j2+1)`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A150: G*(i1-'1,j2)`2 <= c`2 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
A151: dist(G*(i1-'1,j2),G*(i1-'1+1,j2)) = (E-bound C - W-bound C)/2|^k
by A135,A141,GOBRD14:10;
G*(i1-'1,j2)`1 <= c`1 by A64,A68,A76,A139,A133,A140,A143,JORDAN9:17;
then dist(s,c) <= (G*(i1-'1+1,j2)`1-G*(i1-'1,j2)`1) + (G*(i1-'1,j2+1)
`2-G*(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;
end;
end;
hence thesis;
end;
suppose
p = |[w,q]|;
then
A152: p`2 = q by EUCLID:52;
A153: ex S being Real_Sequence of 2 st S is convergent & (for x being
Nat holds S.x in (Lower_Appr C).x) & p = lim S
proof
set R = {(LMP Lower_Arc L~Cage(C,n))`2 where n is Nat: 0 < n};
R c= REAL
proof
let x be object;
assume x in R;
then ex n being Nat st x = (LMP Lower_Arc L~Cage(C,n))`2 &
0 < n;
hence thesis by XREAL_0:def 1;
end;
then reconsider R as Subset of REAL;
deffunc g(Nat) = LMP Lower_Arc L~Cage(C,$1);
reconsider pp = p as Element of REAL 2 by EUCLID:22;
A154: for x being Element of NAT holds g(x) is Element of REAL 2 by EUCLID:22;
consider S being sequence of REAL 2 such that
A155: for n being Element of NAT holds S.n = g(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;
A156: R is bounded_above
proof
take q;
let r be ExtReal;
assume r in R;
then ex n being Nat st r = (LMP Lower_Arc L~Cage(C,n))`2 &
0 < n;
then r in proj2.:(H /\ U) by A12;
hence thesis by A10,SEQ_4:def 1;
end;
A157: (LMP Lower_Arc L~Cage(C,1))`2 in R;
A158: for r being Real st 0= v by A155,A168,A171;
then
A173: p`2 - (Sm)`2 <= p`2 - v by XREAL_1:13;
reconsider SSm = Sm as Point of TOP-REAL 2;
A174: SSm-p1 = S.m-pp;
A175: S.m = LMP Lower_Arc L~Cage(C,m) by A155,A171;
then (Sm)`1 = w by A5;
then |.(Sm)`1-p`1.| = 0 by A11,ABSVALUE:def 1;
then
A176: |. S.m-pp .|<=0+|.(Sm)`2-p`2.| by A174,JGRAPH_1:32;
0 > (Sm)`2-p`2 by A169,A175,A172,Th24,XREAL_1:49;
then
A177: |. S.m-pp .|<=-((Sm)`2-p`2) by A176,ABSVALUE:def 1;
for r being Real st r in R holds q>=r
proof
let r be Real;
assume r in R;
then ex n being Nat st r = (LMP Lower_Arc L~Cage(C,n))`2
& 0 < n;
then r in proj2.:(H /\ U) by A12;
hence thesis by A10,SEQ_4:def 1;
end;
then upper_bound R = q by A157,A156,A159,SEQ_4:def 1;
then p`2-(Sm)`2 < r by A152,A170,A173,XXREAL_0:2;
hence thesis by A177,XXREAL_0:2;
end;
thus
A178: SS is convergent
proof
take p;
let r be Real;
assume 0 0 and
A8: Ball(e,r) c= BDD C by A6,TOPMETR:15;
consider k being Nat such that
A9: for m being 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 thesis by A9,A12,A11,A10,XBOOLE_1:63;
end;
suppose
A13: x in UBD C;
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 = the set of all UBD L~Cage(C,m) where m is Nat
by JORDAN10:def 1;
then consider m being 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 such that
A18: r > 0 and
A19: Ball(e,r) c= LeftComp Cage(C,m) by A17,TOPMETR:15;
consider k being Nat such that
A20: for m being Nat st m > k holds (Upper_Appr C).m meets
Ball(e,r) by A2,A1,A18,KURATO_2:14;
thus thesis
proof
per cases;
suppose
A21: m > k;
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 thesis by A20,A21,A22,A23,XBOOLE_1:63;
end;
suppose
m <= k;
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;
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;
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 thesis by A20,A25,A26,A27,XBOOLE_1:63;
end;
end;
end;
end;
theorem Th36:
South_Arc C c= C
proof
let x be object;
assume
A1: x in South_Arc C;
assume
A2: not x in C;
reconsider 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;
per cases by A3,A5,XBOOLE_0:def 3;
suppose
A6: x in BDD C;
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 such that
A7: r > 0 and
A8: Ball(e,r) c= BDD C by A6,TOPMETR:15;
consider k being Nat such that
A9: for m being 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 thesis by A9,A12,A11,A10,XBOOLE_1:63;
end;
suppose
A13: x in UBD C;
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 = the set of all UBD L~Cage(C,m) where m is Nat
by JORDAN10:def 1;
then consider m being 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 such that
A18: r > 0 and
A19: Ball(e,r) c= LeftComp Cage(C,m) by A17,TOPMETR:15;
consider k being Nat such that
A20: for m being Nat st m > k holds (Lower_Appr C).m meets
Ball(e,r) by A1,A4,A18,KURATO_2:14;
thus thesis
proof
per cases;
suppose
A21: m > k;
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 thesis by A20,A21,A22,A23,XBOOLE_1:63;
end;
suppose
m <= k;
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;
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;
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 thesis by A20,A25,A26,A27,XBOOLE_1:63;
end;
end;
end;
end;
theorem
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
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
per cases by A4,A1,A2,A3,JORDAN16:7;
case
LE LMP C, UMP C, 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;
hence UMP C in Lower_Arc C & LMP C in Upper_Arc C by JORDAN21:49,50;
end;
case
LE UMP C, LMP C, 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;
hence LMP C in Lower_Arc C & UMP C in Upper_Arc C by JORDAN21:49,50;
end;
end;
hence thesis;
end;
:: Moved from JORDAN, AG 20.01.2006
theorem
W-bound C = W-bound North_Arc C
proof
A1: W-min C in North_Arc C by Th29;
North_Arc C c= C by Th35;
hence thesis by A1,JORDAN1J:65;
end;
theorem
E-bound C = E-bound North_Arc C
proof
A1: E-max C in North_Arc C by Th30;
North_Arc C c= C by Th35;
hence thesis by A1,JORDAN1J:66;
end;
theorem
W-bound C = W-bound South_Arc C
proof
A1: W-min C in South_Arc C by Th31;
South_Arc C c= C by Th36;
hence thesis by A1,JORDAN1J:65;
end;
theorem
E-bound C = E-bound South_Arc C
proof
A1: E-max C in South_Arc C by Th32;
South_Arc C c= C by Th36;
hence thesis by A1,JORDAN1J:66;
end;
~~