:: Bounding Boxes for Special Sequences in ${\calE}^2$
:: by Yatsuka Nakamura and Adam Grabowski
::
:: Received June 8, 1998
:: Copyright (c) 1998-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, PRE_TOPC, EUCLID, REAL_1, FUNCT_1, GOBOARD5, FINSEQ_1,
XBOOLE_0, SUBSET_1, XXREAL_0, PARTFUN1, RLTOPSP1, ARYTM_1, ARYTM_3,
INT_1, RELAT_1, JORDAN4, GOBOARD2, TREES_1, MCART_1, GOBOARD1, MATRIX_1,
NAT_1, ZFMISC_1, PSCOMP_1, TOPREAL1, STRUCT_0, TARSKI, SEQ_4, FINSET_1,
SPPOL_1, XXREAL_2, CARD_1, JORDAN5D;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MCART_1,
XCMPLX_0, REAL_1, NAT_1, NAT_D, RELAT_1, FINSEQ_1, FUNCT_1, PARTFUN1,
FINSET_1, MATRIX_0, XXREAL_2, STRUCT_0, TOPREAL1, SPPOL_1, GOBOARD1,
GOBOARD2, GOBOARD5, PRE_TOPC, RLTOPSP1, EUCLID, JORDAN4, PSCOMP_1,
XXREAL_0, SEQ_4;
constructors REAL_1, NAT_D, BINARITH, COMPTS_1, GOBOARD2, SPPOL_1, PSCOMP_1,
JORDAN4, GOBOARD1, SEQ_4, RELSET_1, RVSUM_1;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1,
STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, SPRECT_1, VALUED_0, XXREAL_2,
FUNCT_1, SEQ_4;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_2;
equalities XBOOLE_0, PSCOMP_1, STRUCT_0;
expansions XXREAL_2;
theorems EUCLID, FINSEQ_3, FINSEQ_6, FUNCT_1, FUNCT_2, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD7, NAT_1, PRE_TOPC, SEQ_4, SPPOL_1, SPPOL_2, TOPREAL1,
MATRIX_0, FINSEQ_1, ZFMISC_1, JORDAN4, PSCOMP_1, SPRECT_2, FINSEQ_2,
XBOOLE_0, XBOOLE_1, ORDINAL1, XREAL_1, XXREAL_0, PARTFUN1, XXREAL_2,
NAT_D, XREAL_0, TARSKI;
schemes DOMAIN_1;
begin :: Preliminaries
reserve p, q for Point of TOP-REAL 2,
r for Real,
h for non constant standard special_circular_sequence,
g for FinSequence of TOP-REAL 2,
f for non empty FinSequence of TOP-REAL 2,
I, i1, i, j, k for Nat;
theorem Th1:
for n be Nat, h be FinSequence of TOP-REAL n st len h
>= 2 holds h/.len h in LSeg(h,len h-'1)
proof
let n be Nat;
let h be FinSequence of TOP-REAL n;
set i = len h;
assume
A1: len h >= 2;
then
A2: 2-1 <= i-1 by XREAL_1:9;
i-'1+1 = len h by A1,XREAL_1:235,XXREAL_0:2;
hence thesis by A2,TOPREAL1:21;
end;
theorem Th2:
3 <= i implies i mod (i-'1) = 1
proof
assume
A1: 3 <= i;
then
A2: i-'1 = i-1 by XREAL_1:233,XXREAL_0:2;
3-'1 = 2+1-'1 .= 2 by NAT_D:34;
then 2 <= i-'1 by A1,NAT_D:42;
then 1 < i-1 by A2,XXREAL_0:2;
then 1+i < (i-1)+i by XREAL_1:8;
then 1+i-1 < (i-1)+i-1 by XREAL_1:14;
then
A3: i < (i-1) + (i-1);
i-'1 <= i by NAT_D:35;
hence i mod (i-'1) = i - (i-1) by A2,A3,JORDAN4:2
.= 1;
end;
theorem Th3:
p in rng h implies ex i be Nat st 1 <= i & i+1 <= len h & h.i = p
proof
A1: 4 < len h by GOBOARD7:34;
A2: 1 < len h by GOBOARD7:34,XXREAL_0:2;
assume p in rng h;
then consider x be object such that
A3: x in dom h and
A4: p = h.x by FUNCT_1:def 3;
reconsider i = x as Nat by A3;
A5: 1 <= i by A3,FINSEQ_3:25;
set j = S_Drop (i,h);
A6: i <= len h by A3,FINSEQ_3:25;
1 <= j & j+1 <= len h & h.j = p
proof
A7: i <= len h -' 1 + 1 by A5,A6,XREAL_1:235,XXREAL_0:2;
per cases by A7,NAT_1:8;
suppose
A8: i <= len h-'1;
then j = i by A5,JORDAN4:22;
then j + 1 <= len h -' 1 + 1 by A8,XREAL_1:7;
hence thesis by A4,A5,A2,A8,JORDAN4:22,XREAL_1:235;
end;
suppose
A9: i = len h-'1+1;
then i = len h by A1,XREAL_1:235,XXREAL_0:2;
then i mod (len h -'1) = 1 by A1,Th2,XXREAL_0:2;
then
A10: j = 1 by JORDAN4:def 1;
A11: 1 <= len h by GOBOARD7:34,XXREAL_0:2;
then
A12: len h in dom h by FINSEQ_3:25;
1 in dom h by A11,FINSEQ_3:25;
then h.1 = h/.1 by PARTFUN1:def 6
.= h/.len h by FINSEQ_6:def 1
.= h.len h by A12,PARTFUN1:def 6;
hence thesis by A4,A1,A9,A10,XREAL_1:235,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th4:
for g being FinSequence of REAL st r in rng g holds Incr g.1 <= r
& r <= Incr g.len Incr g
proof
let g be FinSequence of REAL;
assume r in rng g;
then r in rng Incr g by SEQ_4:def 21;
then consider x being object such that
A1: x in dom Incr g and
A2: Incr g.x=r by FUNCT_1:def 3;
reconsider j=x as Nat by A1;
A3: x in Seg len Incr g by A1,FINSEQ_1:def 3;
then
A4: j <= len Incr g by FINSEQ_1:1;
A5: 1 <= j by A3,FINSEQ_1:1;
then
A6: 1 <= len Incr g by A4,XXREAL_0:2;
then 1 in dom Incr g by FINSEQ_3:25;
hence Incr g.1 <= r by A1,A2,A5,SEQ_4:137;
len Incr g in dom Incr g by A6,FINSEQ_3:25;
hence thesis by A1,A2,A4,SEQ_4:137;
end;
theorem Th5:
1 <= i & i <= len h & 1 <= I & I <= width GoB h implies (GoB h)*(
1,I)`1 <= (h/.i)`1 & (h/.i)`1 <= (GoB h)*(len GoB h,I)`1
proof
assume that
A1: 1<=i and
A2: i<=len h and
A3: 1 <= I and
A4: I <= width GoB h;
A5: I<=width GoB(Incr(X_axis(h)),Incr(Y_axis(h))) by A4,GOBOARD2:def 2;
i<=len (X_axis h) by A2,GOBOARD1:def 1;
then
A6: i in dom (X_axis h) by A1,FINSEQ_3:25;
then (X_axis(h)).i=(h/.i)`1 by GOBOARD1:def 1;
then
A7: (h/.i)`1 in rng X_axis h by A6,FUNCT_1:def 3;
A8: GoB h=GoB(Incr(X_axis h),Incr(Y_axis(h))) by GOBOARD2:def 2;
then 1<=len GoB(Incr(X_axis h),Incr(Y_axis h)) by GOBOARD7:32;
then
A9: [1,I] in Indices GoB(Incr(X_axis h),Incr(Y_axis h)) by A3,A5,MATRIX_0:30;
A10: 1<=len GoB h by GOBOARD7:32;
len GoB h <= len GoB(Incr(X_axis h),Incr(Y_axis h)) by GOBOARD2:def 2;
then
A11: [len GoB h,I] in Indices GoB(Incr(X_axis h),Incr(Y_axis h)) by A3,A5,A10,
MATRIX_0:30;
(GoB h)*(len GoB h,I)=(GoB(Incr(X_axis h),Incr(Y_axis h)))* (len GoB h,
I) by GOBOARD2:def 2
.=|[Incr(X_axis h).len GoB h,Incr(Y_axis(h)).I]| by A11,GOBOARD2:def 1;
then
A12: (GoB h)*(len GoB h,I)`1 = Incr(X_axis h).len GoB h by EUCLID:52;
(GoB h)*(1,I)=(GoB(Incr(X_axis(h)),Incr(Y_axis(h))))*(1,I) by GOBOARD2:def 2
.=|[Incr(X_axis(h)).1,Incr(Y_axis(h)).I]| by A9,GOBOARD2:def 1;
then
A13: (GoB h)*(1,I)`1=Incr(X_axis(h)).1 by EUCLID:52;
len GoB h = len Incr (X_axis h) by A8,GOBOARD2:def 1;
hence thesis by A12,A13,A7,Th4;
end;
theorem Th6:
1 <= i & i <= len h & 1 <= I & I <= len GoB h implies (GoB h)*(I,
1)`2 <= (h/.i)`2 & (h/.i)`2 <= (GoB h)*(I,width GoB h)`2
proof
assume that
A1: 1<=i and
A2: i<=len h and
A3: 1 <= I and
A4: I <= len GoB h;
A5: GoB h=GoB(Incr(X_axis h),Incr(Y_axis h)) by GOBOARD2:def 2;
then
A6: 1<=width GoB(Incr(X_axis h),Incr(Y_axis h)) by GOBOARD7:33;
i <= len Y_axis h by A2,GOBOARD1:def 2;
then
A7: i in dom Y_axis h by A1,FINSEQ_3:25;
then (Y_axis h).i = (h/.i)`2 by GOBOARD1:def 2;
then
A8: (h/.i)`2 in rng Y_axis h by A7,FUNCT_1:def 3;
1<=width GoB h by GOBOARD7:33;
then
A9: [I,width GoB h] in Indices GoB(Incr(X_axis h),Incr(Y_axis h)) by A3,A4,A5,
MATRIX_0:30;
(GoB h)*(I,width GoB h)=(GoB(Incr(X_axis h),Incr(Y_axis h)))* (I,width
GoB h) by GOBOARD2:def 2
.=|[Incr(X_axis(h)).I,Incr(Y_axis(h)).width GoB h]| by A9,GOBOARD2:def 1;
then
A10: (GoB h)*(I,width GoB h)`2 = Incr(Y_axis h).width GoB h by EUCLID:52;
I<=len GoB(Incr(X_axis h),Incr(Y_axis h)) by A4,GOBOARD2:def 2;
then
A11: [I,1] in Indices GoB(Incr(X_axis h),Incr(Y_axis h)) by A3,A6,MATRIX_0:30;
(GoB h)*(I,1)=(GoB(Incr(X_axis h),Incr(Y_axis h)))*(I,1) by GOBOARD2:def 2
.= |[Incr(X_axis(h)).I,Incr(Y_axis(h)).1]| by A11,GOBOARD2:def 1;
then
A12: (GoB h)*(I,1)`2 = Incr(Y_axis h).1 by EUCLID:52;
width GoB h = len Incr Y_axis h by A5,GOBOARD2:def 1;
hence thesis by A10,A12,A8,Th4;
end;
theorem Th7:
1 <= i & i <= len GoB f implies ex k,j st k in dom f & [i,j] in
Indices GoB f & f/.k = (GoB f)*(i,j)
proof
assume that
A1: 1 <= i and
A2: i <= len GoB f;
A3: i in dom GoB f by A1,A2,FINSEQ_3:25;
A4: GoB f = GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr X_axis f = len GoB f by GOBOARD2:def 1;
then i in dom Incr X_axis f by A1,A2,FINSEQ_3:25;
then (Incr X_axis f).i in rng Incr X_axis f by FUNCT_1:def 3;
then (Incr X_axis f).i in rng X_axis f by SEQ_4:def 21;
then consider k being Nat such that
A5: k in dom X_axis f and
A6: (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:10;
A7: len X_axis f = len f by GOBOARD1:def 1
.= len Y_axis f by GOBOARD1:def 2;
then dom X_axis f = dom Y_axis f by FINSEQ_3:29;
then (Y_axis f).k in rng Y_axis f by A5,FUNCT_1:def 3;
then (Y_axis f).k in rng Incr Y_axis f by SEQ_4:def 21;
then consider j being Nat such that
A8: j in dom Incr Y_axis f and
A9: (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:10;
reconsider k,j as Nat;
A10: (X_axis f).k = (f/.k)`1 by A5,GOBOARD1:def 1;
take k,j;
len X_axis f = len f by GOBOARD1:def 1;
hence k in dom f by A5,FINSEQ_3:29;
j in Seg len Incr Y_axis f by A8,FINSEQ_1:def 3;
then j in Seg width GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 1;
then [i,j] in [:dom GoB f, Seg width GoB f:] by A4,A3,ZFMISC_1:87;
hence
A11: [i,j] in Indices GoB f by MATRIX_0:def 4;
dom X_axis f = dom Y_axis f by A7,FINSEQ_3:29;
then (Y_axis f).k = (f/.k)`2 by A5,GOBOARD1:def 2;
hence f/.k = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A6,A9,A10,EUCLID:53
.= (GoB f)*(i,j) by A4,A11,GOBOARD2:def 1;
end;
theorem Th8:
1 <= j & j <= width GoB f implies ex k,i st k in dom f & [i,j]
in Indices GoB f & f/.k = (GoB f)*(i,j)
proof
assume that
A1: 1 <= j and
A2: j <= width GoB f;
A3: j in Seg width GoB f by A1,A2,FINSEQ_1:1;
A4: GoB f = GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
then j in dom Incr Y_axis f by A1,A2,FINSEQ_3:25;
then (Incr Y_axis f).j in rng Incr Y_axis f by FUNCT_1:def 3;
then (Incr Y_axis f).j in rng Y_axis f by SEQ_4:def 21;
then consider k being Nat such that
A5: k in dom Y_axis f and
A6: (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:10;
A7: len X_axis f = len f by GOBOARD1:def 1
.= len Y_axis f by GOBOARD1:def 2;
then k in dom X_axis f by A5,FINSEQ_3:29;
then (X_axis f).k in rng X_axis f by FUNCT_1:def 3;
then (X_axis f).k in rng Incr X_axis f by SEQ_4:def 21;
then consider i being Nat such that
A8: i in dom Incr X_axis f and
A9: (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:10;
reconsider k,i as Nat;
k in dom X_axis f by A5,A7,FINSEQ_3:29;
then
A10: (X_axis f).k = (f/.k)`1 by GOBOARD1:def 1;
take k,i;
len Y_axis f = len f by GOBOARD1:def 2;
hence k in dom f by A5,FINSEQ_3:29;
len GoB(Incr X_axis f,Incr Y_axis f) = len Incr X_axis f by GOBOARD2:def 1;
then i in dom GoB(Incr X_axis f,Incr Y_axis f) by A8,FINSEQ_3:29;
then [i,j] in [:dom GoB f, Seg width GoB f:] by A4,A3,ZFMISC_1:87;
hence
A11: [i,j] in Indices GoB f by MATRIX_0:def 4;
(Y_axis f).k = (f/.k)`2 by A5,GOBOARD1:def 2;
hence f/.k = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A6,A9,A10,EUCLID:53
.= (GoB f)*(i,j) by A4,A11,GOBOARD2:def 1;
end;
theorem Th9:
1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f implies ex k
st k in dom f & [i,j] in Indices GoB f & (f/.k)`1 = (GoB f)*(i,j)`1
proof
assume that
A1: 1 <= i and
A2: i <= len GoB f and
A3: 1 <= j and
A4: j <= width GoB f;
A5: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
then j in dom Incr Y_axis f by A3,A4,FINSEQ_3:25;
then j in Seg len Incr Y_axis f by FINSEQ_1:def 3;
then
A6: j in Seg width GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 1;
len Incr X_axis f = len GoB f by A5,GOBOARD2:def 1;
then i in dom Incr X_axis f by A1,A2,FINSEQ_3:25;
then (Incr X_axis f).i in rng Incr X_axis f by FUNCT_1:def 3;
then (Incr X_axis f).i in rng X_axis f by SEQ_4:def 21;
then consider k being Nat such that
A7: k in dom X_axis f and
A8: (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:10;
reconsider k as Nat;
take k;
len X_axis f = len f by GOBOARD1:def 1;
hence k in dom f by A7,FINSEQ_3:29;
i in dom GoB f by A1,A2,FINSEQ_3:25;
then [i,j] in [:dom GoB f, Seg width GoB f:] by A5,A6,ZFMISC_1:87;
hence [i,j] in Indices GoB f by MATRIX_0:def 4;
then
A9: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A5,GOBOARD2:def 1;
thus (f/.k)`1 = Incr(X_axis f).i by A7,A8,GOBOARD1:def 1
.= (GoB f)*(i,j)`1 by A9,EUCLID:52;
end;
theorem Th10:
1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f implies ex k
st k in dom f & [i,j] in Indices GoB f & (f/.k)`2 = (GoB f)*(i,j)`2
proof
assume that
A1: 1 <= i and
A2: i <= len GoB f and
A3: 1 <= j and
A4: j <= width GoB f;
A5: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
then j in dom Incr Y_axis f by A3,A4,FINSEQ_3:25;
then j in Seg len Incr Y_axis f by FINSEQ_1:def 3;
then
A6: j in Seg width GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 1;
len Incr Y_axis f = width GoB f by A5,GOBOARD2:def 1;
then j in dom Incr Y_axis f by A3,A4,FINSEQ_3:25;
then (Incr Y_axis f).j in rng Incr Y_axis f by FUNCT_1:def 3;
then (Incr Y_axis f).j in rng Y_axis f by SEQ_4:def 21;
then consider k being Nat such that
A7: k in dom Y_axis f and
A8: (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:10;
reconsider k as Nat;
take k;
len Y_axis f = len f by GOBOARD1:def 2;
hence k in dom f by A7,FINSEQ_3:29;
i in dom GoB f by A1,A2,FINSEQ_3:25;
then [i,j] in [:dom GoB f, Seg width GoB f:] by A5,A6,ZFMISC_1:87;
hence [i,j] in Indices GoB f by MATRIX_0:def 4;
then
A9: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A5,GOBOARD2:def 1;
thus (f/.k)`2 = Incr(Y_axis f).j by A7,A8,GOBOARD1:def 2
.= (GoB f)*(i,j)`2 by A9,EUCLID:52;
end;
begin :: Extrema of projections
theorem Th11:
1 <= i & i <= len h implies S-bound L~h <= (h/.i)`2 & (h/.i)`2 <= N-bound L~h
proof
A1: len h > 4 by GOBOARD7:34;
assume that
A2: 1<=i and
A3: i<=len h;
i in dom h by A2,A3,FINSEQ_3:25;
then h/.i in L~h by A1,GOBOARD1:1,XXREAL_0:2;
hence thesis by PSCOMP_1:24;
end;
theorem Th12:
1 <= i & i <= len h implies W-bound L~h <= (h/.i)`1 & (h/.i)`1 <= E-bound L~h
proof
A1: len h > 4 by GOBOARD7:34;
assume that
A2: 1<=i and
A3: i<=len h;
i in dom h by A2,A3,FINSEQ_3:25;
then h/.i in L~h by A1,GOBOARD1:1,XXREAL_0:2;
hence thesis by PSCOMP_1:24;
end;
theorem Th13:
for X being Subset of REAL st X = { q`2 : q`1 = W-bound L~h & q
in L~h } holds X = (proj2 | W-most L~h).:the carrier of (TOP-REAL 2)|(W-most L~
h)
proof
set T = (TOP-REAL 2)|(W-most L~h);
set F = proj2 | W-most L~h;
let X be Subset of REAL such that
A1: X = { q`2 : q`1 = W-bound L~h & q in L~h };
thus X c= (proj2 | W-most L~h).:the carrier of T
proof
let x be object;
A2: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|(W-most L~h))
.= W-most L~h by PRE_TOPC:def 5;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A3: q1`2 = x and
A4: q1`1 = W-bound L~h and
A5: q1 in L~h by A1;
A6: x = F.q1 by A3,A4,A5,PSCOMP_1:23,SPRECT_2:12;
A7: q1 in W-most L~h by A4,A5,SPRECT_2:12;
then q1 in the carrier of T by A2,FUNCT_2:def 1;
hence thesis by A2,A7,A6,FUNCT_1:def 6;
end;
thus (proj2 | W-most L~h).:the carrier of T c= X
proof
let x be object;
A8: W-most L~h c= L~h by XBOOLE_1:17;
assume x in (proj2 | W-most L~h).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A9: x1 in the carrier of T and
A10: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|(W-most L~h)) by A9;
then
A11: x1 in W-most L~h by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
A12: x2`1 = (W-min L~h)`1 by A11,PSCOMP_1:31
.= W-bound L~h by EUCLID:52;
x = x2`2 by A10,A11,PSCOMP_1:23;
hence thesis by A1,A11,A12,A8;
end;
end;
theorem Th14:
for X being Subset of REAL st X = { q`2 : q`1 = E-bound L~h & q
in L~h } holds X = (proj2 | E-most L~h).:the carrier of (TOP-REAL 2)|(E-most L~
h)
proof
set T = (TOP-REAL 2)|(E-most L~h);
set F = proj2 | E-most L~h;
let X be Subset of REAL such that
A1: X = { q`2 : q`1 = E-bound L~h & q in L~h };
thus X c= (proj2 | E-most L~h).:the carrier of T
proof
let x be object;
A2: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|(E-most L~h))
.= E-most L~h by PRE_TOPC:def 5;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A3: q1`2 = x and
A4: q1`1 = E-bound L~h and
A5: q1 in L~h by A1;
A6: x = F.q1 by A3,A4,A5,PSCOMP_1:23,SPRECT_2:13;
A7: q1 in E-most L~h by A4,A5,SPRECT_2:13;
then q1 in the carrier of T by A2,FUNCT_2:def 1;
hence thesis by A2,A7,A6,FUNCT_1:def 6;
end;
thus (proj2 | E-most L~h).:the carrier of T c= X
proof
let x be object;
A8: E-most L~h c= L~h by XBOOLE_1:17;
assume x in (proj2 | E-most L~h).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A9: x1 in the carrier of T and
A10: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|(E-most L~h)) by A9;
then
A11: x1 in E-most L~h by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
A12: x2`1 = (E-min L~h)`1 by A11,PSCOMP_1:47
.= E-bound L~h by EUCLID:52;
x = x2`2 by A10,A11,PSCOMP_1:23;
hence thesis by A1,A11,A12,A8;
end;
end;
theorem Th15:
for X being Subset of REAL st X = { q`1 : q`2 = N-bound L~h & q
in L~h } holds X = (proj1 | N-most L~h).:the carrier of (TOP-REAL 2)|(N-most L~
h)
proof
set T = (TOP-REAL 2)|(N-most L~h);
set F = proj1 | N-most L~h;
let X be Subset of REAL such that
A1: X = { q`1 : q`2 = N-bound L~h & q in L~h };
thus X c= (proj1 | N-most L~h).:the carrier of T
proof
let x be object;
A2: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|(N-most L~h))
.= N-most L~h by PRE_TOPC:def 5;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A3: q1`1 = x and
A4: q1`2 = N-bound L~h and
A5: q1 in L~h by A1;
A6: x = F.q1 by A3,A4,A5,PSCOMP_1:22,SPRECT_2:10;
A7: q1 in N-most L~h by A4,A5,SPRECT_2:10;
then q1 in the carrier of T by A2,FUNCT_2:def 1;
hence thesis by A2,A7,A6,FUNCT_1:def 6;
end;
thus (proj1 | N-most L~h).:the carrier of T c= X
proof
let x be object;
A8: N-most L~h c= L~h by XBOOLE_1:17;
assume x in (proj1 | N-most L~h).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A9: x1 in the carrier of T and
A10: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|(N-most L~h)) by A9;
then
A11: x1 in N-most L~h by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
A12: x2`2 = (N-min L~h)`2 by A11,PSCOMP_1:39
.= N-bound L~h by EUCLID:52;
x = x2`1 by A10,A11,PSCOMP_1:22;
hence thesis by A1,A11,A12,A8;
end;
end;
theorem Th16:
for X being Subset of REAL st X = { q`1 : q`2 = S-bound L~h & q
in L~h } holds X = (proj1 | S-most L~h).:the carrier of (TOP-REAL 2)|(S-most L~
h)
proof
set T = (TOP-REAL 2)|(S-most L~h);
set F = proj1 | S-most L~h;
let X be Subset of REAL such that
A1: X = { q`1 : q`2 = S-bound L~h & q in L~h };
thus X c= (proj1 | S-most L~h).:the carrier of T
proof
let x be object;
A2: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|(S-most L~h))
.= S-most L~h by PRE_TOPC:def 5;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A3: q1`1 = x and
A4: q1`2 = S-bound L~h and
A5: q1 in L~h by A1;
A6: x = F.q1 by A3,A4,A5,PSCOMP_1:22,SPRECT_2:11;
A7: q1 in S-most L~h by A4,A5,SPRECT_2:11;
then q1 in the carrier of T by A2,FUNCT_2:def 1;
hence thesis by A2,A7,A6,FUNCT_1:def 6;
end;
thus (proj1 | S-most L~h).:the carrier of T c= X
proof
let x be object;
A8: S-most L~h c= L~h by XBOOLE_1:17;
assume x in (proj1 | S-most L~h).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A9: x1 in the carrier of T and
A10: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|(S-most L~h)) by A9;
then
A11: x1 in S-most L~h by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
A12: x2`2 = (S-min L~h)`2 by A11,PSCOMP_1:55
.= S-bound L~h by EUCLID:52;
x = x2`1 by A10,A11,PSCOMP_1:22;
hence thesis by A1,A11,A12,A8;
end;
end;
theorem Th17:
for X being Subset of REAL st X = { q`1 : q in L~g } holds X = (
proj1 | L~g).:the carrier of (TOP-REAL 2)|L~g
proof
set T = (TOP-REAL 2)|L~g;
set F = proj1 | L~g;
let X be Subset of REAL such that
A1: X = { q`1 : q in L~g };
thus X c= (proj1 | L~g).:the carrier of T
proof
let x be object;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A2: q1`1 = x and
A3: q1 in L~g by A1;
A4: x = F.q1 by A2,A3,PSCOMP_1:22;
A5: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|L~g)
.= L~g by PRE_TOPC:def 5;
then q1 in the carrier of T by A3,FUNCT_2:def 1;
hence thesis by A3,A5,A4,FUNCT_1:def 6;
end;
thus (proj1 | L~g).:the carrier of T c= X
proof
let x be object;
assume x in (proj1 | L~g).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A6: x1 in the carrier of T and
A7: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|L~g) by A6;
then
A8: x1 in L~g by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
x = x2`1 by A7,A8,PSCOMP_1:22;
hence thesis by A1,A8;
end;
end;
theorem Th18:
for X being Subset of REAL st X = { q`2 : q in L~g } holds X = (
proj2 | L~g).:the carrier of (TOP-REAL 2)|L~g
proof
set T = (TOP-REAL 2)|L~g;
set F = proj2 | L~g;
let X be Subset of REAL such that
A1: X = { q`2 : q in L~g };
thus X c= (proj2 | L~g).:the carrier of T
proof
let x be object;
assume x in X;
then consider q1 being Point of TOP-REAL 2 such that
A2: q1`2 = x and
A3: q1 in L~g by A1;
A4: x = F.q1 by A2,A3,PSCOMP_1:23;
A5: dom F = the carrier of T by FUNCT_2:def 1
.= [#] ((TOP-REAL 2)|L~g)
.= L~g by PRE_TOPC:def 5;
then q1 in the carrier of T by A3,FUNCT_2:def 1;
hence thesis by A3,A5,A4,FUNCT_1:def 6;
end;
thus (proj2 | L~g).:the carrier of T c= X
proof
let x be object;
assume x in (proj2 | L~g).:the carrier of T;
then consider x1 be object such that
x1 in dom F and
A6: x1 in the carrier of T and
A7: x = F.x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2)|L~g) by A6;
then
A8: x1 in L~g by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of TOP-REAL 2;
x = x2`2 by A7,A8,PSCOMP_1:23;
hence thesis by A1,A8;
end;
end;
theorem
for X being Subset of REAL st X = { q`2 : q`1 = W-bound L~h & q in L~h
} holds lower_bound X = lower_bound (proj2 | W-most L~h) by Th13;
theorem
for X being Subset of REAL st X = { q`2 : q`1 = W-bound L~h & q in L~h
} holds upper_bound X = upper_bound (proj2 | W-most L~h) by Th13;
theorem
for X being Subset of REAL st X = { q`2 : q`1 = E-bound L~h & q in L~h
} holds lower_bound X = lower_bound (proj2 | E-most L~h) by Th14;
theorem
for X being Subset of REAL st X = { q`2 : q`1 = E-bound L~h & q in L~h
} holds upper_bound X = upper_bound (proj2 | E-most L~h) by Th14;
theorem
for X being Subset of REAL st X = { q`1 : q in L~g } holds lower_bound
X = lower_bound (proj1 | L~g) by Th17;
theorem
for X being Subset of REAL st X = { q`1 : q`2 = S-bound L~h & q in L~h
} holds lower_bound X = lower_bound (proj1 | S-most L~h) by Th16;
theorem
for X being Subset of REAL st X = { q`1 : q`2 = S-bound L~h & q in L~h
} holds upper_bound X = upper_bound (proj1 | S-most L~h) by Th16;
theorem
for X being Subset of REAL st X = { q`1 : q`2 = N-bound L~h & q in L~h
} holds lower_bound X = lower_bound (proj1 | N-most L~h) by Th15;
theorem
for X being Subset of REAL st X = { q`1 : q`2 = N-bound L~h & q in L~h
} holds upper_bound X = upper_bound (proj1 | N-most L~h) by Th15;
theorem
for X being Subset of REAL st X = { q`2 : q in L~g } holds lower_bound
X = lower_bound (proj2 | L~g) by Th18;
theorem
for X being Subset of REAL st X = { q`1 : q in L~g } holds upper_bound
X = upper_bound (proj1 | L~g) by Th17;
theorem
for X being Subset of REAL st X = { q`2 : q in L~g } holds upper_bound
X = upper_bound (proj2 | L~g) by Th18;
theorem Th31:
p in L~h & 1 <= I & I <= width GoB h implies (GoB h)*(1,I)`1 <= p`1
proof
assume that
A1: p in L~h and
A2: 1 <= I and
A3: I <= width GoB h;
consider i such that
A4: 1<=i and
A5: i+1<=len h and
A6: p in LSeg(h/.i,h/.(i+1)) by A1,SPPOL_2:14;
i<=i+1 by NAT_1:11;
then i<=len h by A5,XXREAL_0:2;
then
A7: (GoB h)*(1,I)`1<=(h/.i)`1 by A2,A3,A4,Th5;
1<=i+1 by NAT_1:11;
then
A8: (GoB h)*(1,I)`1<=(h/.(i+1))`1 by A2,A3,A5,Th5;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then (h/.i)`1<=p`1 by A6,TOPREAL1:3;
hence thesis by A7,XXREAL_0:2;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then (h/.(i+1))`1<=p`1 by A6,TOPREAL1:3;
hence thesis by A8,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th32:
p in L~h & 1 <= I & I <= width GoB h implies p`1 <= (GoB h)*(len GoB h,I)`1
proof
assume that
A1: p in L~h and
A2: 1 <= I and
A3: I <= width GoB h;
consider i such that
A4: 1<=i and
A5: i+1<=len h and
A6: p in LSeg(h/.i,h/.(i+1)) by A1,SPPOL_2:14;
i<=i+1 by NAT_1:11;
then i<=len h by A5,XXREAL_0:2;
then
A7: (GoB h)*(len GoB h,I)`1>=(h/.i)`1 by A2,A3,A4,Th5;
1<=i+1 by NAT_1:11;
then
A8: (GoB h)*(len GoB h,I)`1>=(h/.(i+1))`1 by A2,A3,A5,Th5;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then (h/.(i+1))`1>=p`1 by A6,TOPREAL1:3;
hence thesis by A8,XXREAL_0:2;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then (h/.i)`1>=p`1 by A6,TOPREAL1:3;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th33:
p in L~h & 1 <= I & I <= len GoB h implies (GoB h)*(I,1)`2 <= p `2
proof
assume that
A1: p in L~h and
A2: 1 <= I and
A3: I <= len GoB h;
consider i such that
A4: 1<=i and
A5: i+1<=len h and
A6: p in LSeg(h/.i,h/.(i+1)) by A1,SPPOL_2:14;
i<=i+1 by NAT_1:11;
then i<=len h by A5,XXREAL_0:2;
then
A7: (GoB h)*(I,1)`2<=(h/.i)`2 by A2,A3,A4,Th6;
1<=i+1 by NAT_1:11;
then
A8: (GoB h)*(I,1)`2<=(h/.(i+1))`2 by A2,A3,A5,Th6;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then (h/.i)`2<=p`2 by A6,TOPREAL1:4;
hence thesis by A7,XXREAL_0:2;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then (h/.(i+1))`2<=p`2 by A6,TOPREAL1:4;
hence thesis by A8,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th34:
p in L~h & 1 <= I & I <= len GoB h implies p`2 <= (GoB h)*(I, width GoB h)`2
proof
assume that
A1: p in L~h and
A2: 1 <= I and
A3: I <= len GoB h;
consider i such that
A4: 1<=i and
A5: i+1<=len h and
A6: p in LSeg(h/.i,h/.(i+1)) by A1,SPPOL_2:14;
i<=i+1 by NAT_1:11;
then i<=len h by A5,XXREAL_0:2;
then
A7: (GoB h)*(I,width GoB h)`2>=(h/.i)`2 by A2,A3,A4,Th6;
1<=i+1 by NAT_1:11;
then
A8: (GoB h)*(I,width GoB h)`2>=(h/.(i+1))`2 by A2,A3,A5,Th6;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then (h/.(i+1))`2>=p`2 by A6,TOPREAL1:4;
hence thesis by A8,XXREAL_0:2;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then (h/.i)`2>=p`2 by A6,TOPREAL1:4;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th35:
1 <= i & i <= len GoB h & 1 <= j & j <= width GoB h implies ex q
st q`1 = (GoB h)*(i,j)`1 & q in L~h
proof
assume that
A1: 1 <= i and
A2: i <= len GoB h and
A3: 1 <= j and
A4: j <= width GoB h;
consider k such that
A5: k in dom h and
[i,j] in Indices GoB h and
A6: (h/.k)`1 = (GoB h)* (i,j)`1 by A1,A2,A3,A4,Th9;
take q = h/.k;
thus q`1 = (GoB h)*(i,j)`1 by A6;
4 < len h by GOBOARD7:34;
hence thesis by A5,GOBOARD1:1,XXREAL_0:2;
end;
theorem Th36:
1 <= i & i <= len GoB h & 1 <= j & j <= width GoB h implies ex q
st q`2 = (GoB h)*(i,j)`2 & q in L~h
proof
assume that
A1: 1 <= i and
A2: i <= len GoB h and
A3: 1 <= j and
A4: j <= width GoB h;
consider k such that
A5: k in dom h and
[i,j] in Indices GoB h and
A6: (h/.k)`2 = (GoB h)*(i,j)`2 by A1,A2,A3,A4,Th10;
take q = h/.k;
thus q`2 = (GoB h)*(i,j)`2 by A6;
4 < len h by GOBOARD7:34;
hence thesis by A5,GOBOARD1:1,XXREAL_0:2;
end;
theorem Th37:
W-bound L~h = (GoB h)*(1,1)`1
proof
set X = { q`1 : q in L~h }, A = (GoB h)*(1,1)`1;
consider a be object such that
A1: a in L~h by XBOOLE_0:def 1;
A2: X c= REAL
proof
let b be object;
assume b in X;
then ex qq be Point of TOP-REAL 2 st b = qq`1 & qq in L~h;
hence thesis by XREAL_0:def 1;
end;
reconsider a as Point of TOP-REAL 2 by A1;
a`1 in X by A1;
then reconsider X as non empty Subset of REAL by A2;
lower_bound X = A
proof
A3: 1 <= width GoB h by GOBOARD7:33;
A4: for p be Real st p in X holds p >= A
proof
let p be Real;
assume p in X;
then ex s be Point of TOP-REAL 2 st p = s`1 & s in L~h;
hence thesis by A3,Th31;
end;
1 <= len GoB h by GOBOARD7:32;
then consider q1 be Point of TOP-REAL 2 such that
A5: q1`1 = (GoB h)*(1,1)`1 and
A6: q1 in L~h by A3,Th35;
reconsider q11 = q1`1 as Real;
for q be Real st for p be Real st p in X holds p >= q
holds A >= q
proof
A7: q11 in X by A6;
let q be Real;
assume for p be Real st p in X holds p >= q;
hence thesis by A5,A7;
end;
hence thesis by A4,SEQ_4:44;
end;
hence thesis by Th17;
end;
theorem Th38:
S-bound L~h = (GoB h)*(1,1)`2
proof
set X = { q`2 : q in L~h }, A = (GoB h)*(1,1)`2;
consider a be object such that
A1: a in L~h by XBOOLE_0:def 1;
A2: X c= REAL
proof
let b be object;
assume b in X;
then ex qq be Point of TOP-REAL 2 st b = qq`2 & qq in L~h;
hence thesis by XREAL_0:def 1;
end;
reconsider a as Point of TOP-REAL 2 by A1;
a`2 in X by A1;
then reconsider X as non empty Subset of REAL by A2;
lower_bound X = A
proof
A3: 1 <= len GoB h by GOBOARD7:32;
A4: for p be Real st p in X holds p >= A
proof
let p be Real;
assume p in X;
then ex s be Point of TOP-REAL 2 st p = s`2 & s in L~h;
hence thesis by A3,Th33;
end;
1 <= width GoB h by GOBOARD7:33;
then consider q1 be Point of TOP-REAL 2 such that
A5: q1`2 = (GoB h)*(1,1)`2 and
A6: q1 in L~h by A3,Th36;
reconsider q11 = q1`2 as Real;
for q be Real st for p be Real st p in X holds p >= q
holds A >= q
proof
A7: q11 in X by A6;
let q be Real;
assume for p be Real st p in X holds p >= q;
hence thesis by A5,A7;
end;
hence thesis by A4,SEQ_4:44;
end;
hence thesis by Th18;
end;
theorem Th39:
E-bound L~h = (GoB h)*(len GoB h,1)`1
proof
set X = { q`1 : q in L~h }, A = (GoB h)*(len GoB h,1)`1;
consider a be object such that
A1: a in L~h by XBOOLE_0:def 1;
A2: X c= REAL
proof
let b be object;
assume b in X;
then ex qq be Point of TOP-REAL 2 st b = qq`1 & qq in L~h;
hence thesis by XREAL_0:def 1;
end;
reconsider a as Point of TOP-REAL 2 by A1;
a`1 in X by A1;
then reconsider X as non empty Subset of REAL by A2;
upper_bound X = A
proof
A3: for p be Real st p in X holds p <= A
proof
let p be Real;
assume p in X;
then
A4: ex s be Point of TOP-REAL 2 st p = s`1 & s in L~h;
1 <= width GoB h by GOBOARD7:33;
hence thesis by A4,Th32;
end;
A5: 1 <= width GoB h by GOBOARD7:33;
1 <= len GoB h by GOBOARD7:32;
then consider q1 be Point of TOP-REAL 2 such that
A6: q1`1 = (GoB h)*(len GoB h,1)`1 and
A7: q1 in L~h by A5,Th35;
reconsider q11 = q1`1 as Real;
for q be Real st for p be Real st p in X holds p <= q
holds A <= q
proof
A8: q11 in X by A7;
let q be Real;
assume for p be Real st p in X holds p <= q;
hence thesis by A6,A8;
end;
hence thesis by A3,SEQ_4:46;
end;
hence thesis by Th17;
end;
theorem Th40:
N-bound L~h = (GoB h)*(1,width GoB h)`2
proof
set X = { q`2 : q in L~h }, A = (GoB h)*(1,width GoB h)`2;
consider a be object such that
A1: a in L~h by XBOOLE_0:def 1;
A2: X c= REAL
proof
let b be object;
assume b in X;
then ex qq be Point of TOP-REAL 2 st b = qq`2 & qq in L~h;
hence thesis by XREAL_0:def 1;
end;
reconsider a as Point of TOP-REAL 2 by A1;
a`2 in X by A1;
then reconsider X as non empty Subset of REAL by A2;
upper_bound X = A
proof
A3: 1 <= len GoB h by GOBOARD7:32;
A4: for p be Real st p in X holds p <= A
proof
let p be Real;
assume p in X;
then ex s be Point of TOP-REAL 2 st p = s`2 & s in L~h;
hence thesis by A3,Th34;
end;
1 <= width GoB h by GOBOARD7:33;
then consider q1 be Point of TOP-REAL 2 such that
A5: q1`2 = (GoB h)*(1,width GoB h)`2 and
A6: q1 in L~h by A3,Th36;
reconsider q11 = q1`2 as Real;
for q be Real st for p be Real st p in X holds p <= q
holds A <= q
proof
A7: q11 in X by A6;
let q be Real;
assume for p be Real st p in X holds p <= q;
hence thesis by A5,A7;
end;
hence thesis by A4,SEQ_4:46;
end;
hence thesis by Th18;
end;
theorem Th41:
for Y being non empty finite Subset of NAT st 1 <= i & i <= len
f & 1 <= I & I <= len GoB f &
Y = { j where j is Element of NAT: [I,j] in Indices GoB f & ex k st k in
dom f & f/.k = (GoB f)*(I,j) } & (f/.i)`1 = ((GoB f)*(I,1))`1 & i1 = min Y
holds (GoB f)*(I,i1)`2 <= (f/.i)`2
proof
let Y be non empty finite Subset of NAT;
A1: f/.i=|[(f/.i)`1,(f/.i)`2]| by EUCLID:53;
assume
A2: 1<=i & i<=len f & 1<=I & I<=len GoB f &
Y={j where j is Element of NAT:[I,j] in Indices GoB f
& ex k st k in dom f & f/.k=(GoB f)*(I,j)} & (f/.i)`1=((GoB f)*(I,1))`1 & i1=
min Y;
then
A3: i in dom f by FINSEQ_3:25;
then consider i2,j2 be Nat such that
A4: [i2,j2] in Indices GoB f and
A5: f/.i=(GoB f)*(i2,j2) by GOBOARD5:11;
A6: j2<=width GoB f by A4,MATRIX_0:32;
A7: 1<=j2 by A4,MATRIX_0:32;
then
A8: [I,j2] in Indices GoB f by A2,A6,MATRIX_0:30;
A9: i2<=len GoB f by A4,MATRIX_0:32;
1<=i2 by A4,MATRIX_0:32;
then
A10: (f/.i)`2=((GoB f)*(1,j2))`2 by A5,A9,A7,A6,GOBOARD5:1
.=((GoB f)*(I,j2))`2 by A2,A7,A6,GOBOARD5:1;
i1 in Y by A2,XXREAL_2:def 7;
then ex j being Element of NAT
st i1=j & [I,j] in Indices GoB f & ex k st k in dom f & f/.k=(
GoB f)*(I,j) by A2;
then
A11: 1<=i1 by MATRIX_0:32;
A12: j2 in NAT by ORDINAL1:def 12;
(f/.i)`1=((GoB f)*(I,j2))`1 by A2,A7,A6,GOBOARD5:2;
then f/.i=(GoB f)*(I,j2) by A10,A1,EUCLID:53;
then j2 in Y by A2,A3,A8,A12;
then
A13: i1<=j2 by A2,XXREAL_2:def 7;
A14: j2<=width GoB f by A4,MATRIX_0:32;
now
per cases;
case
i1<j2;
hence (GoB f)*(I,i1)`2<=(GoB f)*(I,j2)`2 by A2,A11,A14,GOBOARD5:4;
end;
case
i1>=j2;
hence (GoB f)*(I,i1)`2<=(GoB f)*(I,j2)`2 by A13,XXREAL_0:1;
end;
end;
hence thesis by A10;
end;
theorem Th42:
for Y being non empty finite Subset of NAT st 1 <= i & i <= len
h & 1 <= I & I <= width GoB h &
Y = { j where j is Element of NAT: [j,I] in Indices GoB h & ex k st k in
dom h & h/.k = (GoB h)*(j,I) } & (h/.i)`2 = ((GoB h)* (1,I))`2 & i1 = min Y
holds (GoB h)*(i1,I)`1 <= (h/.i)`1
proof
let Y be non empty finite Subset of NAT;
A1: h/.i=|[(h/.i)`1,(h/.i)`2]| by EUCLID:53;
assume
A2: 1<=i & i<=len h & 1 <= I & I <= width GoB h &
Y={j where j is Element of NAT:[j,I] in Indices
GoB h & ex k st k in dom h & h/.k=(GoB h)*(j,I)} & (h/.i)`2=((GoB h)*(1,I))`2 &
i1=min Y;
then
A3: i in dom h by FINSEQ_3:25;
then consider i2,j2 be Nat such that
A4: [i2,j2] in Indices GoB h and
A5: h/.i=(GoB h)*(i2,j2) by GOBOARD5:11;
A6: i2<=len GoB h by A4,MATRIX_0:32;
A7: 1<=i2 by A4,MATRIX_0:32;
then
A8: [i2,I] in Indices GoB h by A2,A6,MATRIX_0:30;
A9: j2<=width GoB h by A4,MATRIX_0:32;
1<=j2 by A4,MATRIX_0:32;
then
A10: (h/.i)`1=((GoB h)*(i2,1))`1 by A5,A7,A6,A9,GOBOARD5:2
.=((GoB h)*(i2,I))`1 by A2,A7,A6,GOBOARD5:2;
i1 in Y by A2,XXREAL_2:def 7;
then ex j being Element of NAT
st i1=j & [j,I] in Indices GoB h & ex k st k in dom h & h/.k=(
GoB h)*(j,I) by A2;
then
A11: 1<=i1 by MATRIX_0:32;
A12: i2 in NAT by ORDINAL1:def 12;
(h/.i)`2=((GoB h)*(i2,I))`2 by A2,A7,A6,GOBOARD5:1;
then h/.i=(GoB h)*(i2,I) by A10,A1,EUCLID:53;
then i2 in Y by A2,A3,A8,A12;
then
A13: i1<=i2 by A2,XXREAL_2:def 7;
A14: i2<=len GoB h by A4,MATRIX_0:32;
now
per cases;
case
i1<i2;
hence (GoB h)*(i1,I)`1<=(GoB h)*(i2,I)`1 by A2,A11,A14,GOBOARD5:3;
end;
case
i1>=i2;
hence (GoB h)*(i1,I)`1<=(GoB h)*(i2,I)`1 by A13,XXREAL_0:1;
end;
end;
hence thesis by A10;
end;
theorem Th43:
for Y being non empty finite Subset of NAT st 1 <= i & i <= len
h & 1 <= I & I <= width GoB h &
Y = { j where j is Element of NAT: [j,I] in Indices GoB h & ex k st k in
dom h & h/.k = (GoB h)*(j,I) } & (h/.i)`2 = ((GoB h)* (1,I))`2 & i1 = max Y
holds (GoB h)*(i1,I)`1 >= (h/.i)`1
proof
let Y be non empty finite Subset of NAT;
A1: h/.i=|[(h/.i)`1,(h/.i)`2]| by EUCLID:53;
assume
A2: 1<=i & i<=len h & 1<=I & I<=width GoB h &
Y={j where j is Element of NAT:[j,I] in Indices GoB
h & ex k st k in dom h & h/.k=(GoB h)*(j,I)} & (h/.i)`2=((GoB h)* (1,I))`2 & i1
=max Y;
then
A3: i in dom h by FINSEQ_3:25;
then consider i2,j2 be Nat such that
A4: [i2,j2] in Indices GoB h and
A5: h/.i=(GoB h)*(i2,j2) by GOBOARD5:11;
A6: 1<=i2 by A4,MATRIX_0:32;
A7: i2<=len GoB h by A4,MATRIX_0:32;
then
A8: [i2,I] in Indices GoB h by A2,A6,MATRIX_0:30;
A9: j2<=width GoB h by A4,MATRIX_0:32;
1<=j2 by A4,MATRIX_0:32;
then
A10: (h/.i)`1=((GoB h)*(i2,1))`1 by A5,A6,A7,A9,GOBOARD5:2
.=((GoB h)*(i2,I))`1 by A2,A6,A7,GOBOARD5:2;
i1 in Y by A2,XXREAL_2:def 8;
then ex j being Element of NAT
st i1=j & [j,I] in Indices GoB h & ex k st k in dom h & h/.k=(
GoB h)*(j,I) by A2;
then
A11: i1 <= len GoB h by MATRIX_0:32;
A12: i2 in NAT by ORDINAL1:def 12;
(h/.i)`2=((GoB h)*(i2,I))`2 by A2,A6,A7,GOBOARD5:1;
then h/.i=(GoB h)*(i2,I) by A10,A1,EUCLID:53;
then i2 in Y by A2,A3,A8,A12;
then
A13: i1>=i2 by A2,XXREAL_2:def 8;
now
per cases;
case
i1>i2;
hence (GoB h)*(i1,I)`1>=(GoB h)*(i2,I)`1 by A2,A6,A11,GOBOARD5:3;
end;
case
i1<=i2;
hence (GoB h)*(i1,I)`1>=(GoB h)*(i2,I)`1 by A13,XXREAL_0:1;
end;
end;
hence thesis by A10;
end;
theorem Th44:
for Y being non empty finite Subset of NAT st 1 <= i & i <= len
f & 1 <= I & I <= len GoB f &
Y = { j where j is Element of NAT: [I,j] in Indices GoB f & ex k st k in
dom f & f/.k = (GoB f)*(I,j) } & (f/.i)`1 = ((GoB f)* (I,1))`1 & i1 = max Y
holds (GoB f)*(I,i1)`2 >= (f/.i)`2
proof
let Y be non empty finite Subset of NAT;
A1: f/.i=|[(f/.i)`1,(f/.i)`2]| by EUCLID:53;
assume
A2: 1<=i & i<=len f & 1 <= I & I <= len GoB f &
Y={j where j is Element of NAT:[I,j] in Indices
GoB f & ex k st k in dom f & f/.k=(GoB f)*(I,j)} & (f/.i)`1=((GoB f)*(I,1))`1 &
i1=max Y;
then
A3: i in dom f by FINSEQ_3:25;
then consider i2,j2 be Nat such that
A4: [i2,j2] in Indices GoB f and
A5: f/.i=(GoB f)*(i2,j2) by GOBOARD5:11;
A6: 1<=j2 by A4,MATRIX_0:32;
A7: j2<=width GoB f by A4,MATRIX_0:32;
then
A8: [I,j2] in Indices GoB f by A2,A6,MATRIX_0:30;
A9: i2<=len GoB f by A4,MATRIX_0:32;
1<=i2 by A4,MATRIX_0:32;
then
A10: (f/.i)`2=((GoB f)*(1,j2))`2 by A5,A9,A6,A7,GOBOARD5:1
.=((GoB f)*(I,j2))`2 by A2,A6,A7,GOBOARD5:1;
i1 in Y by A2,XXREAL_2:def 8;
then ex j being Element of NAT
st i1=j & [I,j] in Indices GoB f & ex k st k in dom f & f/.k=(
GoB f)*(I,j) by A2;
then
A11: i1<=width GoB f by MATRIX_0:32;
A12: j2 in NAT by ORDINAL1:def 12;
(f/.i)`1=((GoB f)*(I,j2))`1 by A2,A6,A7,GOBOARD5:2;
then f/.i=(GoB f)*(I,j2) by A10,A1,EUCLID:53;
then j2 in Y by A2,A3,A8,A12;
then
A13: i1>=j2 by A2,XXREAL_2:def 8;
now
per cases;
case
i1 > j2;
hence (GoB f)*(I,i1)`2 >= (GoB f)*(I,j2)`2 by A2,A11,A6,GOBOARD5:4;
end;
case
i1<=j2;
hence (GoB f)*(I,i1)`2 >= (GoB f)*(I,j2)`2 by A13,XXREAL_0:1;
end;
end;
hence thesis by A10;
end;
Lm1: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`1=W-bound L~h & p in L~h &
Y={j where j is Element of NAT:[1,j] in Indices GoB h & ex i st i in
dom h & h/.i=(GoB h)*(1,j)} & i1=min Y holds (GoB h)*(1,i1)`2<=p`2
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
A1: 1 <= len GoB h by GOBOARD7:32;
assume
A2: p`1=W-bound L~h & p in L~h &
Y={j where j is Element of NAT:[1,j] in Indices GoB h & ex i st i
in dom h & h/.i=(GoB h)*(1,j)} & i1=min Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`1=((GoB h)*(1,1))`1 by A2,Th37;
A9: 1 <= width GoB h by GOBOARD7:33;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A11: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A12: p`1=(h/.(i+1))`1 by A5,A10,GOBOARD7:5;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then
A13: (h/.i)`2<=p`2 by A5,TOPREAL1:4;
(GoB h)*(1,i1)`2<=(h/.i)`2 by A2,A8,A1,A3,A7,A11,Th41;
hence thesis by A13,XXREAL_0:2;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then
A14: (h/.(i+1))`2<=p`2 by A5,TOPREAL1:4;
(GoB h)*(1,i1)`2<=(h/.(i+1))`2 by A2,A8,A1,A4,A6,A12,Th41;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A16: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A17: p`2=(h/.(i+1))`2 by A5,A15,GOBOARD7:6;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then
A18: (h/.i)`1<=((GoB h)*(1,1))`1 by A8,A5,TOPREAL1:3;
(h/.i)`1>=((GoB h)*(1,1))`1 by A9,A3,A7,Th5;
then (h/.i)`1=((GoB h)*(1,1))`1 by A18,XXREAL_0:1;
hence thesis by A2,A1,A3,A7,A16,Th41;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then
A19: (h/.(i+1))`1<=((GoB h)*(1,1))`1 by A8,A5,TOPREAL1:3;
(h/.(i+1))`1>=((GoB h)*(1,1))`1 by A9,A4,A6,Th5;
then (h/.(i+1))`1=((GoB h)*(1,1))`1 by A19,XXREAL_0:1;
hence thesis by A2,A1,A4,A6,A17,Th41;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm2: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`1=W-bound L~h & p in L~h &
Y={j where j is Element of NAT:[1,j] in Indices GoB h & ex i st i in
dom h & h/.i=(GoB h)*(1,j)} & i1=max Y holds (GoB h)*(1,i1)`2 >= p`2
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
A1: 1 <= len GoB h by GOBOARD7:32;
assume
A2: p`1=W-bound L~h & p in L~h &
Y={j where j is Element of NAT:[1,j] in Indices GoB h & ex i st i
in dom h & h/.i=(GoB h)*(1,j)} & i1=max Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`1=((GoB h)*(1,1))`1 by A2,Th37;
A9: 1 <= width GoB h by GOBOARD7:33;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A11: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A12: p`1=(h/.(i+1))`1 by A5,A10,GOBOARD7:5;
now
per cases;
case
(h/.i)`2>=(h/.(i+1))`2;
then
A13: (h/.i)`2 >= p`2 by A5,TOPREAL1:4;
(GoB h)*(1,i1)`2>=(h/.i)`2 by A2,A8,A3,A1,A7,A11,Th44;
hence thesis by A13,XXREAL_0:2;
end;
case
(h/.i)`2<(h/.(i+1))`2;
then
A14: (h/.(i+1))`2>=p`2 by A5,TOPREAL1:4;
(GoB h)*(1,i1)`2>=(h/.(i+1))`2 by A2,A8,A4,A1,A6,A12,Th44;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A16: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A17: p`2=(h/.(i+1))`2 by A5,A15,GOBOARD7:6;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then
A18: (h/.i)`1<=((GoB h)*(1,1))`1 by A8,A5,TOPREAL1:3;
(h/.i)`1>=((GoB h)*(1,1))`1 by A3,A9,A7,Th5;
then (h/.i)`1=((GoB h)*(1,1))`1 by A18,XXREAL_0:1;
hence thesis by A2,A3,A1,A7,A16,Th44;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then
A19: (h/.(i+1))`1<=((GoB h)*(1,1))`1 by A8,A5,TOPREAL1:3;
(h/.(i+1))`1>=((GoB h)*(1,1))`1 by A4,A9,A6,Th5;
then (h/.(i+1))`1=((GoB h)*(1,1))`1 by A19,XXREAL_0:1;
hence thesis by A2,A4,A1,A6,A17,Th44;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm3: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`1=E-bound L~h & p in L~h &
Y={j where j is Element of NAT:[len GoB h,j] in Indices GoB h & ex i st
i in dom h & h/.i=(GoB h)*(len GoB h,j)} & i1=min Y holds (GoB h)*(len GoB h,i1
)`2<=p`2
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
A1: 1 <= len GoB h by GOBOARD7:32;
assume
A2: p`1=E-bound L~h & p in L~h &
Y={j where j is Element of NAT:[len GoB h,j] in Indices GoB h &
ex i st i in dom h & h/.i=(GoB h)*(len GoB h,j)} & i1=min Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`1=((GoB h)*(len GoB h,1))`1 by A2,Th39;
A9: 1 <= width GoB h by GOBOARD7:33;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A11: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A12: p`1=(h/.(i+1))`1 by A5,A10,GOBOARD7:5;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then
A13: (h/.i)`2<=p`2 by A5,TOPREAL1:4;
(GoB h)*(len GoB h,i1)`2<=(h/.i)`2 by A2,A8,A3,A7,A1,A11,Th41;
hence thesis by A13,XXREAL_0:2;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then
A14: (h/.(i+1))`2<=p`2 by A5,TOPREAL1:4;
(GoB h)*(len GoB h,i1)`2<=(h/.(i+1))`2 by A2,A8,A4,A6,A1,A12,Th41;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A16: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A17: p`2=(h/.(i+1))`2 by A5,A15,GOBOARD7:6;
now
per cases;
case
(h/.i)`1>=(h/.(i+1))`1;
then
A18: (h/.i)`1>=((GoB h)*(len GoB h,1))`1 by A8,A5,TOPREAL1:3;
(h/.i)`1<=((GoB h)*(len GoB h,1))`1 by A9,A3,A7,Th5;
then (h/.i)`1=((GoB h)*(len GoB h,1))`1 by A18,XXREAL_0:1;
hence thesis by A2,A3,A7,A1,A16,Th41;
end;
case
(h/.i)`1<(h/.(i+1))`1;
then
A19: (h/.(i+1))`1>=((GoB h)*(len GoB h,1))`1 by A8,A5,TOPREAL1:3;
(h/.(i+1))`1<=((GoB h)*(len GoB h,1))`1 by A9,A4,A6,Th5;
then (h/.(i+1))`1=((GoB h)*(len GoB h,1))`1 by A19,XXREAL_0:1;
hence thesis by A2,A4,A6,A1,A17,Th41;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm4: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`1=E-bound L~h & p in L~h &
Y={j where j is Element of NAT:[len GoB h,j] in Indices GoB h & ex i st
i in dom h & h/.i=(GoB h)*(len GoB h,j)} & i1=max Y holds (GoB h)*(len GoB h,i1
)`2 >= p`2
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
A1: 1 <= len GoB h by GOBOARD7:32;
assume
A2: p`1=E-bound L~h & p in L~h &
Y={j where j is Element of NAT:[len GoB h,j] in Indices GoB h &
ex i st i in dom h & h/.i=(GoB h)*(len GoB h,j)} & i1=max Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`1=((GoB h)*(len GoB h,1))`1 by A2,Th39;
A9: 1 <= width GoB h by GOBOARD7:33;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A11: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A12: p`1=(h/.(i+1))`1 by A5,A10,GOBOARD7:5;
per cases;
suppose
(h/.i)`2>=(h/.(i+1))`2;
then
A13: (h/.i)`2 >= p`2 by A5,TOPREAL1:4;
(GoB h)*(len GoB h,i1)`2>=(h/.i)`2 by A2,A8,A1,A3,A7,A11,Th44;
hence thesis by A13,XXREAL_0:2;
end;
suppose
(h/.i)`2<(h/.(i+1))`2;
then
A14: (h/.(i+1))`2>=p`2 by A5,TOPREAL1:4;
(GoB h)*(len GoB h,i1)`2>=(h/.(i+1))`2 by A2,A8,A1,A4,A6,A12,Th44;
hence thesis by A14,XXREAL_0:2;
end;
end;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A16: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A17: p`2=(h/.(i+1))`2 by A5,A15,GOBOARD7:6;
now
per cases;
case
(h/.i)`1>=(h/.(i+1))`1;
then
A18: (h/.i)`1>=((GoB h)*(len GoB h,1))`1 by A8,A5,TOPREAL1:3;
(h/.i)`1<=((GoB h)*(len GoB h,1))`1 by A9,A3,A7,Th5;
then (h/.i)`1=((GoB h)*(len GoB h,1))`1 by A18,XXREAL_0:1;
hence thesis by A2,A1,A3,A7,A16,Th44;
end;
case
(h/.i)`1<(h/.(i+1))`1;
then
A19: (h/.(i+1))`1>=((GoB h)*(len GoB h,1))`1 by A8,A5,TOPREAL1:3;
(h/.(i+1))`1<=((GoB h)*(len GoB h,1))`1 by A9,A4,A6,Th5;
then (h/.(i+1))`1=((GoB h)*(len GoB h,1))`1 by A19,XXREAL_0:1;
hence thesis by A2,A1,A4,A6,A17,Th44;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm5: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`2=S-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,1] in Indices GoB h & ex i st i in
dom h & h/.i=(GoB h)*(j,1)} & i1=min Y holds (GoB h)*(i1,1)`1<=p`1
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
A1: 1 <= width GoB h by GOBOARD7:33;
assume
A2: p`2=S-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,1] in Indices GoB h & ex i st i
in dom h & h/.i=(GoB h)*(j,1)} & i1=min Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`2=((GoB h)*(1,1))`2 by A2,Th38;
A9: 1 <= len GoB h by GOBOARD7:32;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A11: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A12: p`2=(h/.(i+1))`2 by A5,A10,GOBOARD7:6;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then
A13: (h/.i)`1<=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,1)`1<=(h/.i)`1 by A2,A8,A3,A7,A1,A11,Th42;
hence thesis by A13,XXREAL_0:2;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then
A14: (h/.(i+1))`1<=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,1)`1<=(h/.(i+1))`1 by A2,A8,A4,A1,A6,A12,Th42;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A16: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A17: p`1=(h/.(i+1))`1 by A5,A15,GOBOARD7:5;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then
A18: (h/.i)`2<=((GoB h)*(1,1))`2 by A8,A5,TOPREAL1:4;
(h/.i)`2>=((GoB h)*(1,1))`2 by A3,A7,A9,Th6;
then (h/.i)`2=((GoB h)*(1,1))`2 by A18,XXREAL_0:1;
hence thesis by A2,A3,A7,A1,A16,Th42;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then
A19: (h/.(i+1))`2<=((GoB h)*(1,1))`2 by A8,A5,TOPREAL1:4;
(h/.(i+1))`2>=((GoB h)*(1,1))`2 by A4,A9,A6,Th6;
then (h/.(i+1))`2=((GoB h)*(1,1))`2 by A19,XXREAL_0:1;
hence thesis by A2,A4,A1,A6,A17,Th42;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm6: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT,
h st p`2=N-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,width GoB h] in Indices GoB h & ex i
st i in dom h & h/.i=(GoB h)*(j,width GoB h)} & i1=min Y holds (GoB h)*(i1,
width GoB h)`1<=p`1
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT,h;
set I = width GoB h;
A1: 1 <= I by GOBOARD7:33;
assume
A2: p`2=N-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,width GoB h] in Indices GoB h &
ex i st i in dom h & h/.i=(GoB h)*(j,width GoB h)} & i1=min Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: p`2=((GoB h)*(1,width GoB h))`2 by A2,Th40;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: 1<=i+1 by A3,XREAL_1:145;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A9: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A10: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A11: p`2=(h/.(i+1))`2 by A5,A9,GOBOARD7:6;
now
per cases;
case
(h/.i)`1<=(h/.(i+1))`1;
then
A12: (h/.i)`1<=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,I)`1<=(h/.i)`1 by A2,A6,A1,A3,A7,A10,Th42;
hence thesis by A12,XXREAL_0:2;
end;
case
(h/.i)`1>(h/.(i+1))`1;
then
A13: (h/.(i+1))`1<=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,I)`1<=(h/.(i+1))`1 by A2,A6,A1,A4,A8,A11,Th42;
hence thesis by A13,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A14: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A15: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A16: 1 <= len GoB h by GOBOARD7:32;
A17: p`1=(h/.(i+1))`1 by A5,A14,GOBOARD7:5;
now
per cases;
case
(h/.i)`2>=(h/.(i+1))`2;
then
A18: (h/.i)`2>=((GoB h)*(1,I))`2 by A6,A5,TOPREAL1:4;
(h/.i)`2<=((GoB h)*(1,I))`2 by A3,A7,A16,Th6;
then (h/.i)`2=((GoB h)*(1,I))`2 by A18,XXREAL_0:1;
hence thesis by A2,A1,A3,A7,A15,Th42;
end;
case
(h/.i)`2<(h/.(i+1))`2;
then
A19: (h/.(i+1))`2>=((GoB h)*(1,I))`2 by A6,A5,TOPREAL1:4;
(h/.(i+1))`2 <= ((GoB h)*(1,I))`2 by A4,A8,A16,Th6;
then (h/.(i+1))`2=((GoB h)*(1,I))`2 by A19,XXREAL_0:1;
hence thesis by A2,A1,A4,A8,A17,Th42;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm7: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT
st p`2=S-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,1] in Indices GoB h & ex i st i in dom
h & h/.i=(GoB h)*(j,1)} & i1=max Y holds (GoB h)*(i1,1)`1>=p`1
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT;
A1: 1 <= width GoB h by GOBOARD7:33;
assume
A2: p`2=S-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,1] in Indices GoB h & ex i st i
in dom h & h/.i=(GoB h)*(j,1)} & i1=max Y;
then consider i such that
A3: 1<=i and
A4: i+1<=len h and
A5: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A6: 1<=i+1 by A3,XREAL_1:145;
i<=i+1 by NAT_1:11;
then
A7: i<=len h by A4,XXREAL_0:2;
A8: p`2=((GoB h)*(1,1))`2 by A2,Th38;
A9: 1 <= len GoB h by GOBOARD7:32;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A3,A4,TOPREAL1:def 3;
then
A10: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A11: p`2=(h/.i)`2 by A5,GOBOARD7:6;
A12: p`2=(h/.(i+1))`2 by A5,A10,GOBOARD7:6;
now
per cases;
case
(h/.i)`1>=(h/.(i+1))`1;
then
A13: (h/.i)`1>=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,1)`1>=(h/.i)`1 by A2,A8,A3,A7,A1,A11,Th43;
hence thesis by A13,XXREAL_0:2;
end;
case
(h/.i)`1<(h/.(i+1))`1;
then
A14: (h/.(i+1))`1>=p`1 by A5,TOPREAL1:3;
(GoB h)*(i1,1)`1>=(h/.(i+1))`1 by A2,A8,A4,A1,A6,A12,Th43;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A3,A4,TOPREAL1:def 3;
then
A15: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A16: p`1=(h/.i)`1 by A5,GOBOARD7:5;
A17: p`1=(h/.(i+1))`1 by A5,A15,GOBOARD7:5;
now
per cases;
case
(h/.i)`2<=(h/.(i+1))`2;
then
A18: (h/.i)`2<=((GoB h)*(1,1))`2 by A8,A5,TOPREAL1:4;
(h/.i)`2>=((GoB h)*(1,1))`2 by A3,A7,A9,Th6;
then (h/.i)`2=((GoB h)*(1,1))`2 by A18,XXREAL_0:1;
hence thesis by A2,A3,A7,A1,A16,Th43;
end;
case
(h/.i)`2>(h/.(i+1))`2;
then
A19: (h/.(i+1))`2<=((GoB h)*(1,1))`2 by A8,A5,TOPREAL1:4;
(h/.(i+1))`2>=((GoB h)*(1,1))`2 by A4,A9,A6,Th6;
then (h/.(i+1))`2=((GoB h)*(1,1))`2 by A19,XXREAL_0:1;
hence thesis by A2,A4,A1,A6,A17,Th43;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm8: for p being Point of TOP-REAL 2, Y being non empty finite Subset of NAT
st p`2=N-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,width GoB h] in Indices GoB h & ex i st
i in dom h & h/.i=(GoB h)*(j,width GoB h)} & i1=max Y holds (GoB h)*(i1,width
GoB h)`1>=p`1
proof
let p be Point of TOP-REAL 2,Y be non empty finite Subset of NAT;
assume
A1: p`2=N-bound L~h & p in L~h &
Y={j where j is Element of NAT:[j,width GoB h] in Indices GoB h &
ex i st i in dom h & h/.i=(GoB h)*(j,width GoB h)} & i1=max Y;
then consider i such that
A2: 1<=i and
A3: i+1<=len h and
A4: p in LSeg(h/.i,h/.(i+1)) by SPPOL_2:14;
A5: p`2=((GoB h)*(1,width GoB h))`2 by A1,Th40;
i<=i+1 by NAT_1:11;
then
A6: i<=len h by A3,XXREAL_0:2;
A7: 1<=i+1 by A2,XREAL_1:145;
now
per cases by SPPOL_1:19;
case
LSeg(h,i) is horizontal;
then LSeg(h/.i,h/.(i+1)) is horizontal by A2,A3,TOPREAL1:def 3;
then
A8: (h/.i)`2=(h/.(i+1))`2 by SPPOL_1:15;
then
A9: p`2=(h/.i)`2 by A4,GOBOARD7:6;
A10: p`2=(h/.(i+1))`2 by A4,A8,GOBOARD7:6;
now
per cases;
case
A11: (h/.i)`1>=(h/.(i+1))`1;
1 <= width GoB h by GOBOARD7:33;
then
A12: (GoB h)*(i1,width GoB h)`1>=(h/.i)`1 by A1,A5,A2,A6,A9,Th43;
(h/.i)`1>=p`1 by A4,A11,TOPREAL1:3;
hence thesis by A12,XXREAL_0:2;
end;
case
A13: (h/.i)`1<(h/.(i+1))`1;
1 <= width GoB h by GOBOARD7:33;
then
A14: (GoB h)*(i1,width GoB h)`1>=(h/.(i+1))`1 by A1,A5,A3,A7,A10,Th43;
(h/.(i+1))`1>=p`1 by A4,A13,TOPREAL1:3;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
LSeg(h,i) is vertical;
then LSeg(h/.i,h/.(i+1)) is vertical by A2,A3,TOPREAL1:def 3;
then
A15: (h/.i)`1=(h/.(i+1))`1 by SPPOL_1:16;
then
A16: p`1=(h/.i)`1 by A4,GOBOARD7:5;
A17: 1 <= len GoB h by GOBOARD7:32;
A18: p`1=(h/.(i+1))`1 by A4,A15,GOBOARD7:5;
now
per cases;
case
(h/.i)`2>=(h/.(i+1))`2;
then
A19: (h/.i)`2>=((GoB h)*(1,width GoB h))`2 by A5,A4,TOPREAL1:4;
(h/.i)`2<=((GoB h)*(1,width GoB h))`2 by A2,A6,A17,Th6;
then
A20: (h/.i)`2=((GoB h)*(1,width GoB h))`2 by A19,XXREAL_0:1;
1 <= width GoB h by GOBOARD7:33;
hence thesis by A1,A2,A6,A16,A20,Th43;
end;
case
(h/.i)`2 < (h/.(i+1))`2;
then
A21: (h/.(i+1))`2>=((GoB h)*(1,width GoB h))`2 by A5,A4,TOPREAL1:4;
(h/.(i+1))`2<=((GoB h)*(1,width GoB h))`2 by A3,A7,A17,Th6;
then
A22: (h/.(i+1))`2=((GoB h)*(1,width GoB h))`2 by A21,XXREAL_0:1;
1 <= width GoB h by GOBOARD7:33;
hence thesis by A1,A3,A7,A18,A22,Th43;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm9: len h >= 2 by GOBOARD7:34,XXREAL_0:2;
begin :: Coordinates of the special circular sequences bounding boxes
definition
let g be non constant standard special_circular_sequence;
func i_s_w g -> Nat means
:Def1:
[1,it] in Indices GoB g & (GoB g )*(1,it) = W-min L~g;
existence
proof
{q`2:q`1=W-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`2:q`1=W-bound(L~g) & q in L~g};
then ex q st X=q`2 & q`1=W-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`2:q`1=W-bound L~g & q in L~g} as Subset of REAL;
set s1=(GoB g)*(1,1)`2;
defpred P[Nat] means [1,$1] in Indices GoB g & ex i st i in dom
g & g/.i=(GoB g)*(1,$1);
set Y={j where j is Element of NAT:P[j]};
A1: Y c= Seg width GoB g
proof
let y be object;
assume y in Y;
then
ex j being Element of NAT
st y=j & [1,j] in Indices GoB g & ex i st i in dom g & g/.i = (
GoB g)*(1,j);
then [1,y] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A2: Y is Subset of NAT from DOMAIN_1:sch 7;
A3: 1 <= len GoB g by GOBOARD7:32;
then consider i,j such that
A4: i in dom g and
A5: [1,j] in Indices GoB g and
A6: g/.i = (GoB g)*(1,j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in Y by A4,A5,A6;
then reconsider Y as non empty finite Subset of NAT by A1,A2;
set i1 = min Y;
i1 in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A7: j=i1 and
A8: [1,j] in Indices GoB g and
A9: ex i being Nat st i in dom g & g/.i=(GoB g)*(1,j);
A10: i1 <= width (GoB g) by A7,A8,MATRIX_0:32;
A11: 1 <= len GoB g by A8,MATRIX_0:32;
1 <= i1 by A7,A8,MATRIX_0:32;
then
A12: (GoB g)*(1,i1)`1=(GoB g)*(1,1)`1 by A11,A10,GOBOARD5:2;
then
A13: (GoB g)*(1,i1)`1=W-bound L~g by Th37;
consider i such that
A14: i in dom g and
A15: g/.i=(GoB g)*(1,j) by A9;
A16: i<=len g by A14,FINSEQ_3:25;
A17: 1<=i by A14,FINSEQ_3:25;
A18: now
per cases by A16,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A17,TOPREAL1:21;
hence (GoB g)*(1,i1) in L~g by A7,A15,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(1,i1) in L~g by A7,A15,SPPOL_2:17;
end;
end;
(GoB g)*(1,i1)`1=W-bound(L~g) by A12,Th37;
then
A19: (GoB g)*(1,i1)`2 in {q`2:q`1=W-bound(L~g) & q in L~g} by A18;
for r being Real st r in B holds r>= (GoB g)*(1,i1)`2
proof
let r be Real;
assume r in B;
then ex q st r=q`2 & q`1=W-bound(L~g) & q in L~g;
hence thesis by Lm1;
end;
then
A20: lower_bound B >=(GoB g)*(1,i1)`2 by A19,SEQ_4:43;
s1 is LowerBound of B
proof
let r be ExtReal;
assume r in B;
then ex q st r=q`2 & q`1 = W-bound L~g & q in L~g;
hence thesis by A3,Th33;
end;
then B is bounded_below;
then lower_bound B <=(GoB g)*(1,i1)`2 by A19,SEQ_4:def 2;
then (GoB g)*(1,i1)`2=lower_bound B by A20,XXREAL_0:1
.= lower_bound (proj2 | W-most L~g) by Th13;
hence thesis by A7,A8,A13,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_n_w g -> Nat means
:Def2:
[1,it] in Indices GoB g & (GoB g )*(1,it) = W-max L~g;
existence
proof
{q`2:q`1=W-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`2:q`1=W-bound(L~g) & q in L~g};
then ex q st X=q`2 & q`1=W-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`2:q`1=W-bound L~g & q in L~g} as Subset of REAL;
set s1 = (GoB g)*(1,width GoB g)`2;
defpred P[Nat] means [1,$1] in Indices GoB g & ex i st i in dom
g & g/.i=(GoB g)*(1,$1);
set Y={j where j is Element of NAT:P[j]};
A21: Y c= Seg width GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [1,j] in Indices GoB g & ex i st i in dom g & g/.i =
(GoB g)*(1,j);
then [1,y] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A22: Y is Subset of NAT from DOMAIN_1:sch 7;
A23: 1 <= len GoB g by GOBOARD7:32;
then consider i,j such that
A24: i in dom g and
A25: [1,j] in Indices GoB g and
A26: g/.i = (GoB g)*(1,j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in Y by A24,A25,A26;
then reconsider Y as non empty finite Subset of NAT by A21,A22;
reconsider i1 = max Y as Nat by TARSKI:1;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A27: j=i1 and
A28: [1,j] in Indices GoB g and
A29: ex i being Nat st i in dom g & g/.i=(GoB g)*(1,j);
A30: i1 <= width GoB g by A27,A28,MATRIX_0:32;
A31: 1 <= len GoB g by A28,MATRIX_0:32;
1 <= i1 by A27,A28,MATRIX_0:32;
then
A32: (GoB g)*(1,i1)`1=(GoB g)*(1,1)`1 by A31,A30,GOBOARD5:2;
then
A33: (GoB g)*(1,i1)`1=W-bound L~g by Th37;
consider i such that
A34: i in dom g and
A35: g/.i=(GoB g)*(1,j) by A29;
A36: i<=len g by A34,FINSEQ_3:25;
A37: 1<=i by A34,FINSEQ_3:25;
A38: now
per cases by A36,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A37,TOPREAL1:21;
hence (GoB g)*(1,i1) in L~g by A27,A35,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(1,i1) in L~g by A27,A35,SPPOL_2:17;
end;
end;
(GoB g)*(1,i1)`1=W-bound L~g by A32,Th37;
then
A39: (GoB g)*(1,i1)`2 in {q`2:q`1=W-bound L~g & q in L~g} by A38;
for r being Real st r in B holds r <= (GoB g)*(1,i1)`2
proof
let r be Real;
assume r in B;
then ex q st r = q`2 & q`1 = W-bound L~g & q in L~g;
hence thesis by Lm2;
end;
then
A40: upper_bound B <= (GoB g)*(1,i1)`2 by A39,SEQ_4:45;
s1 is UpperBound of B
proof
let r be ExtReal;
assume r in B;
then ex q st r=q`2 & q`1 = W-bound L~g & q in L~g;
hence thesis by A23,Th34;
end;
then B is bounded_above;
then upper_bound B >= (GoB g)*(1,i1)`2 by A39,SEQ_4:def 1;
then (GoB g)*(1,i1)`2 = upper_bound B by A40,XXREAL_0:1
.= upper_bound (proj2 | W-most L~g) by Th13;
hence thesis by A27,A28,A33,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_s_e g -> Nat means
:Def3:
[len GoB g,it] in Indices GoB g & (GoB g)*(len GoB g,it) = E-min L~g;
existence
proof
{q`2:q`1=E-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`2:q`1=E-bound L~g & q in L~g};
then ex q st X=q`2 & q`1=E-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`2:q`1=E-bound L~g & q in L~g} as Subset of REAL;
set s1=(GoB g)*(len GoB g,1)`2;
defpred P[Nat] means [len GoB g,$1] in Indices GoB g & ex i st
i in dom g & g/.i=(GoB g)*(len GoB g,$1);
set Y={j where j is Element of NAT:P[j]};
A41: Y c= Seg width GoB g
proof
let y be object;
assume y in Y;
then
ex j being Element of NAT
st y=j & [len GoB g,j] in Indices GoB g & ex i st i in dom g &
g/.i = (GoB g)*(len GoB g,j);
then [len GoB g,y] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A42: Y is Subset of NAT from DOMAIN_1:sch 7;
A43: 1 <= len GoB g by GOBOARD7:32;
then consider i,j such that
A44: i in dom g and
A45: [len GoB g,j] in Indices GoB g and
A46: g/.i = (GoB g)*(len GoB g,j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in Y by A44,A45,A46;
then reconsider Y as non empty finite Subset of NAT by A41,A42;
set i1 = min Y;
i1 in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A47: j=i1 and
A48: [len GoB g,j] in Indices GoB g and
A49: ex i st i in dom g & g/.i=(GoB g)*(len GoB g,j);
A50: i1 <= width GoB g by A47,A48,MATRIX_0:32;
A51: 1 <= len GoB g by A48,MATRIX_0:32;
1 <= i1 by A47,A48,MATRIX_0:32;
then
A52: (GoB g)*(len GoB g,i1)`1=(GoB g)*(len GoB g,1)`1 by A51,A50,GOBOARD5:2;
then
A53: (GoB g)*(len GoB g,i1)`1=E-bound L~g by Th39;
consider i such that
A54: i in dom g and
A55: g/.i=(GoB g)*(len GoB g,j) by A49;
A56: i<=len g by A54,FINSEQ_3:25;
A57: 1<=i by A54,FINSEQ_3:25;
A58: now
per cases by A56,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A57,TOPREAL1:21;
hence (GoB g)*(len GoB g,i1) in L~g by A47,A55,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(len GoB g,i1) in L~g by A47,A55,SPPOL_2:17;
end;
end;
(GoB g)*(len GoB g,i1)`1=E-bound L~g by A52,Th39;
then
A59: (GoB g)*(len GoB g,i1)`2 in {q`2:q`1=E-bound L~g & q in L~g} by A58;
for r be Real st r in B holds r>= (GoB g)*(len GoB g,i1)`2
proof
let r be Real;
assume r in B;
then ex q st r=q`2 & q`1=E-bound L~g & q in L~g;
hence thesis by Lm3;
end;
then
A60: lower_bound B >= (GoB g)*(len GoB g,i1)`2 by A59,SEQ_4:43;
s1 is LowerBound of B
proof
let r be ExtReal;
assume r in B;
then ex q st r=q`2 & q`1 = E-bound L~g & q in L~g;
hence thesis by A43,Th33;
end;
then B is bounded_below;
then lower_bound B <=(GoB g)*(len GoB g,i1)`2 by A59,SEQ_4:def 2;
then (GoB g)*(len GoB g,i1)`2=lower_bound B by A60,XXREAL_0:1
.= lower_bound (proj2 | E-most L~g) by Th14;
hence thesis by A47,A48,A53,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_n_e g -> Nat means
:Def4:
[len GoB g,it] in Indices GoB g & (GoB g)*(len GoB g,it) = E-max L~g;
existence
proof
{q`2:q`1=E-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`2:q`1=E-bound(L~g) & q in L~g};
then ex q st X=q`2 & q`1=E-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`2:q`1=E-bound L~g & q in L~g} as Subset of REAL;
defpred P[Nat] means [len GoB g,$1] in Indices GoB g & ex i st
i in dom g & g/.i=(GoB g)*(len GoB g,$1);
set Y={j where j is Element of NAT:P[j]};
A61: Y c= Seg width GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [len GoB g,j] in Indices GoB g & ex i st i in dom g
& g/.i = (GoB g)*(len GoB g,j);
then [len GoB g,y] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A62: Y is Subset of NAT from DOMAIN_1:sch 7;
0 <> len GoB g by MATRIX_0:def 10;
then 1 <= len GoB g by NAT_1:14;
then consider i,j such that
A63: i in dom g and
A64: [len GoB g,j] in Indices GoB g and
A65: g/.i = (GoB g)*(len GoB g,j) by Th7;
j in NAT by ORDINAL1:def 12;
then j in Y by A63,A64,A65;
then reconsider Y as non empty finite Subset of NAT by A61,A62;
reconsider i1 = max Y as Nat by TARSKI:1;
set s1 = (GoB g)*(len GoB g,width GoB g)`2;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A66: j=i1 and
A67: [len GoB g,j] in Indices GoB g and
A68: ex i st i in dom g & g/.i=(GoB g)*(len GoB g,j);
A69: i1 <= width GoB g by A66,A67,MATRIX_0:32;
A70: 1 <= len GoB g by A67,MATRIX_0:32;
1 <= i1 by A66,A67,MATRIX_0:32;
then
A71: (GoB g)*(len GoB g,i1)`1=(GoB g)*(len GoB g,1)`1 by A70,A69,GOBOARD5:2;
then
A72: (GoB g)*(len GoB g,i1)`1 = E-bound L~g by Th39;
consider i such that
A73: i in dom g and
A74: g/.i=(GoB g)*(len GoB g,j) by A68;
A75: i<=len g by A73,FINSEQ_3:25;
A76: 1<=i by A73,FINSEQ_3:25;
A77: now
per cases by A75,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A76,TOPREAL1:21;
hence (GoB g)*(len GoB g,i1) in L~g by A66,A74,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(len GoB g,i1) in L~g by A66,A74,SPPOL_2:17;
end;
end;
(GoB g)*(len GoB g,i1)`1=E-bound L~g by A71,Th39;
then
A78: (GoB g)*(len GoB g,i1)`2 in {q`2:q`1=E-bound L~g & q in L~g} by A77;
for r being Real st r in B holds r <= (GoB g)*(len GoB g,i1) `2
proof
let r be Real;
assume r in B;
then ex q st r = q`2 & q`1 = E-bound L~g & q in L~g;
hence thesis by Lm4;
end;
then
A79: upper_bound B <= (GoB g)*(len GoB g,i1)`2 by A78,SEQ_4:45;
s1 is UpperBound of B
proof
let r be ExtReal;
assume r in B;
then
A80: ex q st r=q`2 & q`1 = E-bound L~g & q in L~g;
1 <= len GoB g by GOBOARD7:32;
hence thesis by A80,Th34;
end;
then B is bounded_above;
then upper_bound B >= (GoB g)*(len GoB g,i1)`2 by A78,SEQ_4:def 1;
then (GoB g)*(len GoB g,i1)`2 = upper_bound B by A79,XXREAL_0:1
.= upper_bound (proj2 | E-most L~g) by Th14;
hence thesis by A66,A67,A72,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_w_s g -> Nat means
:Def5:
[it, 1] in Indices GoB g & (GoB g)*(it,1) = S-min L~g;
existence
proof
{q`1:q`2=S-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`1:q`2=S-bound L~g & q in L~g};
then ex q st X=q`1 & q`2=S-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`1:q`2=S-bound L~g & q in L~g} as Subset of REAL;
set s1=(GoB g)*(1,1)`1;
defpred P[Nat] means [$1,1] in Indices GoB g & ex i st i in dom
g & g/.i=(GoB g)*($1,1);
set Y={j where j is Element of NAT:P[j]};
A81: Y c= dom GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [j,1] in Indices GoB g & ex i st i in dom g & g/.i =
(GoB g)*(j,1);
then [y,1] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A82: Y is Subset of NAT from DOMAIN_1:sch 7;
A83: 1 <= width GoB g by GOBOARD7:33;
then consider i,j such that
A84: i in dom g and
A85: [j,1] in Indices GoB g and
A86: g/.i = (GoB g)*(j,1) by Th8;
j in NAT by ORDINAL1:def 12;
then j in Y by A84,A85,A86;
then reconsider Y as non empty finite Subset of NAT by A81,A82;
set i1 = min Y;
i1 in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A87: j=i1 and
A88: [j,1] in Indices GoB g and
A89: ex i st i in dom g & g/.i=(GoB g)*(j,1);
A90: i1 <= len GoB g by A87,A88,MATRIX_0:32;
A91: 1 <= width GoB g by A88,MATRIX_0:32;
1 <= i1 by A87,A88,MATRIX_0:32;
then
A92: (GoB g)*(i1,1)`2=(GoB g)*(1,1)`2 by A90,A91,GOBOARD5:1;
then
A93: (GoB g)*(i1,1)`2=S-bound L~g by Th38;
consider i such that
A94: i in dom g and
A95: g/.i=(GoB g)*(j,1) by A89;
A96: i<=len g by A94,FINSEQ_3:25;
A97: 1<=i by A94,FINSEQ_3:25;
A98: now
per cases by A96,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A97,TOPREAL1:21;
hence (GoB g)*(i1,1) in L~g by A87,A95,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(i1,1) in L~g by A87,A95,SPPOL_2:17;
end;
end;
(GoB g)*(i1,1)`2=S-bound L~g by A92,Th38;
then
A99: (GoB g)*(i1,1)`1 in {q`1:q`2=S-bound L~g & q in L~g} by A98;
for r being Real st r in B holds r>= (GoB g)*(i1,1)`1
proof
let r be Real;
assume r in B;
then ex q st r=q`1 & q`2=S-bound L~g & q in L~g;
hence thesis by Lm5;
end;
then
A100: lower_bound B >=(GoB g)*(i1,1)`1 by A99,SEQ_4:43;
s1 is LowerBound of B
proof
let r be ExtReal;
assume r in B;
then ex q st r=q`1 & q`2 = S-bound L~g & q in L~g;
hence thesis by A83,Th31;
end;
then B is bounded_below;
then lower_bound B <=(GoB g)*(i1,1)`1 by A99,SEQ_4:def 2;
then (GoB g)*(i1,1)`1=lower_bound B by A100,XXREAL_0:1
.= lower_bound (proj1 | S-most L~g) by Th16;
hence thesis by A87,A88,A93,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_e_s g -> Nat means
:Def6:
[it, 1] in Indices GoB g & (GoB g)*(it,1) = S-max L~g;
existence
proof
{q`1:q`2=S-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`1:q`2=S-bound L~g & q in L~g};
then ex q st X=q`1 & q`2=S-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`1:q`2 = S-bound L~g & q in L~g} as Subset of REAL;
defpred P[Nat] means [$1,1] in Indices GoB g & ex i st i in dom
g & g/.i=(GoB g)*($1,1);
set Y={j where j is Element of NAT:P[j]};
A101: Y c= dom GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [j,1] in Indices GoB g & ex i st i in dom g & g/.i =
(GoB g)*(j,1);
then [y,1] in [: dom GoB g, Seg width GoB g :] by MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A102: Y is Subset of NAT from DOMAIN_1:sch 7;
1 <= width GoB g by GOBOARD7:33;
then consider i,j such that
A103: i in dom g and
A104: [j,1] in Indices GoB g and
A105: g/.i = (GoB g)*(j,1) by Th8;
j in NAT by ORDINAL1:def 12;
then j in Y by A103,A104,A105;
then reconsider Y as non empty finite Subset of NAT by A101,A102;
reconsider i1 = max Y as Nat by TARSKI:1;
set s1 = (GoB g)*(len GoB g,1)`1;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A106: j=i1 and
A107: [j,1] in Indices GoB g and
A108: ex i st i in dom g & g/.i=(GoB g)*(j,1);
A109: i1 <= len GoB g by A106,A107,MATRIX_0:32;
A110: 1 <= width GoB g by A107,MATRIX_0:32;
1 <= i1 by A106,A107,MATRIX_0:32;
then
A111: (GoB g)*(i1,1)`2=(GoB g)*(1,1)`2 by A109,A110,GOBOARD5:1;
then
A112: (GoB g)*(i1,1)`2 = S-bound L~g by Th38;
consider i such that
A113: i in dom g and
A114: g/.i=(GoB g)*(j,1) by A108;
A115: i<=len g by A113,FINSEQ_3:25;
A116: 1<=i by A113,FINSEQ_3:25;
A117: now
per cases by A115,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A116,TOPREAL1:21;
hence (GoB g)*(i1,1) in L~g by A106,A114,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(i1,1) in L~g by A106,A114,SPPOL_2:17;
end;
end;
(GoB g)*(i1,1)`2=S-bound L~g by A111,Th38;
then
A118: (GoB g)*(i1,1)`1 in {q`1:q`2=S-bound L~g & q in L~g} by A117;
for r being Real st r in B holds r <= (GoB g)*(i1,1)`1
proof
let r be Real;
assume r in B;
then ex q st r = q`1 & q`2 = S-bound L~g & q in L~g;
hence thesis by Lm7;
end;
then
A119: upper_bound B <= (GoB g)*(i1,1)`1 by A118,SEQ_4:45;
s1 is UpperBound of B
proof
let r be ExtReal;
assume r in B;
then
A120: ex q st r=q`1 & q`2 = S-bound L~g & q in L~g;
1 <= width GoB g by GOBOARD7:33;
hence thesis by A120,Th32;
end;
then B is bounded_above;
then upper_bound B >= (GoB g)*(i1,1)`1 by A118,SEQ_4:def 1;
then (GoB g)*(i1,1)`1 = upper_bound B by A119,XXREAL_0:1
.= upper_bound (proj1 | S-most L~g) by Th16;
hence thesis by A106,A107,A112,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_w_n g -> Nat means
:Def7:
[it, width GoB g] in Indices GoB g & (GoB g)*(it,width GoB g) = N-min L~g;
existence
proof
{q`1:q`2=N-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`1:q`2=N-bound L~g & q in L~g};
then ex q st X=q`1 & q`2=N-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`1:q`2=N-bound L~g & q in L~g} as Subset of REAL;
defpred P[Nat] means [$1,width GoB g] in Indices GoB g & ex i
st i in dom g & g/.i=(GoB g)*($1,width GoB g);
set Y={j where j is Element of NAT:P[j]};
A121: Y c= dom GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [j,width GoB g] in Indices GoB g & ex i st i in dom
g & g/.i = (GoB g)*(j,width GoB g);
then [y,width GoB g] in [: dom GoB g, Seg width GoB g :] by
MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A122: Y is Subset of NAT from DOMAIN_1:sch 7;
1 <= width GoB g by GOBOARD7:33;
then consider i,j such that
A123: i in dom g and
A124: [j,width GoB g] in Indices GoB g and
A125: g/.i = (GoB g)*(j,width GoB g) by Th8;
j in NAT by ORDINAL1:def 12;
then j in Y by A123,A124,A125;
then reconsider Y as non empty finite Subset of NAT by A121,A122;
set i1 = min Y;
set s1=(GoB g)*(1,width GoB g)`1;
i1 in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A126: j=i1 and
A127: [j,width GoB g] in Indices GoB g and
A128: ex i being Nat st i in dom g & g/.i=(GoB g)*(j,width GoB g);
A129: i1 <= len GoB g by A126,A127,MATRIX_0:32;
A130: 1 <= width GoB g by A127,MATRIX_0:32;
1 <= i1 by A126,A127,MATRIX_0:32;
then
A131: (GoB g)*(i1,width GoB g)`2=(GoB g)*(1,width GoB g)`2 by A129,A130,
GOBOARD5:1;
then
A132: (GoB g)*(i1,width GoB g)`2=N-bound L~g by Th40;
consider i such that
A133: i in dom g and
A134: g/.i=(GoB g)*(j,width GoB g) by A128;
A135: i<=len g by A133,FINSEQ_3:25;
A136: 1<=i by A133,FINSEQ_3:25;
A137: now
per cases by A135,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A136,TOPREAL1:21;
hence (GoB g)*(i1,width GoB g) in L~g by A126,A134,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(i1,width GoB g) in L~g by A126,A134,SPPOL_2:17;
end;
end;
(GoB g)*(i1,width GoB g)`2=N-bound L~g by A131,Th40;
then
A138: (GoB g)*(i1,width GoB g)`1 in {q`1:q`2=N-bound L~g & q in L~g} by A137;
for r being Real st r in B holds r>= (GoB g)*(i1,width GoB g) `1
proof
let r be Real;
assume r in B;
then ex q st r=q`1 & q`2=N-bound L~g & q in L~g;
hence thesis by Lm6;
end;
then
A139: lower_bound B >=(GoB g)*(i1,width GoB g)`1 by A138,SEQ_4:43;
s1 is LowerBound of B
proof
let r be ExtReal;
assume r in B;
then
A140: ex q1 be Point of TOP-REAL 2 st r=q1`1 & q1`2 = N-bound L~g & q1 in L~g;
1 <= width GoB g by GOBOARD7:33;
hence thesis by A140,Th31;
end;
then B is bounded_below;
then lower_bound B <= (GoB g)*(i1,width GoB g)`1 by A138,SEQ_4:def 2;
then (GoB g)*(i1,width GoB g)`1=lower_bound B by A139,XXREAL_0:1
.= lower_bound (proj1 | N-most L~g) by Th15;
hence thesis by A126,A127,A132,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
func i_e_n g -> Nat means
:Def8:
[it, width GoB g] in Indices GoB g & (GoB g)*(it,width GoB g) = N-max L~g;
existence
proof
{q`1:q`2=N-bound L~g & q in L~g} c= REAL
proof
let X be object;
assume X in {q`1:q`2=N-bound L~g & q in L~g};
then ex q st X=q`1 & q`2=N-bound L~g & q in L~g;
hence thesis by XREAL_0:def 1;
end;
then reconsider B={q`1:q`2 = N-bound L~g & q in L~g} as Subset of REAL;
defpred P[Nat] means [$1,width GoB g] in Indices GoB g & ex i
st i in dom g & g/.i=(GoB g)*($1,width GoB g);
set Y={j where j is Element of NAT:P[j]};
A141: Y c= dom GoB g
proof
let y be object;
assume y in Y;
then ex j being Element of NAT
st y=j & [j,width GoB g] in Indices GoB g & ex i st i in dom
g & g/.i = (GoB g)*(j,width GoB g);
then [y,width GoB g] in [: dom GoB g, Seg width GoB g :] by
MATRIX_0:def 4;
hence thesis by ZFMISC_1:87;
end;
A142: Y is Subset of NAT from DOMAIN_1:sch 7;
1 <= width GoB g by GOBOARD7:33;
then consider i,j such that
A143: i in dom g and
A144: [j,width GoB g] in Indices GoB g and
A145: g/.i = (GoB g)*(j,width GoB g) by Th8;
j in NAT by ORDINAL1:def 12;
then j in Y by A143,A144,A145;
then reconsider Y as non empty finite Subset of NAT by A141,A142;
reconsider i1 = max Y as Nat by TARSKI:1;
set s1 = (GoB g)*(len GoB g,width GoB g)`1;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A146: j=i1 and
A147: [j,width GoB g] in Indices GoB g and
A148: ex i being Nat st i in dom g & g/.i=(GoB g)*(j,width GoB g);
A149: i1 <= len GoB g by A146,A147,MATRIX_0:32;
A150: 1 <= width GoB g by A147,MATRIX_0:32;
1 <= i1 by A146,A147,MATRIX_0:32;
then
A151: (GoB g)*(i1,width GoB g)`2=(GoB g)*(1,width GoB g)`2 by A149,A150,
GOBOARD5:1;
then
A152: (GoB g)*(i1,width GoB g)`2 = N-bound L~g by Th40;
consider i such that
A153: i in dom g and
A154: g/.i=(GoB g)*(j,width GoB g) by A148;
A155: i<=len g by A153,FINSEQ_3:25;
A156: 1<=i by A153,FINSEQ_3:25;
A157: now
per cases by A155,XXREAL_0:1;
case
i<len g;
then i+1<=len g by NAT_1:13;
then g/.i in LSeg(g,i) by A156,TOPREAL1:21;
hence (GoB g)*(i1,width GoB g) in L~g by A146,A154,SPPOL_2:17;
end;
case
i=len g;
then g/.i in LSeg(g,i-'1) by Lm9,Th1;
hence (GoB g)*(i1,width GoB g) in L~g by A146,A154,SPPOL_2:17;
end;
end;
(GoB g)*(i1,width GoB g)`2=N-bound L~g by A151,Th40;
then
A158: (GoB g)*(i1,width GoB g)`1 in {q`1:q`2=N-bound L~g & q in L~g } by A157;
for r being Real st r in B holds r <= (GoB g)*(i1,width GoB g )`1
proof
let r be Real;
assume r in B;
then ex q st r = q`1 & q`2 = N-bound L~g & q in L~g;
hence thesis by Lm8;
end;
then
A159: upper_bound B <= (GoB g)*(i1,width GoB g)`1 by A158,SEQ_4:45;
s1 is UpperBound of B
proof
let r be ExtReal;
assume r in B;
then
A160: ex q st r=q`1 & q`2 = N-bound L~g & q in L~g;
1 <= width GoB g by GOBOARD7:33;
hence thesis by A160,Th32;
end;
then B is bounded_above;
then upper_bound B >= (GoB g)*(i1,width GoB g)`1 by A158,SEQ_4:def 1;
then (GoB g)*(i1,width GoB g)`1 = upper_bound B by A159,XXREAL_0:1
.= upper_bound (proj1 | N-most L~g) by Th15;
hence thesis by A146,A147,A152,EUCLID:53;
end;
uniqueness by GOBOARD1:5;
end;
theorem
1 <= i_w_n h & i_w_n h <= len GoB h & 1 <= i_e_n h & i_e_n h <= len
GoB h & 1 <= i_w_s h & i_w_s h <= len GoB h & 1 <= i_e_s h & i_e_s h <= len GoB
h
proof
A1: [i_e_n h, width GoB h] in Indices GoB h by Def8;
A2: [i_w_s h, 1] in Indices GoB h by Def5;
A3: [i_e_s h, 1] in Indices GoB h by Def6;
[i_w_n h, width GoB h] in Indices GoB h by Def7;
hence thesis by A1,A2,A3,MATRIX_0:32;
end;
theorem
1 <= i_n_e h & i_n_e h <= width GoB h & 1 <= i_s_e h & i_s_e h <=
width GoB h & 1 <= i_n_w h & i_n_w h <= width GoB h & 1 <= i_s_w h & i_s_w h <=
width GoB h
proof
A1: [len GoB h, i_s_e h] in Indices GoB h by Def3;
A2: [1, i_n_w h] in Indices GoB h by Def2;
A3: [1, i_s_w h] in Indices GoB h by Def1;
[len GoB h, i_n_e h] in Indices GoB h by Def4;
hence thesis by A1,A2,A3,MATRIX_0:32;
end;
Lm10: for i1, i2 be Nat st 1 <= i1 & i1+1<=len h & 1<=i2 & i2+1<=
len h & h.i1=h.i2 holds i1 = i2
proof
let i1, i2 be Nat;
assume that
A1: 1 <= i1 and
A2: i1+1 <= len h;
A3: i1 < len h by A2,NAT_1:13;
assume that
A4: 1 <= i2 and
A5: i2+1 <= len h and
A6: h.i1 = h.i2;
A7: i2 < len h by A5,NAT_1:13;
then
A8: i2 in dom h by A4,FINSEQ_3:25;
assume
A9: i1 <> i2;
A10: now
per cases by A9,XXREAL_0:1;
suppose
i1 < i2;
hence h/.i1 <> h/.i2 by A1,A7,GOBOARD7:36;
end;
suppose
i2 < i1;
hence h/.i1 <> h/.i2 by A4,A3,GOBOARD7:36;
end;
end;
i1 in dom h by A1,A3,FINSEQ_3:25;
then h/.i1 = h.i2 by A6,PARTFUN1:def 6
.= h/.i2 by A8,PARTFUN1:def 6;
hence thesis by A10;
end;
definition
let g be non constant standard special_circular_sequence;
func n_s_w g -> Nat means
:Def9:
1 <= it & it+1 <= len g & g.it = W-min L~g;
existence
proof
W-min L~g in rng g by SPRECT_2:43;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_n_w g -> Nat means
:Def10:
1 <= it & it+1 <= len g & g.it = W-max L~g;
existence
proof
W-max L~g in rng g by SPRECT_2:44;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_s_e g -> Nat means
:Def11:
1 <= it & it+1 <= len g & g.it = E-min L~g;
existence
proof
E-min L~g in rng g by SPRECT_2:45;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_n_e g -> Nat means
:Def12:
1 <= it & it+1 <= len g & g.it = E-max L~g;
existence
proof
E-max L~g in rng g by SPRECT_2:46;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_w_s g -> Nat means
:Def13:
1 <= it & it+1 <= len g & g.it = S-min L~g;
existence
proof
S-min L~g in rng g by SPRECT_2:41;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_e_s g -> Nat means
:Def14:
1 <= it & it+1 <= len g & g.it = S-max L~g;
existence
proof
S-max L~g in rng g by SPRECT_2:42;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_w_n g -> Nat means
:Def15:
1 <= it & it+1 <= len g & g.it = N-min L~g;
existence
proof
N-min L~g in rng g by SPRECT_2:39;
hence thesis by Th3;
end;
uniqueness by Lm10;
func n_e_n g -> Nat means
:Def16:
1 <= it & it+1 <= len g & g.it = N-max L~g;
existence
proof
N-max L~g in rng g by SPRECT_2:40;
hence thesis by Th3;
end;
uniqueness by Lm10;
end;
theorem
n_w_n h <> n_w_s h
proof
set i1 = n_w_n h, i2 = n_w_s h;
A1: i1 <= i1 + 1 by NAT_1:11;
A2: 1 <= i1 by Def15;
i1+1 <= len h by Def15;
then i1 <= len h by A1,XXREAL_0:2;
then i1 in dom h by A2,FINSEQ_3:25;
then
A3: h.i1 = h/.i1 by PARTFUN1:def 6;
A4: i2 <= i2 + 1 by NAT_1:11;
A5: h.i2 = S-min L~h by Def13;
A6: 1 <= i2 by Def13;
i2+1 <= len h by Def13;
then i2 <= len h by A4,XXREAL_0:2;
then i2 in dom h by A6,FINSEQ_3:25;
then
A7: h.i2 = h/.i2 by PARTFUN1:def 6;
A8: h.i1 = N-min L~h by Def15;
thus i1 <> i2
proof
assume i1 = i2;
then
A9: N-bound(L~h) = (h/.i2)`2 by A8,A3,EUCLID:52
.= S-bound(L~h) by A5,A7,EUCLID:52;
A10: 1 <= len h by GOBOARD7:34,XXREAL_0:2;
then
A11: (h/.1)`2 >= S-bound (L~h) by Th11;
consider ii be Nat such that
A12: ii in dom h and
A13: (h/.ii)`2 <> (h/.1)`2 by GOBOARD7:31;
A14: ii <= len h by A12,FINSEQ_3:25;
A15: 1 <= ii by A12,FINSEQ_3:25;
then
A16: (h/.ii)`2 <= N-bound (L~h) by A14,Th11;
A17: (h/.ii)`2 >= S-bound L~h by A15,A14,Th11;
(h/.1)`2 <= N-bound (L~h) by A10,Th11;
then (h/.1)`2 = N-bound (L~h) by A9,A11,XXREAL_0:1;
hence thesis by A9,A13,A16,A17,XXREAL_0:1;
end;
end;
theorem
n_s_w h <> n_s_e h
proof
set i1 = n_s_w h, i2 = n_s_e h;
A1: i1 <= i1 + 1 by NAT_1:11;
A2: 1 <= i1 by Def9;
i1+1 <= len h by Def9;
then i1 <= len h by A1,XXREAL_0:2;
then i1 in dom h by A2,FINSEQ_3:25;
then
A3: h.i1 = h/.i1 by PARTFUN1:def 6;
A4: i2 <= i2 + 1 by NAT_1:11;
A5: h.i2 = E-min L~h by Def11;
A6: 1 <= i2 by Def11;
i2+1 <= len h by Def11;
then i2 <= len h by A4,XXREAL_0:2;
then i2 in dom h by A6,FINSEQ_3:25;
then
A7: h.i2 = h/.i2 by PARTFUN1:def 6;
A8: h.i1 = W-min L~h by Def9;
thus i1 <> i2
proof
assume i1 = i2;
then
A9: W-bound L~h = (h/.i2)`1 by A8,A3,EUCLID:52
.= E-bound L~h by A5,A7,EUCLID:52;
A10: 1 <= len h by GOBOARD7:34,XXREAL_0:2;
then
A11: (h/.1)`1 >= W-bound L~h by Th12;
consider ii be Nat such that
A12: ii in dom h and
A13: (h/.ii)`1 <> (h/.1)`1 by GOBOARD7:30;
A14: ii <= len h by A12,FINSEQ_3:25;
A15: 1 <= ii by A12,FINSEQ_3:25;
then
A16: (h/.ii)`1 <= E-bound L~h by A14,Th12;
A17: (h/.ii)`1 >= W-bound L~h by A15,A14,Th12;
(h/.1)`1 <= E-bound L~h by A10,Th12;
then (h/.1)`1 = W-bound L~h by A9,A11,XXREAL_0:1;
hence thesis by A9,A13,A16,A17,XXREAL_0:1;
end;
end;
theorem
n_e_n h <> n_e_s h
proof
set i1 = n_e_n h, i2 = n_e_s h;
A1: i1 <= i1 + 1 by NAT_1:11;
A2: 1 <= i1 by Def16;
i1+1 <= len h by Def16;
then i1 <= len h by A1,XXREAL_0:2;
then i1 in dom h by A2,FINSEQ_3:25;
then
A3: h.i1 = h/.i1 by PARTFUN1:def 6;
A4: i2 <= i2 + 1 by NAT_1:11;
A5: h.i2 = S-max L~h by Def14;
A6: 1 <= i2 by Def14;
i2+1 <= len h by Def14;
then i2 <= len h by A4,XXREAL_0:2;
then i2 in dom h by A6,FINSEQ_3:25;
then
A7: h.i2 = h/.i2 by PARTFUN1:def 6;
A8: h.i1 = N-max L~h by Def16;
thus i1 <> i2
proof
assume i1 = i2;
then
A9: N-bound(L~h) = (h/.i2)`2 by A8,A3,EUCLID:52
.= S-bound(L~h) by A5,A7,EUCLID:52;
A10: 1 <= len h by GOBOARD7:34,XXREAL_0:2;
then
A11: (h/.1)`2 >= S-bound (L~h) by Th11;
consider ii be Nat such that
A12: ii in dom h and
A13: (h/.ii)`2 <> (h/.1)`2 by GOBOARD7:31;
A14: ii <= len h by A12,FINSEQ_3:25;
A15: 1 <= ii by A12,FINSEQ_3:25;
then
A16: (h/.ii)`2 <= N-bound (L~h) by A14,Th11;
A17: (h/.ii)`2 >= S-bound L~h by A15,A14,Th11;
(h/.1)`2 <= N-bound (L~h) by A10,Th11;
then (h/.1)`2 = N-bound (L~h) by A9,A11,XXREAL_0:1;
hence thesis by A9,A13,A16,A17,XXREAL_0:1;
end;
end;
theorem
n_n_w h <> n_n_e h
proof
set i1 = n_n_w h, i2 = n_n_e h;
A1: i1 <= i1 + 1 by NAT_1:11;
A2: 1 <= i1 by Def10;
i1+1 <= len h by Def10;
then i1 <= len h by A1,XXREAL_0:2;
then i1 in dom h by A2,FINSEQ_3:25;
then
A3: h.i1 = h/.i1 by PARTFUN1:def 6;
A4: i2 <= i2 + 1 by NAT_1:11;
A5: h.i2 = E-max L~h by Def12;
A6: 1 <= i2 by Def12;
i2+1 <= len h by Def12;
then i2 <= len h by A4,XXREAL_0:2;
then i2 in dom h by A6,FINSEQ_3:25;
then
A7: h.i2 = h/.i2 by PARTFUN1:def 6;
A8: h.i1 = W-max L~h by Def10;
thus i1 <> i2
proof
assume i1 = i2;
then
A9: W-bound L~h = (h/.i2)`1 by A8,A3,EUCLID:52
.= E-bound L~h by A5,A7,EUCLID:52;
A10: 1 <= len h by GOBOARD7:34,XXREAL_0:2;
then
A11: (h/.1)`1 >= W-bound L~h by Th12;
consider ii be Nat such that
A12: ii in dom h and
A13: (h/.ii)`1 <> (h/.1)`1 by GOBOARD7:30;
A14: ii <= len h by A12,FINSEQ_3:25;
A15: 1 <= ii by A12,FINSEQ_3:25;
then
A16: (h/.ii)`1 <= E-bound L~h by A14,Th12;
A17: (h/.ii)`1 >= W-bound L~h by A15,A14,Th12;
(h/.1)`1 <= E-bound L~h by A10,Th12;
then (h/.1)`1 = W-bound L~h by A9,A11,XXREAL_0:1;
hence thesis by A9,A13,A16,A17,XXREAL_0:1;
end;
end;