:: Preparing the Internal Approximations of Simple Closed Curves
:: by Andrzej Trybulec
::
:: Received May 21, 2002
:: Copyright (c) 2002-2026 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, SUBSET_1, TOPREAL2, EUCLID, XXREAL_0, CARD_1, TREES_1,
JORDAN8, RLTOPSP1, RELAT_1, JORDAN1A, XBOOLE_0, JORDAN6, TOPREAL1,
JORDAN9, TARSKI, PRE_TOPC, GOBOARD9, JORDAN1H, ARYTM_3, FINSEQ_1,
MATRIX_1, JORDAN1E, CONNSP_1, PSCOMP_1, INT_1, MCART_1, FUNCT_1, SEQ_4,
SEQ_1, RCOMP_1, STRUCT_0, REAL_1, ZFMISC_1, RELAT_2, XXREAL_2, XXREAL_1,
JORDAN10, JORDAN2C, SETFAM_1, GOBOARD5, ARYTM_1, NEWTON, METRIC_1,
JORDAN11, MEASURE5, CONVEX1, FUNCT_7, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_D, NEWTON, XXREAL_2, SEQ_4,
FUNCT_1, RELSET_1, FUNCT_2, NAT_1, FINSEQ_1, MATRIX_0, SEQ_1, RCOMP_1,
STRUCT_0, PRE_TOPC, METRIC_1, METRIC_6, CONNSP_1, COMPTS_1, RLTOPSP1,
EUCLID, TOPREAL1, TOPREAL2, GOBOARD5, GOBOARD9, PSCOMP_1, JORDAN2C,
JORDAN6, JORDAN8, JORDAN9, JORDAN10, JORDAN1A, JORDAN1E, JORDAN1H,
TOPREAL6, JORDAN1K;
constructors REAL_1, NAT_D, RCOMP_1, NEWTON, BINARITH, TOPS_1, CONNSP_1,
TBSP_1, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6,
JORDAN1K, JORDAN8, JORDAN9, JORDAN10, JORDAN1A, JORDAN1E, JORDAN1H,
SEQ_4, CONVEX1, GOBOARD1;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, MEMBERED, STRUCT_0, COMPTS_1, TBSP_1, EUCLID, TOPREAL1, TOPREAL2,
SPPOL_2, PSCOMP_1, TOPREAL5, SPRECT_2, JORDAN6, JORDAN2C, TOPREAL6,
JORDAN8, JORDAN10, XXREAL_2, JORDAN, RLTOPSP1, JORDAN1, JORDAN5A, NEWTON;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, JORDAN1H;
equalities XBOOLE_0, JORDAN1H, PSCOMP_1, SUBSET_1;
expansions TARSKI, XBOOLE_0, JORDAN1H;
theorems SEQ_4, JORDAN8, NEWTON, NAT_1, GOBOARD7, GOBOARD5, XBOOLE_0,
XBOOLE_1, JORDAN2C, SUBSET_1, GOBOARD9, ZFMISC_1, EUCLID, JORDAN6,
PSCOMP_1, SPRECT_1, TARSKI, TOPREAL3, SETFAM_1, RCOMP_1, RELAT_1,
FUNCT_2, TOPREAL1, PRE_TOPC, JORDAN1A, ENUMSET1, FUNCT_1, JCT_MISC,
JORDAN10, GOBRD14, JORDAN1B, JORDAN1C, JORDAN1F, JORDAN1G, JORDAN1H,
JORDAN1I, JORDAN1J, PREPOWER, XREAL_1, JORDAN1K, METRIC_6, WEIERSTR,
JORDAN9, XXREAL_0, JORDAN1, INT_1, MATRIX_0, XXREAL_2, NAT_D, RLTOPSP1,
ORDINAL1;
schemes DOMAIN_1, FUNCT_2;
begin
reserve i,j,k,n for Nat,
C for being_simple_closed_curve Subset of TOP-REAL 2;
Lm1: i > 0 & 1 <= j & j <= width Gauge(C,i) & k <= j & 1 <= k & k <= width
Gauge(C,i) & LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i
),k)) /\ Upper_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),j)} & LSeg(
Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) /\ Lower_Arc
L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),k)} implies LSeg(Gauge(C,i)*(
Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),k)) c= Cl RightComp Cage(C,i
)
proof
assume that
A1: i > 0 and
A2: 1 <= j and
A3: j <= width Gauge(C,i) and
A4: k <= j and
A5: 1 <= k and
A6: k <= width Gauge(C,i) and
A7: LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),
k)) /\ Upper_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),j)} and
A8: LSeg(Gauge(C,i)*(Center Gauge(C,i),j),Gauge(C,i)*(Center Gauge(C,i),
k)) /\ Lower_Arc L~Cage(C,i) = {Gauge(C,i)*(Center Gauge(C,i),k)};
set p = Gauge(C,i)*(Center Gauge(C,i),j), q = Gauge(C,i)*(Center Gauge(C,i),
k), S = RightComp Cage(C,i);
A9: {q} c= Lower_Arc L~Cage(C,i) by A8,XBOOLE_1:17;
A10: X-SpanStart(C,i) = Center Gauge(C,i) by JORDAN1B:16;
then
A11: 1 < Center Gauge(C,i) by JORDAN1H:49,XXREAL_0:2;
A12: Center Gauge(C,i) < len Gauge(C,i) by A10,JORDAN1H:49;
then
A13: [Center Gauge(C,i),j] in Indices Gauge(C,i) by A2,A3,A11,MATRIX_0:30;
p in {p} by TARSKI:def 1;
then p in Upper_Arc L~Cage(C,i) by A7,XBOOLE_0:def 4;
then
A14: p in L~Upper_Seq(C,i) by A1,JORDAN1G:55;
A15: [Center Gauge(C,i),k] in Indices Gauge(C,i) by A5,A6,A11,A12,MATRIX_0:30;
q in {q} by TARSKI:def 1;
then q in Lower_Arc L~Cage(C,i) by A8,XBOOLE_0:def 4;
then q in L~Lower_Seq(C,i) by A1,JORDAN1G:56;
then j <> k by A2,A6,A11,A12,A14,JORDAN1J:57;
then
A16: p <> q by A13,A15,JORDAN1H:26;
set A = LSeg(p,q) \ {p,q};
LSeg(p,q) /\ L~Cage(C,i) = LSeg(p,q) /\ (Upper_Arc L~Cage(C,i) \/
Lower_Arc L~Cage(C,i)) by JORDAN6:50
.= LSeg(p,q) /\ Upper_Arc L~Cage(C,i) \/ LSeg(p,q) /\ Lower_Arc L~Cage(C
,i) by XBOOLE_1:23
.= {p,q} by A7,A8,ENUMSET1:1;
then A misses L~Cage(C,i) by XBOOLE_1:90;
then
A17: A c= (L~Cage(C,i))` by SUBSET_1:23;
A18: C c= S by JORDAN10:11;
LSeg(q,p) meets Upper_Arc C by A1,A3,A4,A5,A7,A8,A11,A12,JORDAN1J:61;
then
A19: LSeg(q,p) meets C by JORDAN6:61,XBOOLE_1:63;
{p} c= Upper_Arc L~Cage(C,i) by A7,XBOOLE_1:17;
then {p} \/ {q} c= Upper_Arc L~Cage(C,i) \/ Lower_Arc L~Cage(C,i) by A9,
XBOOLE_1:13;
then {p} \/ {q} c= L~Cage(C,i) by JORDAN6:50;
then
A20: {p,q} c= L~Cage(C,i) by ENUMSET1:1;
L~Cage(C,i) misses C by JORDAN10:5;
then {p,q} misses C by A20,XBOOLE_1:63;
then
A21: A meets C by A19,XBOOLE_1:84;
A22: A is convex by JORDAN1:46;
S is_a_component_of (L~Cage(C,i))` by GOBOARD9:def 2;
then A c= S by A17,A21,A18,A22,GOBOARD9:4;
hence thesis by A16,JORDAN1H:3;
end;
Lm2: ex n st n is_sufficiently_large_for C
proof
set s = (W-bound C + E-bound C)/2, e = Gauge(C,1)*(X-SpanStart(C,1),len
Gauge(C,1)), f = Gauge(C,1)*(X-SpanStart(C,1),1);
A1: len Gauge(C,1) = width Gauge(C,1) by JORDAN8:def 1;
A2: X-SpanStart(C,1) = Center Gauge(C,1) by JORDAN1B:16;
then X-SpanStart(C,1) = (len Gauge(C,1)) div 2 + 1 by JORDAN1A:def 1;
then
A3: 1 <= X-SpanStart(C,1) by NAT_1:11;
len Gauge(C,1) >= 4 by JORDAN8:10;
then
A4: 1 < len Gauge(C,1) by XXREAL_0:2;
then
A5: f`1 = s by A2,JORDAN1A:38;
then
A6: f in Vertical_Line s by JORDAN1A:8;
0 < len Gauge(C,1) by JORDAN8:10;
then len Gauge(C,1) qua Integer div 2 < len Gauge(C,1) by INT_1:56;
then (len Gauge(C,1)) div 2 + 1 <= len Gauge(C,1) by NAT_1:13;
then X-SpanStart(C,1) <= len Gauge(C,1) by A2,JORDAN1A:def 1;
then
A7: f`2 < e`2 by A3,A4,A1,GOBOARD5:4;
set e1 = proj2.e, f1 = proj2.f;
A8: proj2.e = e`2 by PSCOMP_1:def 6;
4 <= len Gauge (C,1) by JORDAN8:10;
then
A9: 1 <= len Gauge (C,1) by XXREAL_0:2;
set AA = LSeg(e,f) /\ Upper_Arc C, BB = LSeg(e,f) /\ Lower_Arc C;
deffunc F(Nat)=
In(lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,$1+1))),REAL);
consider Es being Real_Sequence such that
A10: for i being Element of NAT holds Es.i = F(i) from FUNCT_2:sch 4;
reconsider A = proj2.:AA, B = proj2.:BB as compact Subset of REAL by
JCT_MISC:15;
deffunc G(Element of NAT)=|[s,Es.$1]|;
consider E being sequence of the carrier of TOP-REAL 2 such that
A11: for i being Element of NAT holds E.i = G(i) from FUNCT_2:sch 4;
A12: e`1 = s by A2,A4,JORDAN1A:38;
then e in Vertical_Line s by JORDAN1A:8;
then
A13: LSeg(e,f) c= Vertical_Line s by A6,JORDAN1A:13;
A14: A misses B
proof
assume A meets B;
then consider z being object such that
A15: z in A and
A16: z in B by XBOOLE_0:3;
reconsider z as Real by A15;
consider p being Point of TOP-REAL 2 such that
A17: p in AA and
A18: z = proj2.p by A15,FUNCT_2:65;
A19: p in Upper_Arc C by A17,XBOOLE_0:def 4;
consider q being Point of TOP-REAL 2 such that
A20: q in BB and
A21: z = proj2.q by A16,FUNCT_2:65;
A22: p`2 = proj2.q by A18,A21,PSCOMP_1:def 6
.= q`2 by PSCOMP_1:def 6;
A23: q in Lower_Arc C by A20,XBOOLE_0:def 4;
A24: q in LSeg(e,f) by A20,XBOOLE_0:def 4;
A25: p in LSeg(e,f) by A17,XBOOLE_0:def 4;
then p`1 = s by A13,JORDAN6:31
.= q`1 by A13,A24,JORDAN6:31;
then p = q by A22,TOPREAL3:6;
then p in Upper_Arc C /\ Lower_Arc C by A19,A23,XBOOLE_0:def 4;
then
A26: p in {W-min C,E-max C } by JORDAN6:50;
per cases by A26,TARSKI:def 2;
suppose
A27: p = W-min C;
A28: (W-min C)`1 = W-bound C by EUCLID:52;
(W-min C)`1 = s by A13,A25,A27,JORDAN6:31;
hence contradiction by A28,SPRECT_1:31;
end;
suppose
A29: p = E-max C;
A30: (E-max C)`1 = E-bound C by EUCLID:52;
(E-max C)`1 = s by A13,A25,A29,JORDAN6:31;
hence contradiction by A30,SPRECT_1:31;
end;
end;
deffunc H(Nat) =
In(upper_bound(proj2.:(LSeg(f,E.$1) /\ Lower_Arc L~Cage(C,$1+1))),REAL);
consider Fs being Real_Sequence such that
A31: for i being Element of NAT holds Fs.i = H(i) from FUNCT_2:sch 4;
deffunc I(Element of NAT)=|[s,Fs.$1]|;
consider F being sequence of the carrier of TOP-REAL 2 such that
A32: for i being Element of NAT holds F.i = I(i) from FUNCT_2:sch 4;
deffunc F1(Nat)=proj2.:LSeg(E.$1,F.$1);
consider S being sequence of bool REAL such that
A33: for i being Element of NAT holds S.i = F1(i) from FUNCT_2:sch 4;
A34: for i holds E.i in Upper_Arc L~Cage(C,i+1)
proof
let i be Nat;
set p = E.i;
A35: i+1 >= 1 by NAT_1:11;
reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1) as compact Subset of
TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A36: dom proj2 /\ DD = DD by XBOOLE_1:28;
A37: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1B:16;
then
LSeg(Gauge(C,i+1)*(X-SpanStart(C,i+1),1), Gauge(C,i+1)*(X-SpanStart(C
,i+1),len Gauge(C,i+1))) meets Upper_Arc L~Cage(C,i+1) by JORDAN1B:31;
then LSeg(f,e) meets Upper_Arc L~Cage(C,i+1) by A2,A37,A35,JORDAN1A:44
,XBOOLE_1:63;
then DD <> {};
then dom proj2 meets DD by A36;
then
A38: D <> {} by RELAT_1:118;
A39: i in NAT by ORDINAL1:def 12;
then Es.i = F(i) by A10;
then consider dd being Point of TOP-REAL 2 such that
A40: dd in DD and
A41: Es.i = proj2.dd by A38,FUNCT_2:65,RCOMP_1:14;
A42: dd in LSeg(e,f) by A40,XBOOLE_0:def 4;
A43: E.i = |[s,Es.i]| by A11,A39;
then p`2 = Es.i by EUCLID:52;
then
A44: dd`2 = p`2 by A41,PSCOMP_1:def 6;
p`1 = s by A43,EUCLID:52;
then
A45: dd`1 = p`1 by A13,A42,JORDAN6:31;
dd in Upper_Arc L~Cage(C,i+1) by A40,XBOOLE_0:def 4;
hence thesis by A45,A44,TOPREAL3:6;
end;
A46: for i holds F.i in Lower_Arc L~Cage(C,i+1)
proof
let i;
set p = F.i;
A47: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1B:16;
reconsider DD = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset
of TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
A48: E.i in Upper_Arc L~Cage(C,i+1) by A34;
A49: i in NAT by ORDINAL1:def 12;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A50: dom proj2 /\ DD = DD by XBOOLE_1:28;
A51: E.i = |[s,Es.i]| by A11,A49;
then
A52: (E.i)`1 = s by EUCLID:52;
then E.i in Vertical_Line s by JORDAN1A:8;
then
A53: LSeg(E.i,f) c= Vertical_Line s by A6,JORDAN1A:13;
(E.i)`2 = Es.i by A51,EUCLID:52
.= F(i) by A10,A49
.= lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1)));
then ex j st 1 <= j & j <= width Gauge(C,i+1) & E.i = Gauge(C,i+1)*(
X-SpanStart(C,i+1),j) by A2,A1,A47,A52,JORDAN1F:13;
then LSeg(f,E.i) meets Lower_Arc L~Cage(C,i+1) by A2,A47,A48,JORDAN1J:62;
then DD <> {};
then dom proj2 meets DD by A50;
then
A54: D <> {} by RELAT_1:118;
A55: i in NAT by ORDINAL1:def 12;
Fs.i = H(i) by A31,A55;
then consider dd being Point of TOP-REAL 2 such that
A56: dd in DD and
A57: Fs.i = proj2.dd by A54,FUNCT_2:65,RCOMP_1:14;
A58: dd in Lower_Arc L~Cage(C,i+1) by A56,XBOOLE_0:def 4;
A59: F.i = |[s,Fs.i]| by A32,A55;
then p`2 = Fs.i by EUCLID:52;
then
A60: dd`2 = p`2 by A57,PSCOMP_1:def 6;
A61: dd in LSeg(E.i,f) by A56,XBOOLE_0:def 4;
p`1 = s by A59,EUCLID:52;
then dd`1 = p`1 by A61,A53,JORDAN6:31;
hence thesis by A58,A60,TOPREAL3:6;
end;
A62: for i being Nat holds S.i qua Subset of REAL is interval &
S.i meets A & S.i meets B
proof
let i be Nat;
reconsider DD = LSeg(e,f) /\ Upper_Arc L~Cage(C,i+1) as compact Subset of
TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
A63: X-SpanStart(C,i+1) = Center Gauge(C,i+1) by JORDAN1B:16;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A64: dom proj2 /\ DD = DD by XBOOLE_1:28;
A65: 1 <= i+1 by NAT_1:11;
A66: i in NAT by ORDINAL1:def 12;
LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),1), Gauge(C,i+1)*(Center
Gauge(C,i+1),len Gauge(C,i+1))) meets Upper_Arc L~Cage(C,i+1) by JORDAN1B:31;
then LSeg(f,e) meets Upper_Arc L~Cage(C,i+1) by A2,A65,JORDAN1A:44
,XBOOLE_1:63;
then DD <> {};
then dom proj2 meets DD by A64;
then
A67: D <> {} by RELAT_1:118;
Es.i = F(i) by A10,A66;
then consider dd being Point of TOP-REAL 2 such that
A68: dd in DD and
A69: Es.i = proj2.dd by A67,FUNCT_2:65,RCOMP_1:14;
A70: dd in LSeg(f,e) by A68,XBOOLE_0:def 4;
reconsider DD = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset
of TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A71: dom proj2 /\ DD = DD by XBOOLE_1:28;
A72: i in NAT by ORDINAL1:def 12;
A73: E.i = |[s,Es.i]| by A11,A72;
then
A74: (E.i)`1 = s by EUCLID:52;
A75: F.i = |[s,Fs.i]| by A32,A72;
then
A76: (F.i)`1 = s by EUCLID:52;
A77: (F.i)`2 =Fs.i by A75,EUCLID:52
.= H(i) by A31,A72
.= upper_bound(proj2.:(LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1)));
(E.i)`2 = Es.i by A73,EUCLID:52
.= F(i) by A10,A72
.= lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1)));
then consider j such that
A78: 1 <= j and
A79: j <= width Gauge(C,i+1) and
A80: E.i = Gauge(C,i+1)*(X-SpanStart(C,i+1),j) by A2,A1,A74,A63,JORDAN1F:13;
A81: E.i in Upper_Arc L~Cage(C,i+1) by A34;
then consider k such that
A82: 1 <= k and
A83: k <= width Gauge(C,i+1) and
A84: F.i = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by A2,A63,A76,A78,A79,A80,A77,
JORDAN1I:28;
A85: i in NAT by ORDINAL1:def 12;
(E.i)`2 = Es.i by A73,EUCLID:52
.= F(i) by A10,A85
.= lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1)));
then ex j st 1 <= j & j <= width Gauge(C,i+1) & E.i = Gauge(C,i+1)*(
X-SpanStart(C,i+1),j) by A2,A1,A74,A63,JORDAN1F:13;
then LSeg(f,E.i) meets Lower_Arc L~Cage(C,i+1) by A2,A63,A81,JORDAN1J:62;
then DD <> {};
then dom proj2 meets DD by A71;
then
A86: D <> {} by RELAT_1:118;
A87: (E.i)`2 = Es.i by A73,EUCLID:52
.= dd`2 by A69,PSCOMP_1:def 6;
for p being Real st p in D holds p <= (E.i)`2
proof
let p be Real;
assume p in D;
then consider x being object such that
x in dom proj2 and
A88: x in DD and
A89: p = proj2.x by FUNCT_1:def 6;
A90: f`2 <= (E.i)`2 by A7,A70,A87,TOPREAL1:4;
reconsider x as Point of TOP-REAL 2 by A88;
x in LSeg(f,E.i) by A88,XBOOLE_0:def 4;
then x`2 <= (E.i)`2 by A90,TOPREAL1:4;
hence thesis by A89,PSCOMP_1:def 6;
end;
then
A91: upper_bound D <= (E.i)`2 by A86,SEQ_4:45;
dd`1 = (E.i)`1 by A13,A74,A70,JORDAN6:31;
then
A92: E.i in LSeg(e,f) by A70,A87,TOPREAL3:6;
Fs.i = H(i) by A31,A85;
then consider dd being Point of TOP-REAL 2 such that
A93: dd in DD and
A94: Fs.i = proj2.dd by A86,FUNCT_2:65,RCOMP_1:14;
A95: (F.i)`2 = Fs.i by A75,EUCLID:52
.= dd`2 by A94,PSCOMP_1:def 6;
A96: dd in LSeg(E.i,f) by A93,XBOOLE_0:def 4;
E.i in Vertical_Line s by A74,JORDAN1A:8;
then LSeg(E.i,f) c= Vertical_Line s by A6,JORDAN1A:13;
then dd`1 = (F.i)`1 by A76,A96,JORDAN6:31;
then
A97: F.i in LSeg(E.i,f) by A96,A95,TOPREAL3:6;
f in LSeg(e,f) by RLTOPSP1:68;
then LSeg(f,E.i) c= LSeg(e,f) by A92,TOPREAL1:6;
then
A98: LSeg(E.i,F.i) c= LSeg(e,f) by A92,A97,TOPREAL1:6;
A99: for x be set holds x in LSeg(E.i,F.i) /\ Upper_Arc L~Cage(C,i+1)
implies x = E.i
proof
let x be set;
reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,i+1) as compact Subset
of TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
assume
A100: x in LSeg(E.i,F.i) /\ Upper_Arc L~Cage(C,i+1);
then reconsider p = x as Point of TOP-REAL 2;
A101: p in LSeg(E.i,F.i) by A100,XBOOLE_0:def 4;
A102: i in NAT by ORDINAL1:def 12;
p in Upper_Arc L~Cage(C,i+1) by A100,XBOOLE_0:def 4;
then p in DD by A98,A101,XBOOLE_0:def 4;
then proj2.p in D by FUNCT_2:35;
then
A103: p`2 in D by PSCOMP_1:def 6;
E.i = |[s,Es.i]| by A11,A102;
then
A104: (E.i)`2 = Es.i by EUCLID:52
.= F(i) by A10,A102
.= lower_bound D;
D is real-bounded by RCOMP_1:10;
then
A105: (E.i)`2 <= p`2 by A104,A103,SEQ_4:def 2;
p`2 <= (E.i)`2 by A77,A91,A101,TOPREAL1:4;
then
A106: p`2 = (E.i)`2 by A105,XXREAL_0:1;
p`1 = (E.i)`1 by A74,A76,A101,GOBOARD7:5;
hence thesis by A106,TOPREAL3:6;
end;
A107: Gauge(C,i+1)*(Center Gauge(C,i+1),j) in LSeg(Gauge(C,i+1)*(Center
Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) by RLTOPSP1:68;
A108: LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center
Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1) = {Gauge(C,i+1)*(Center Gauge(C,i+1
),j)}
proof
thus LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center
Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1) c= {Gauge(C,i+1)*(Center Gauge(C,i+
1),j)}
proof
let x be object;
assume x in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)
*(Center Gauge(C,i+1),j)) /\ Upper_Arc L~Cage(C,i+1);
then x = Gauge(C,i+1)*(Center Gauge(C,i+1),j) by A63,A80,A84,A99;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {Gauge(C,i+1)*(Center Gauge(C,i+1),j)};
then x = Gauge(C,i+1)*(Center Gauge(C,i+1),j) by TARSKI:def 1;
hence thesis by A63,A81,A80,A107,XBOOLE_0:def 4;
end;
E.i in LSeg(E.i,f) by RLTOPSP1:68;
then
A109: LSeg(E.i,F.i) c= LSeg(E.i,f) by A97,TOPREAL1:6;
A110: for x be set holds x in LSeg(E.i,F.i) /\ Lower_Arc L~Cage(C,i+1)
implies x = F.i
proof
let x be set;
reconsider EE = LSeg(f,E.i) /\ Lower_Arc L~Cage(C,i+1) as compact Subset
of TOP-REAL 2;
reconsider E0 = proj2.:EE as compact Subset of REAL by JCT_MISC:15;
assume
A111: x in LSeg(E.i,F.i) /\ Lower_Arc L~Cage(C,i+1);
then reconsider p = x as Point of TOP-REAL 2;
A112: p in LSeg(E.i,F.i) by A111,XBOOLE_0:def 4;
A113: i in NAT by ORDINAL1:def 12;
p in Lower_Arc L~Cage(C,i+1) by A111,XBOOLE_0:def 4;
then p in EE by A109,A112,XBOOLE_0:def 4;
then proj2.p in E0 by FUNCT_2:35;
then
A114: p`2 in E0 by PSCOMP_1:def 6;
F.i = |[s,Fs.i]| by A32,A113;
then
A115: (F.i)`2 = Fs.i by EUCLID:52
.= H(i) by A31,A113
.= upper_bound E0;
E0 is real-bounded by RCOMP_1:10;
then
A116: (F.i)`2 >= p`2 by A115,A114,SEQ_4:def 1;
p`2 >= (F.i)`2 by A77,A91,A112,TOPREAL1:4;
then
A117: p`2 = (F.i)`2 by A116,XXREAL_0:1;
p`1 = (F.i)`1 by A74,A76,A112,GOBOARD7:5;
hence thesis by A117,TOPREAL3:6;
end;
A118: F.i in Lower_Arc L~Cage(C,i+1) by A46;
A119: S.i = proj2.:LSeg(E.i,F.i) by A33,A85;
hence S.i is interval by JCT_MISC:6;
A120: Center Gauge(C,i+1) <= len Gauge(C,i+1) by JORDAN1B:13;
A121: Gauge(C,i+1)*(Center Gauge(C,i+1),k) in LSeg(Gauge(C,i+1)*(Center
Gauge(C,i+1),k), Gauge(C,i+1)*(Center Gauge(C,i+1),j)) by RLTOPSP1:68;
A122: LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center
Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1) = {Gauge(C,i+1)*(Center Gauge(C,i+1
),k)}
proof
thus LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)*(Center
Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1) c= {Gauge(C,i+1)*(Center Gauge(C,i+
1),k)}
proof
let x be object;
assume x in LSeg(Gauge(C,i+1)*(Center Gauge(C,i+1),k), Gauge(C,i+1)
*(Center Gauge(C,i+1),j)) /\ Lower_Arc L~Cage(C,i+1);
then x = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by A63,A80,A84,A110;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {Gauge(C,i+1)*(Center Gauge(C,i+1),k)};
then x = Gauge(C,i+1)*(Center Gauge(C,i+1),k) by TARSKI:def 1;
hence thesis by A84,A118,A121,XBOOLE_0:def 4;
end;
1 <= Center Gauge(C,i+1) by JORDAN1B:11;
then
A123: k <= j by A63,A78,A80,A77,A83,A84,A120,A91,GOBOARD5:4;
then LSeg(E.i,F.i) meets AA by A63,A98,A79,A80,A82,A84,A108,A122,
JORDAN1J:64,XBOOLE_1:77;
hence S.i meets A by A119,JORDAN1A:14;
LSeg(E.i,F.i) meets BB by A63,A98,A79,A80,A82,A84,A123,A108,A122,
JORDAN1J:63,XBOOLE_1:77;
hence thesis by A119,JORDAN1A:14;
end;
proj2.f = f`2 by PSCOMP_1:def 6;
then
A124: proj2.:LSeg(f,e) = [.f1,e1.] by A7,A8,SPRECT_1:53;
then
A125: B c= [.f1,e1.] by RELAT_1:123,XBOOLE_1:17;
A c= [.f1,e1.] by A124,RELAT_1:123,XBOOLE_1:17;
then consider r being Real such that
A126: r in [.f1,e1.] and
A127: not r in A \/ B and
A128: for i being Nat ex k being Nat st i <= k & r
in S.k by A14,A125,A62,JCT_MISC:12;
reconsider r as Real;
set p = |[s,r]|;
A129: p`1 = s by EUCLID:52;
for Y being set st Y in BDD-Family C holds p in Y
proof
let Y be set;
A130: BDD-Family C = the set of all Cl BDD L~Cage(C,k1) where k1 is Nat
by JORDAN10:def 2;
assume Y in BDD-Family C;
then consider k1 being Nat such that
A131: Y = Cl BDD L~Cage(C,k1) by A130;
consider k0 being Nat such that
A132: k1 <= k0 and
A133: r in S.k0 by A128;
A134: proj2.(F.k0) = (F.k0)`2 by PSCOMP_1:def 6;
reconsider EE = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset
of TOP-REAL 2;
reconsider CC = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset
of TOP-REAL 2;
reconsider W = proj2.:CC as compact Subset of REAL by JCT_MISC:15;
A135: Center Gauge(C,k0+1) <= len Gauge(C,k0+1) by JORDAN1B:13;
reconsider E0 = proj2.:EE as compact Subset of REAL by JCT_MISC:15;
CC c= the carrier of TOP-REAL 2;
then CC c= dom proj2 by FUNCT_2:def 1;
then
A136: dom proj2 /\ CC = CC by XBOOLE_1:28;
A137: RightComp Cage(C,k0+1) c= RightComp Cage(C,k0) by JORDAN1H:48,NAT_1:11;
RightComp Cage(C,k0) c= RightComp Cage(C,k1) by A132,JORDAN1H:48;
then RightComp Cage(C,k0+1) c= RightComp Cage(C,k1) by A137;
then
A138: Cl RightComp Cage(C,k0+1) c= Cl RightComp Cage(C,k1) by PRE_TOPC:19;
A139: E.k0 in Upper_Arc L~Cage(C,k0+1) by A34;
A140: 1+0 <= k0+1 by NAT_1:11;
A141: E.k0 in Upper_Arc L~Cage(C,k0+1) by A34;
A142: X-SpanStart(C,k0+1) = Center Gauge(C,k0+1) by JORDAN1B:16;
reconsider DD = LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1) as compact Subset
of TOP-REAL 2;
A143: proj2.(E.k0) = (E.k0)`2 by PSCOMP_1:def 6;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
A144: k0 in NAT by ORDINAL1:def 12;
A145: Fs.k0 = H(k0) by A31,A144
.= upper_bound D;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A146: dom proj2 /\ DD = DD by XBOOLE_1:28;
A147: E.k0 = |[s,Es.k0]| by A11,A144;
then
A148: (E.k0)`1 = s by EUCLID:52;
(E.k0)`2 = Es.k0 by A147,EUCLID:52
.= F(k0) by A10,A144
.= lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1)));
then ex j st 1 <= j & j <= width Gauge(C,k0+1) & E.k0 = Gauge (C,k0+1)
*(X-SpanStart(C,k0+1),j) by A2,A1,A148,A142,JORDAN1F:13;
then
A149: LSeg(f,E.k0) meets Lower_Arc L~Cage(C,k0+1) by A2,A142,A141,JORDAN1J:62;
then DD <> {};
then dom proj2 meets DD by A146;
then D <> {} by RELAT_1:118;
then consider dd being Point of TOP-REAL 2 such that
A150: dd in DD and
A151: Fs.k0 = proj2.dd by A145,FUNCT_2:65,RCOMP_1:14;
A152: dd in LSeg(E.k0,f) by A150,XBOOLE_0:def 4;
reconsider DD = LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1) as compact Subset of
TOP-REAL 2;
reconsider D = proj2.:DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of TOP-REAL 2;
then DD c= dom proj2 by FUNCT_2:def 1;
then
A153: dom proj2 /\ DD = DD by XBOOLE_1:28;
LSeg(Gauge(C,k0+1)*(Center Gauge(C,k0+1),1), Gauge(C,k0+1)*(Center
Gauge(C,k0+1),len Gauge(C,k0+1))) meets Upper_Arc L~Cage(C,k0+1) by JORDAN1B:31
;
then LSeg(f,e) meets Upper_Arc L~Cage(C,k0+1) by A2,A140,JORDAN1A:44
,XBOOLE_1:63;
then DD <> {};
then dom proj2 meets DD by A153;
then
A154: D <> {} by RELAT_1:118;
A155: F.k0 = |[s,Fs.k0]| by A32,A144;
then
A156: (F.k0)`1 = s by EUCLID:52;
A157: (F.k0)`2 = Fs.k0 by A155,EUCLID:52
.= dd`2 by A151,PSCOMP_1:def 6;
E.k0 in Vertical_Line s by A148,JORDAN1A:8;
then LSeg(E.k0,f) c= Vertical_Line s by A6,JORDAN1A:13;
then dd`1 = (F.k0)`1 by A156,A152,JORDAN6:31;
then
A158: F.k0 in LSeg(E.k0,f) by A152,A157,TOPREAL3:6;
Es.k0 = F(k0) by A10,A144;
then consider dd being Point of TOP-REAL 2 such that
A159: dd in DD and
A160: Es.k0 = proj2.dd by A154,FUNCT_2:65,RCOMP_1:14;
A161: dd in LSeg(f,e) by A159,XBOOLE_0:def 4;
A162: (E.k0)`2 = Es.k0 by A147,EUCLID:52
.= dd`2 by A160,PSCOMP_1:def 6;
then
A163: f`2 <= (E.k0)`2 by A7,A161,TOPREAL1:4;
then
A164: (F.k0)`2 <= (E.k0)`2 by A152,A157,TOPREAL1:4;
r in proj2.:LSeg(E.k0,F.k0) by A33,A133,A144;
then r in [.proj2.(F.k0),proj2.(E.k0).] by A143,A134,A164,SPRECT_1:53;
then
A165: p in LSeg(E.k0,F.k0) by A148,A156,JORDAN1A:11;
A166: F.k0 in Lower_Arc L~Cage(C,k0+1) by A46;
A167: f in LSeg(f,e) by RLTOPSP1:68;
A168: E.k0 in LSeg(f,E.k0) by RLTOPSP1:68;
then
A169: LSeg(E.k0,F.k0) c= LSeg(f,E.k0) by A158,TOPREAL1:6;
for x being object holds x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+
1) iff x = F.k0
proof
let x be object;
thus x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) implies x = F.k0
proof
F.k0 = |[s,Fs.k0]| by A32,A144;
then
A170: (F.k0)`2 = Fs.k0 by EUCLID:52
.= H(k0) by A31,A144;
assume
A171: x in LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1);
then reconsider p = x as Point of TOP-REAL 2;
A172: p in LSeg(E.k0,F.k0) by A171,XBOOLE_0:def 4;
then
A173: p`2 >= (F.k0)`2 by A164,TOPREAL1:4;
p in Lower_Arc L~Cage(C,k0+1) by A171,XBOOLE_0:def 4;
then p in EE by A169,A172,XBOOLE_0:def 4;
then proj2.p in E0 by FUNCT_2:35;
then
A174: p`2 in E0 by PSCOMP_1:def 6;
E0 is real-bounded by RCOMP_1:10;
then (F.k0)`2 >= p`2 by A170,A174,SEQ_4:def 1;
then
A175: p`2 = (F.k0)`2 by A173,XXREAL_0:1;
p`1 = (F.k0)`1 by A148,A156,A172,GOBOARD7:5;
hence thesis by A175,TOPREAL3:6;
end;
assume
A176: x = F.k0;
then x in LSeg(E.k0,F.k0) by RLTOPSP1:68;
hence thesis by A166,A176,XBOOLE_0:def 4;
end;
then
A177: LSeg(E.k0,F.k0) /\ Lower_Arc L~Cage(C,k0+1) = {F.k0} by TARSKI:def 1;
A178: for p being Real st p in W holds p <= (E.k0)`2
proof
let p be Real;
assume p in W;
then consider x being object such that
x in dom proj2 and
A179: x in CC and
A180: p = proj2.x by FUNCT_1:def 6;
reconsider x as Point of TOP-REAL 2 by A179;
x in LSeg(f,E.k0) by A179,XBOOLE_0:def 4;
then x`2 <= (E.k0)`2 by A163,TOPREAL1:4;
hence thesis by A180,PSCOMP_1:def 6;
end;
CC <> {} by A149;
then dom proj2 meets CC by A136;
then W <> {} by RELAT_1:118;
then
A181: upper_bound W <= (E.k0)`2 by A178,SEQ_4:45;
dd`1 = (E.k0)`1 by A13,A148,A161,JORDAN6:31;
then E.k0 in LSeg(f,e) by A161,A162,TOPREAL3:6;
then LSeg(f,E.k0) c= LSeg(e,f) by A167,TOPREAL1:6;
then
A182: LSeg(E.k0,F.k0) c= LSeg(e,f) by A158,A168,TOPREAL1:6;
for x being object holds x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+
1) iff x = E.k0
proof
let x be object;
thus x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) implies x = E.k0
proof
E.k0 = |[s,Es.k0]| by A11,A144;
then
A183: (E.k0)`2 = Es.k0 by EUCLID:52
.= F(k0) by A10,A144;
assume
A184: x in LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1);
then reconsider p = x as Point of TOP-REAL 2;
A185: p in LSeg(E.k0,F.k0) by A184,XBOOLE_0:def 4;
then
A186: p`2 <= (E.k0)`2 by A164,TOPREAL1:4;
p in Upper_Arc L~Cage(C,k0+1) by A184,XBOOLE_0:def 4;
then p in DD by A182,A185,XBOOLE_0:def 4;
then proj2.p in D by FUNCT_2:35;
then
A187: p`2 in D by PSCOMP_1:def 6;
D is real-bounded by RCOMP_1:10;
then (E.k0)`2 <= p`2 by A183,A187,SEQ_4:def 2;
then
A188: p`2 = (E.k0)`2 by A186,XXREAL_0:1;
p`1 = (E.k0)`1 by A148,A156,A185,GOBOARD7:5;
hence thesis by A188,TOPREAL3:6;
end;
assume
A189: x = E.k0;
then x in LSeg(E.k0,F.k0) by RLTOPSP1:68;
hence thesis by A139,A189,XBOOLE_0:def 4;
end;
then
A190: LSeg(E.k0,F.k0) /\ Upper_Arc L~Cage(C,k0+1) = {E.k0} by TARSKI:def 1;
(E.k0)`2 = Es.k0 by A147,EUCLID:52
.= F(k0) by A10,A144
.= lower_bound(proj2.:(LSeg(f,e) /\ Upper_Arc L~Cage(C,k0+1)));
then consider j such that
A191: 1 <= j and
A192: j <= width Gauge(C,k0+1) and
A193: E.k0 = Gauge(C,k0+1)*(X-SpanStart(C,k0+1),j) by A2,A1,A148,A142,
JORDAN1F:13;
A194: (F.k0)`2 =Fs.k0 by A155,EUCLID:52
.= H(k0) by A31,A144
.= upper_bound(proj2.:(LSeg(f,E.k0) /\ Lower_Arc L~Cage(C,k0+1)));
then consider k such that
A195: 1 <= k and
A196: k <= width Gauge(C,k0+1) and
A197: F.k0 = Gauge(C,k0+1)*(X-SpanStart(C,k0+1),k) by A2,A156,A142,A191,A192
,A193,A139,JORDAN1I:28;
1 <= Center Gauge(C,k0+1) by JORDAN1B:11;
then k <= j by A142,A191,A193,A194,A196,A197,A135,A181,GOBOARD5:4;
then LSeg(E.k0,F.k0) c= Cl RightComp Cage(C,k0+1) by A142,A191,A192,A193
,A195,A196,A197,A190,A177,Lm1;
then p in Cl RightComp Cage(C,k0+1) by A165;
then p in Cl RightComp Cage(C,k1) by A138;
hence thesis by A131,GOBRD14:37;
end;
then
A198: p in meet BDD-Family C by SETFAM_1:def 1;
A199: p in LSeg(e,f) by A5,A12,A126,JORDAN1A:11;
A200: now
assume p in C;
then p in Lower_Arc C \/ Upper_Arc C by JORDAN6:50;
then p in (Lower_Arc C \/ Upper_Arc C) /\ LSeg(e,f) by A199,XBOOLE_0:def 4;
then p in AA \/ BB by XBOOLE_1:23;
then proj2.p in proj2.:(AA \/ BB) by FUNCT_2:35;
then r in proj2.:(AA \/ BB) by PSCOMP_1:65;
hence contradiction by A127,RELAT_1:120;
end;
meet BDD-Family C = C \/ BDD C by JORDAN10:21;
then p in BDD C by A200,A198,XBOOLE_0:def 3;
then consider n,i,j such that
A201: 1 < i and
A202: i < len Gauge(C,n) and
A203: 1 < j and
A204: j < width Gauge(C,n) and
A205: p`1 <> (Gauge(C,n)*(i,j))`1 and
A206: p in cell(Gauge(C,n),i,j) and
A207: cell(Gauge(C,n),i,j) c= BDD C by JORDAN1C:23;
take n,j;
thus j < width Gauge(C,n) by A204;
A208: X-SpanStart(C,n) = Center Gauge(C,n) by JORDAN1B:16;
A209: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A210: X-SpanStart(C,n) <= len Gauge(C,n) by JORDAN1H:49;
A211: 1 <= X-SpanStart(C,n) by JORDAN1H:49,XXREAL_0:2;
n > 0 by A202,A204,A207,JORDAN1B:41;
then (Gauge(C,n)*(X-SpanStart(C,n),j))`1 = s by A2,A5,A203,A204,A208,A9,A209,
JORDAN1A:36;
hence thesis by A129,A201,A202,A203,A204,A205,A206,A207,A211,A210,JORDAN1B:22
;
end;
definition
let C;
func ApproxIndex C -> Element of NAT means
:Def1:
it
is_sufficiently_large_for C & for j st j is_sufficiently_large_for C holds j >=
it;
existence
proof
defpred P[Nat] means $1 is_sufficiently_large_for C;
set X = {i where i is Element of NAT: P[i]};
A1: X is Subset of NAT from DOMAIN_1:sch 7;
consider i such that
A2: i is_sufficiently_large_for C by Lm2;
A3: i in NAT by ORDINAL1:def 12;
i in X by A2,A3;
then reconsider X as non empty Subset of NAT by A1;
take min X;
min X in X by XXREAL_2:def 7;
then ex i being Element of NAT
st i = min X & i is_sufficiently_large_for C;
hence min X is_sufficiently_large_for C;
let j;
A4: j in NAT by ORDINAL1:def 12;
assume j is_sufficiently_large_for C;
then j in X by A4;
hence thesis by XXREAL_2:def 7;
end;
uniqueness
proof
let it1,it2 be Element of NAT such that
A5: it1 is_sufficiently_large_for C and
A6: for j st j is_sufficiently_large_for C holds j >= it1 and
A7: it2 is_sufficiently_large_for C and
A8: for j st j is_sufficiently_large_for C holds j >= it2;
A9: it2 <= it1 by A5,A8;
it1 <= it2 by A6,A7;
hence thesis by A9,XXREAL_0:1;
end;
end;
theorem Th1:
ApproxIndex C >= 1
proof
ApproxIndex C is_sufficiently_large_for C by Def1;
hence thesis by JORDAN1H:51;
end;
definition
let C;
func Y-InitStart C -> Element of NAT means
:Def2:
it < width Gauge(C,
ApproxIndex C) & cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it
) c= BDD C & for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,
ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it;
existence
proof
set n = ApproxIndex C;
defpred P[Nat] means $1 < width Gauge(C,n) & cell(Gauge(C,n),
X-SpanStart(C,n)-'1,$1) c= BDD C;
set X = { i where i is Element of NAT: P[i] };
A1: X is Subset of NAT from DOMAIN_1:sch 7;
n is_sufficiently_large_for C by Def1;
then consider j such that
A2: P[j];
A3: j in NAT by ORDINAL1:def 12;
j in X by A2,A3;
then reconsider X as non empty Subset of NAT by A1;
take min X;
min X in X by XXREAL_2:def 7;
then ex i being Element of NAT st i = min X & P[i];
hence P[min X];
let i;
A4: i in NAT by ORDINAL1:def 12;
assume P[i];
then i in X by A4;
hence thesis by XXREAL_2:def 7;
end;
uniqueness
proof
let it1,it2 be Element of NAT;
assume that
A5: it1 < width Gauge(C,ApproxIndex C) and
A6: cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it1)
c= BDD C and
A7: for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,
ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it1
and
A8: it2 < width Gauge(C,ApproxIndex C) and
A9: cell(Gauge(C,ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,it2)
c= BDD C and
A10: for j st j < width Gauge(C,ApproxIndex C) & cell(Gauge(C,
ApproxIndex C),X-SpanStart(C,ApproxIndex C)-'1,j) c= BDD C holds j >= it2;
A11: it2 <= it1 by A5,A6,A10;
it1 <= it2 by A7,A8,A9;
hence thesis by A11,XXREAL_0:1;
end;
end;
theorem Th2:
Y-InitStart C > 1
proof
set m = ApproxIndex C;
A1: X-SpanStart(C,m)-'1 <= len Gauge(C,m) by JORDAN1H:50;
assume
A2: Y-InitStart C <= 1;
per cases by A2,NAT_1:25;
suppose
A3: Y-InitStart C = 0;
A4: cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= UBD C by A1,JORDAN1A:49;
0 <= width Gauge(C,m);
then
A5: cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) is non empty by A1,JORDAN1A:24;
cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= BDD C by A3,Def2;
hence contradiction by A5,A4,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
Y-InitStart C = 1;
then
A6: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= BDD C by Def2;
set i1 = X-SpanStart(C,m);
A7: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,m) by JORDAN1H:49;
then
A8: i1-'1 < len Gauge(C,m) by A7,XXREAL_0:2;
BDD C c= C` by JORDAN2C:25;
then
A9: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= C` by A6;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A10: UBD C is_a_component_of C` by JORDAN2C:def 3;
A11: width Gauge(C,m) <> 0 by MATRIX_0:def 10;
then
A12: 0+1 <= width Gauge(C,m) by NAT_1:14;
then
A13: cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) is non empty by A1,JORDAN1A:24;
1 <= i1-'1 by JORDAN1H:50;
then
cell(Gauge(C,m),i1-'1,0) /\ cell(Gauge(C,m),i1-'1,0+1) = LSeg(Gauge(C
,m)*(i1-'1,0+1),Gauge(C,m)*(i1-'1+1,0+1)) by A11,A8,GOBOARD5:26;
then
A14: cell(Gauge(C,m),i1-'1,0) meets cell(Gauge(C,m),i1-'1,0+1);
cell(Gauge(C,m),X-SpanStart(C,m)-'1,0) c= UBD C by A1,JORDAN1A:49;
then cell(Gauge(C,m),X-SpanStart(C,m)-'1,1) c= UBD C by A12,A8,A14,A10,A9,
GOBOARD9:4,JORDAN1A:25;
hence contradiction by A6,A13,JORDAN2C:24,XBOOLE_1:68;
end;
end;
theorem Th3:
Y-InitStart C + 1 < width Gauge(C,ApproxIndex C)
proof
set m = ApproxIndex C;
A1: X-SpanStart(C,m)-'1 <= len Gauge(C,m) by JORDAN1H:50;
assume Y-InitStart C + 1 >= width Gauge(C,m);
then
A2: Y-InitStart C + 1 > width Gauge(C,m) or Y-InitStart C + 1 = width Gauge(
C,m) by XXREAL_0:1;
A3: Y-InitStart C < width Gauge(C,m) or Y-InitStart C = width Gauge(C,m) by
Def2;
per cases by A2,A3,NAT_1:13;
suppose
Y-InitStart C = width Gauge(C,m);
hence contradiction by Def2;
end;
suppose
Y-InitStart C + 1 = width Gauge(C,m);
then Y-InitStart C = width Gauge(C,m)-'1 by NAT_D:34;
then
A4: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= BDD C by Def2;
BDD C c= C` by JORDAN2C:25;
then
A5: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= C` by A4;
A6: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)) c= UBD C by A1,
JORDAN1A:50;
set i1 = X-SpanStart(C,m);
A7: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,m) by JORDAN1H:49;
then
A8: i1-'1 < len Gauge(C,m) by A7,XXREAL_0:2;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A9: UBD C is_a_component_of C` by JORDAN2C:def 3;
width Gauge(C,m)-'1 <= width Gauge(C,m) by NAT_D:44;
then
A10: cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) is non empty
by A1,JORDAN1A:24;
A11: width Gauge(C,m)-1 < width Gauge(C,m) by XREAL_1:146;
A12: 1 <= i1-'1 by JORDAN1H:50;
A13: width Gauge(C,m) <> 0 by MATRIX_0:def 10;
then width Gauge(C,m)-'1+1 = width Gauge(C,m) by NAT_1:14,XREAL_1:235;
then cell(Gauge(C,m),i1-'1,width Gauge(C,m)) /\ cell(Gauge(C,m),i1-'1,
width Gauge(C,m)-'1) = LSeg(Gauge(C,m)*(i1-'1,width Gauge(C,m)), Gauge(C,m)*(i1
-'1+1,width Gauge(C,m))) by A8,A11,A12,GOBOARD5:26;
then
A14: cell(Gauge(C,m),i1-'1,width Gauge(C,m)) meets cell(Gauge(C,m),i1-'1,
width Gauge(C,m)-'1);
width Gauge(C,m)-'1 < width Gauge(C,m) by A13,A11,NAT_1:14,XREAL_1:233;
then cell(Gauge(C,m),X-SpanStart(C,m)-'1,width Gauge(C,m)-'1) c= UBD C by
A6,A8,A14,A9,A5,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A4,A10,JORDAN2C:24,XBOOLE_1:68;
end;
end;
definition
let C,n;
assume n is_sufficiently_large_for C;
then
A1: n >= ApproxIndex C by Def1;
set i1 = X-SpanStart(C,n);
func Y-SpanStart(C,n) -> Element of NAT means
:Def3:
it <= width Gauge(C,n)
& (for k st it <= k & k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds
cell(Gauge(C,n),X-SpanStart(C,n)-'1,k) c= BDD C) & for j st j <= width Gauge(C,
n) & for k st j <= k & k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds
cell(Gauge(C,n),X-SpanStart(C,n)-'1,k) c= BDD C holds j >= it;
existence
proof
set m = ApproxIndex C;
defpred P[Nat] means $1 <= width Gauge(C,n) & for k st $1 <= k
& k <= 2|^(n-'m)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),i1-'1,k) c= BDD C;
set X = { i where i is Element of NAT: P[i]};
set j0 = 2|^(n-'m)*(Y-InitStart C-'2)+2;
A2: X is Subset of NAT from DOMAIN_1:sch 7;
A3: Y-InitStart C+1 < width Gauge(C,m) by Th3;
then Y-InitStart C + 1 < 2|^m + (2+1) by JORDAN1A:28;
then Y-InitStart C + 1 < 2|^m + 2 + 1;
then
A4: Y-InitStart C < 2|^m + 2 by XREAL_1:6;
A5: 1 < Y-InitStart C by Th2;
then 1+1 <= Y-InitStart C by NAT_1:13;
then Y-InitStart C-'2 < 2|^m by A4,NAT_D:54;
then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^(n-'m)*(2|^m) by XREAL_1:64;
then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^((n-'m)+m) by NEWTON:8;
then
A6: 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^n by A1,XREAL_1:235;
A7: now
2|^(m-'1) <= 2|^m by NAT_D:35,PREPOWER:93;
then
A8: 2|^(m-'1) + 2 <= 2|^m + 2 by XREAL_1:6;
len Gauge(C,m) = 2|^m + (2 + 1) by JORDAN8:def 1
.= 2|^m + 2 + 1;
then
A9: X-SpanStart(C,m) < len Gauge(C,m) by A8,NAT_1:13;
A10: Y-InitStart C >= 1+1 by A5,NAT_1:13;
let j;
assume that
A11: j0 <= j and
A12: j <= 2|^(n-'m)*(Y-InitStart C-'2)+2;
A13: m >= 1 by Th1;
1 <= 2|^(m-'1) by PREPOWER:11;
then
A14: 2+1 <= X-SpanStart(C,m) by XREAL_1:6;
A15: cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) c= BDD C by Def2;
j = j0 by A11,A12,XXREAL_0:1;
then
A16: j = 2|^(n-'m)*(Y-InitStart C-2)+2 by A10,XREAL_1:233;
(n-'m)+(m-'1) = (n-'m)+(m-1) by Th1,XREAL_1:233
.= (n-'m)+ m-1
.= n-1 by A1,XREAL_1:235
.= n-'1 by A1,A13,XREAL_1:233,XXREAL_0:2;
then i1 = 2|^(n-'m)*(X-SpanStart(C,m)-2)+2 by NEWTON:8;
then cell(Gauge(C,n),i1-'1,j) c= cell(Gauge(C,m),X-SpanStart(C,m)-'1,
Y-InitStart C) by A1,A3,A14,A9,A16,Th2,JORDAN1A:48;
hence cell(Gauge(C,n),i1-'1,j) c= BDD C by A15;
end;
2|^n <= 2|^n + 1 by NAT_1:11;
then 2|^(n-'m)*(Y-InitStart C-'2) <= 2|^n + 1 by A6,XXREAL_0:2;
then j0 <= 2|^n + 1+2 by XREAL_1:6;
then j0 <= 2|^n + (1+2);
then j0 <= len Gauge(C,n) by JORDAN8:def 1;
then j0 <= width Gauge(C,n) by JORDAN8:def 1;
then j0 in X by A7;
then reconsider X as non empty Subset of NAT by A2;
take min X;
min X in X by XXREAL_2:def 7;
then ex j being Element of NAT st j = min X & P[j];
hence P[min X];
let j;
A17: j in NAT by ORDINAL1:def 12;
assume P[j];
then j in X by A17;
hence thesis by XXREAL_2:def 7;
end;
uniqueness
proof
let it1,it2 be Element of NAT;
defpred definiens[Element of NAT] means $1 <= width Gauge(C,n) & (for i st
$1 <= i & i <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n)
,X-SpanStart(C,n)-'1,i) c= BDD C) & for j st j <= width Gauge(C,n) & for i st j
<= i & i <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),
X-SpanStart(C,n)-'1,i) c= BDD C holds j >= $1;
assume that
A18: definiens[it1] and
A19: definiens[it2];
A20: it2 <= it1 by A18,A19;
it1 <= it2 by A18,A19;
hence thesis by A20,XXREAL_0:1;
end;
end;
theorem Th4:
n is_sufficiently_large_for C implies X-SpanStart(C,n) = 2|^(n-'
ApproxIndex C)*(X-SpanStart(C,ApproxIndex C)-2)+2
proof
set m = ApproxIndex C;
A1: m >= 1 by Th1;
assume n is_sufficiently_large_for C;
then
A2: n >=ApproxIndex C by Def1;
(n-'m)+(m-'1) = (n-'m)+(m-1) by Th1,XREAL_1:233
.= (n-'m)+ m-1
.= n-1 by A2,XREAL_1:235
.= n-'1 by A2,A1,XREAL_1:233,XXREAL_0:2;
hence thesis by NEWTON:8;
end;
theorem Th5:
n is_sufficiently_large_for C implies Y-SpanStart(C,n) <= 2|^(n-'
ApproxIndex C)*(Y-InitStart C-'2)+2
proof
set m = ApproxIndex C;
A1: X-SpanStart(C,m) > 2 by JORDAN1H:49;
set j0 = 2|^(n-'m)*(Y-InitStart C-'2)+2;
set i1 = X-SpanStart(C,n);
assume
A2: n is_sufficiently_large_for C;
then
A3: n >=ApproxIndex C by Def1;
A4: 1 < Y-InitStart C by Th2;
then 1+1 <= Y-InitStart C by NAT_1:13;
then
A5: Y-InitStart C-'2 = Y-InitStart C-2 by XREAL_1:233;
A6: Y-InitStart C+1 < width Gauge(C,m) by Th3;
A7: now
m-'1 <= m by NAT_D:44;
then
A8: 2|^(m-'1) <= 2|^m by PREPOWER:93;
len Gauge(C,m) = 2|^m + 3 by JORDAN8:def 1;
then
A9: X-SpanStart(C,m) < len Gauge(C,m) by A8,XREAL_1:8;
A10: 2+1 <= X-SpanStart(C,m) by A1,NAT_1:13;
A11: i1 = 2|^(n-'m)*(X-SpanStart(C,m)-2)+2 by A2,Th4;
let j;
assume that
A12: j0 <= j and
A13: j <= 2|^(n-'m)*(Y-InitStart C-'2)+2;
A14: cell(Gauge(C,m),X-SpanStart(C,m)-'1,Y-InitStart C) c= BDD C by Def2;
j = j0 by A12,A13,XXREAL_0:1;
then cell(Gauge(C,n),i1-'1,j) c= cell(Gauge(C,m),X-SpanStart(C,m)-'1,
Y-InitStart C) by A3,A6,A5,A10,A9,A11,Th2,JORDAN1A:48;
hence cell(Gauge(C,n),i1-'1,j) c= BDD C by A14;
end;
Y-InitStart C < Y-InitStart C +1 by XREAL_1:29;
then Y-InitStart C < width Gauge(C,m) by Th3,XXREAL_0:2;
then j0 <= width Gauge(C,n) by A3,A4,A5,JORDAN1A:32;
hence thesis by A2,A7,Def3;
end;
theorem Th6:
n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart
(C,n)-'1,Y-SpanStart(C,n)) c= BDD C
proof
assume
A1: n is_sufficiently_large_for C;
then Y-SpanStart(C,n) <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 by Th5;
hence thesis by A1,Def3;
end;
theorem Th7:
n is_sufficiently_large_for C implies 1 < Y-SpanStart(C,n) &
Y-SpanStart(C,n) <= width Gauge(C,n)
proof
assume
A1: n is_sufficiently_large_for C;
thus 1 < Y-SpanStart(C,n)
proof
A2: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:50;
assume
A3: Y-SpanStart(C,n) <= 1;
per cases by A3,NAT_1:25;
suppose
A4: Y-SpanStart(C,n) = 0;
A5: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A2,JORDAN1A:49;
0 <= width Gauge(C,n);
then
A6: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A2,JORDAN1A:24;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= BDD C by A1,A4,Th6;
hence contradiction by A6,A5,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
Y-SpanStart(C,n) = 1;
then
A7: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= BDD C by A1,Th6;
set i1 = X-SpanStart(C,n);
A8: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,n) by JORDAN1H:49;
then
A9: i1-'1 < len Gauge(C,n) by A8,XXREAL_0:2;
BDD C c= C` by JORDAN2C:25;
then
A10: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A7;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A11: UBD C is_a_component_of C` by JORDAN2C:def 3;
A12: width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A13: 0+1 <= width Gauge(C,n) by NAT_1:14;
then
A14: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A2,JORDAN1A:24;
1 <= i1-'1 by JORDAN1H:50;
then
cell(Gauge(C,n),i1-'1,0) /\ cell(Gauge(C,n),i1-'1,0+1) = LSeg(Gauge
(C,n)*(i1-'1,0+1),Gauge(C,n)*(i1-'1+1,0+1)) by A12,A9,GOBOARD5:26;
then
A15: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0+1);
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A2,JORDAN1A:49;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A13,A9,A15,A11
,A10,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A7,A14,JORDAN2C:24,XBOOLE_1:68;
end;
end;
thus thesis by A1,Def3;
end;
theorem
n is_sufficiently_large_for C implies [X-SpanStart(C,n),Y-SpanStart(C,
n)] in Indices Gauge(C,n)
proof
A1: X-SpanStart(C,n) < len Gauge(C,n) by JORDAN1H:49;
1+1 < X-SpanStart(C,n) by JORDAN1H:49;
then
A2: 1 < X-SpanStart(C,n) by NAT_1:13;
assume
A3: n is_sufficiently_large_for C;
then
A4: Y-SpanStart(C,n) <= width Gauge(C,n) by Th7;
1 < Y-SpanStart(C,n) by A3,Th7;
hence thesis by A2,A1,A4,MATRIX_0:30;
end;
theorem
n is_sufficiently_large_for C implies [X-SpanStart(C,n)-'1,Y-SpanStart
(C,n)] in Indices Gauge(C,n)
proof
A1: 1 <= X-SpanStart(C,n)-'1 by JORDAN1H:50;
A2: X-SpanStart(C,n)-'1 < len Gauge(C,n) by JORDAN1H:50;
assume
A3: n is_sufficiently_large_for C;
then
A4: Y-SpanStart(C,n) <= width Gauge(C,n) by Th7;
1 < Y-SpanStart(C,n) by A3,Th7;
hence thesis by A1,A2,A4,MATRIX_0:30;
end;
theorem
n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart(C,n)
-'1,Y-SpanStart(C,n)-'1) meets C
proof
set i1 = X-SpanStart(C,n);
A1: Y-SpanStart(C,n)-1 < Y-SpanStart(C,n) by XREAL_1:146;
assume
A2: n is_sufficiently_large_for C;
then
A3: 1 < Y-SpanStart(C,n) by Th7;
assume
A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)-'1) misses C;
A5: for k st Y-SpanStart(C,n)-'1 <= k & k <= 2|^(n-'ApproxIndex C)*(
Y-InitStart C-'2)+2 holds cell(Gauge(C,n),i1-'1,k) c= BDD C
proof
let k such that
A6: Y-SpanStart(C,n)-'1 <= k and
A7: k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2;
per cases by A6,XXREAL_0:1;
suppose
A8: Y-SpanStart(C,n)-'1 = k;
1 < Y-SpanStart(C,n) by A2,Th7;
then
A9: k+1 = Y-SpanStart(C,n) by A8,XREAL_1:235;
A10: cell(Gauge(C,n),i1-'1,k) c= C` by A4,A8,SUBSET_1:23;
A11: k < k+1 by XREAL_1:29;
Y-SpanStart(C,n) <= width Gauge(C,n) by A2,Th7;
then
A12: k < width Gauge(C,n) by A9,A11,XXREAL_0:2;
set W = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C};
A13: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,n) by JORDAN1H:49;
then
A14: i1-'1 < len Gauge(C,n) by A13,XXREAL_0:2;
A15: BDD C = union W by JORDAN2C:def 4;
1+1 < X-SpanStart(C,n) by JORDAN1H:49;
then 1 <= i1-1 by XREAL_1:19;
then 1 <= i1-'1 by NAT_D:39;
then
cell(Gauge(C,n),i1-'1,k) /\ cell(Gauge(C,n),i1-'1,k+1) = LSeg(Gauge
(C,n)*(i1-'1,k+1),Gauge(C,n)*(i1-'1+1,k+1)) by A14,A12,GOBOARD5:26;
then cell(Gauge(C,n),i1-'1,k) meets cell(Gauge(C,n),i1-'1,k+1);
then cell(Gauge(C,n),i1-'1,k) meets BDD C by A2,A9,Th6,XBOOLE_1:63;
then consider e being set such that
A16: e in W and
A17: cell(Gauge(C,n),i1-'1,k) meets e by A15,ZFMISC_1:80;
consider B being Subset of TOP-REAL 2 such that
A18: e = B and
A19: B is_inside_component_of C by A16;
A20: B c= BDD C by A15,A16,A18,ZFMISC_1:74;
B is_a_component_of C` by A19,JORDAN2C:def 2;
then cell(Gauge(C,n),i1-'1,k) c= B by A10,A14,A12,A17,A18,GOBOARD9:4
,JORDAN1A:25;
hence thesis by A20;
end;
suppose
Y-SpanStart(C,n)-'1 < k;
then Y-SpanStart(C,n) < k+1 by NAT_D:55;
then Y-SpanStart(C,n) <= k by NAT_1:13;
hence thesis by A2,A7,Def3;
end;
end;
Y-SpanStart(C,n) <= width Gauge(C,n) by A2,Def3;
then Y-SpanStart(C,n)-'1 <= width Gauge(C,n) by NAT_D:44;
then Y-SpanStart(C,n)-'1 >=Y-SpanStart(C,n) by A2,A5,Def3;
hence contradiction by A3,A1,XREAL_1:233;
end;
theorem
n is_sufficiently_large_for C implies cell(Gauge(C,n),X-SpanStart(C,n)
-'1,Y-SpanStart(C,n)) misses C
proof
assume n is_sufficiently_large_for C;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) c= BDD C by Th6;
hence thesis by JORDAN1A:7,XBOOLE_1:63;
end;
:: Moved from JORDAN1K, AK 20.02.2006
begin :: BDD & UBD
reserve p,q for Point of TOP-REAL 2,
D for Simple_closed_curve;
theorem Th12:
UBD C meets UBD D
proof
reconsider A = C as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r1 being Real, x1 being Point of Euclid 2 such that
0 < r1 and
A1: A c= Ball(x1,r1) by METRIC_6:def 3;
reconsider B = D as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r2 being Real, x2 being Point of Euclid 2 such that
0 < r2 and
A2: B c= Ball(x2,r2) by METRIC_6:def 3;
reconsider C9 = Ball(x1,r1)`, D9 = Ball(x2,r2)` as connected Subset of
TOP-REAL 2 by JORDAN1K:37;
consider x3 being Point of Euclid 2, r3 being Real such that
A3: Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x3,r3) by WEIERSTR:1;
A4: now
assume D9 is bounded;
then D9 is bounded Subset of Euclid 2 by JORDAN2C:11;
hence contradiction by JORDAN1K:8;
end;
A5: now
assume C9 is bounded;
then C9 is bounded Subset of Euclid 2 by JORDAN2C:11;
hence contradiction by JORDAN1K:8;
end;
Ball(x3,r3)` c= (Ball(x1,r1) \/ Ball(x2,r2))` by A3,SUBSET_1:12;
then
A6: Ball(x3,r3)` c= Ball(x1,r1)` /\ Ball(x2,r2)` by XBOOLE_1:53;
then
A7: Ball(x3,r3)` c= Ball(x1,r1)` by XBOOLE_1:18;
A8: Ball(x3,r3)` c= Ball(x2,r2)` by A6,XBOOLE_1:18;
Ball(x2,r2)` c= B` by A2,SUBSET_1:12;
then Ball(x2,r2)` misses B by SUBSET_1:23;
then D9 c= UBD D by A4,JORDAN2C:125;
then
A9: Ball(x3,r3)` c= UBD D by A8;
Ball(x1,r1)` c= A` by A1,SUBSET_1:12;
then Ball(x1,r1)` misses A by SUBSET_1:23;
then C9 c= UBD C by A5,JORDAN2C:125;
then
A10: Ball(x3,r3)` c= UBD C by A7;
Ball(x3,r3)` <> {}Euclid 2 by JORDAN1K:8;
hence thesis by A10,A9,XBOOLE_1:68;
end;
theorem Th13:
q in UBD C & p in BDD C implies dist(q,C) < dist(q,p)
proof
assume that
A1: q in UBD C and
A2: p in BDD C and
A3: dist(q,C) >= dist(q,p);
A4: UBD C is_a_component_of C` by JORDAN2C:124;
now
assume LSeg(p,q) meets C;
then consider x being object such that
A5: x in LSeg(p,q) and
A6: x in C by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A5;
A7: dist(q,C) <= dist(q,x) by A6,JORDAN1K:50;
C misses BDD C by JORDAN1A:7;
then x <> p by A2,A6,XBOOLE_0:3;
hence contradiction by A3,A5,A7,JORDAN1K:30,XXREAL_0:2;
end;
then
A8: LSeg(p,q) c= C` by SUBSET_1:23;
q in LSeg(p,q) by RLTOPSP1:68;
then
A9: LSeg(p,q) meets UBD C by A1,XBOOLE_0:3;
A10: BDD C = union{B where B is Subset of TOP-REAL 2: B
is_inside_component_of C} by JORDAN2C:def 4;
then consider X being set such that
A11: p in X and
A12: X in {B where B is Subset of TOP-REAL 2: B is_inside_component_of C
} by A2,TARSKI:def 4;
consider B being Subset of TOP-REAL 2 such that
A13: X = B and
A14: B is_inside_component_of C by A12;
B c= BDD C by A10,A12,A13,ZFMISC_1:74;
then
A15: B misses UBD C by JORDAN2C:24,XBOOLE_1:63;
p in LSeg(p,q) by RLTOPSP1:68;
then
A16: LSeg(p,q) meets B by A11,A13,XBOOLE_0:3;
B is_a_component_of C` by A14,JORDAN2C:def 2;
then UBD C = B by A8,A4,A9,A16,JORDAN9:1;
hence contradiction by A15;
end;
theorem Th14:
not p in BDD C implies dist(p,C) <= dist(p,BDD C)
proof
per cases;
suppose
p in C;
then dist(p,C) = 0 by JORDAN1K:45;
hence thesis by JORDAN1K:44;
end;
suppose
A1: not p in C;
assume that
A2: not p in BDD C and
A3: dist(p,C) > dist(p,BDD C);
A4: ex q st q in BDD C & dist(p,q) < dist(p,C) by A3,JORDAN1K:48;
p in C` by A1,SUBSET_1:29;
then p in (BDD C) \/ (UBD C) by JORDAN2C:27;
then p in UBD C by A2,XBOOLE_0:def 3;
hence contradiction by A4,Th13;
end;
end;
theorem Th15:
not(C c= BDD D & D c= BDD C)
proof
assume that
A1: C c= BDD D and
A2: D c= BDD C;
UBD C meets UBD D by Th12;
then consider e being object such that
A3: e in UBD C and
A4: e in UBD D by XBOOLE_0:3;
reconsider p = e as Point of TOP-REAL 2 by A3;
UBD D misses BDD D by JORDAN2C:24;
then
A5: not p in BDD D by A4,XBOOLE_0:3;
UBD C misses BDD C by JORDAN2C:24;
then
A6: not p in BDD C by A3,XBOOLE_0:3;
then dist(p,C) <= dist(p, BDD C) by Th14;
then dist(p, BDD D) < dist(p, BDD C) by A1,A5,JORDAN1K:51,XXREAL_0:2;
then dist(p, BDD D) < dist(p,D) by A2,A6,JORDAN1K:51,XXREAL_0:2;
hence contradiction by A5,Th14;
end;
theorem Th16:
C c= BDD D implies D c= UBD C
proof
assume
A1: C c= BDD D;
assume
A2: not D c= UBD C;
C misses D by A1,JORDAN1A:7,XBOOLE_1:63;
then D c= BDD C by A2,JORDAN1K:19;
hence contradiction by A1,Th15;
end;
theorem
L~Cage(C,n) c= UBD C
proof
C c= BDD L~Cage(C,n) by JORDAN10:12;
hence thesis by Th16;
end;