:: Some Remarks on Finite Sequences on Go-boards
:: by Adam Naumowicz
::
:: Received August 29, 2001
:: Copyright (c) 2001-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, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD1,
RLTOPSP1, RELAT_1, XBOOLE_0, TOPREAL1, MATRIX_1, XXREAL_0, MCART_1,
RCOMP_1, PSCOMP_1, PRE_TOPC, TREES_1, TARSKI, ARYTM_3, PARTFUN1,
COMPLEX1, ARYTM_1, CARD_1, SPPOL_1, JORDAN1E, JORDAN9, FINSEQ_6,
FINSEQ_5, FINSEQ_4, JORDAN6, TOPREAL2, RELAT_2, JORDAN8, ORDINAL4,
FUNCT_1, NAT_1, RFINSEQ, JORDAN1A, SEQ_4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
NAT_1, NAT_D, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4,
FINSEQ_5, FINSEQ_6, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1,
CONNSP_1, RFINSEQ, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1,
SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8, JORDAN9, JORDAN1A, JORDAN1E;
constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, JORDAN5C,
JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4,
RELSET_1, PSCOMP_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_6,
STRUCT_0, SPPOL_2, SPRECT_1, SPRECT_2, TOPREAL6, JORDAN8, JORDAN1A,
JORDAN1E, FUNCT_1, EUCLID, PSCOMP_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI;
equalities STRUCT_0, PSCOMP_1;
theorems JORDAN8, NAT_1, GOBOARD7, GOBOARD5, SPRECT_3, ABSVALUE, GOBOARD1,
JORDAN6, PSCOMP_1, TARSKI, TOPREAL3, SPRECT_2, FINSEQ_6, RELAT_1,
FINSEQ_5, TOPREAL1, PRE_TOPC, JORDAN5B, FINSEQ_1, JORDAN1E, JORDAN1A,
REVROT_1, JORDAN9, JORDAN1B, FINSEQ_3, UNIFORM1, FINSEQ_4, JORDAN1D,
SPRECT_5, RFINSEQ, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0,
EUCLID, PARTFUN1, MATRIX_0, XREAL_0;
begin
reserve i,j,k,m,n for Nat,
f for FinSequence of the carrier of TOP-REAL 2,
G for Go-board;
theorem Th1:
f is_sequence_on G & LSeg(G*(i,j),G*(i,k)) meets L~f & [i,j] in
Indices G & [i,k] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(i,
n)`2 = lower_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f))
proof
set X = LSeg(G*(i,j),G*(i,k)) /\ L~f;
assume that
A1: f is_sequence_on G and
A2: LSeg(G*(i,j),G*(i,k)) meets L~f and
A3: [i,j] in Indices G and
A4: [i,k] in Indices G and
A5: j <= k;
A6: 1 <= i & i <= len G by A3,MATRIX_0:32;
ex x being object st x in LSeg(G*(i,j),G*(i,k)) & x in L~f by A2,XBOOLE_0:3;
then reconsider X1=X as non empty compact Subset of TOP-REAL 2
by XBOOLE_0:def 4;
consider p being object such that
A7: p in S-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A7;
A8: p in X by A7,XBOOLE_0:def 4;
then
A9: p in LSeg(G*(i,j),G*(i,k)) by XBOOLE_0:def 4;
proj2.:X = (proj2|X).:X by RELAT_1:129;
then
A10: lower_bound(proj2.:X) = lower_bound((proj2|X).: [#]((TOP-REAL 2)|X))
by PRE_TOPC:def 5
.= S-bound X;
A11: 1 <= k by A4,MATRIX_0:32;
A12: p`2 = (S-min X)`2 by A7,PSCOMP_1:55
.= lower_bound(proj2.:X) by A10,EUCLID:52;
A13: 1 <= i & i <= len G by A3,MATRIX_0:32;
A14: 1 <= j by A3,MATRIX_0:32;
A15: k <= width G by A4,MATRIX_0:32;
then
A16: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A14,SPRECT_3:12;
then
A17: G*(i,j)`2 <= p`2 by A9,TOPREAL1:4;
A18: p`2 <= G*(i,k)`2 by A9,A16,TOPREAL1:4;
A19: j <= width G by A3,MATRIX_0:32;
then
A20: G*(i,j)`1 = G*(i,1)`1 by A6,A14,GOBOARD5:2
.= G*(i,k)`1 by A13,A11,A15,GOBOARD5:2;
p in L~f by A8,XBOOLE_0:def 4;
then p in union { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TOPREAL1:def 4;
then consider Y being set such that
A21: p in Y and
A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TARSKI:def 4;
consider i1 being Nat such that
A23: Y = LSeg(f,i1) and
A24: 1 <= i1 and
A25: i1+1 <= len f by A22;
A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3;
1 < i1+1 by A24,NAT_1:13;
then i1+1 in Seg len f by A25,FINSEQ_1:1;
then
A27: i1+1 in dom f by FINSEQ_1:def 3;
then consider io,jo being Nat such that
A28: [io,jo] in Indices G and
A29: f/.(i1+1) = G*(io,jo) by A1,GOBOARD1:def 9;
A30: 1 <= io & io <= len G by A28,MATRIX_0:32;
A31: 1 <= jo by A28,MATRIX_0:32;
i1 <= len f by A25,NAT_1:13;
then i1 in Seg len f by A24,FINSEQ_1:1;
then
A32: i1 in dom f by FINSEQ_1:def 3;
then consider i0,j0 being Nat such that
A33: [i0,j0] in Indices G and
A34: f/.i1 = G*(i0,j0) by A1,GOBOARD1:def 9;
A35: 1 <= i0 & i0 <= len G by A33,MATRIX_0:32;
A36: 1 <= j0 by A33,MATRIX_0:32;
A37: j0 <= width G by A33,MATRIX_0:32;
A38: jo <= width G by A28,MATRIX_0:32;
A39: f is special by A1,A32,JORDAN8:4,RELAT_1:38;
ex n st j <= n & n <= k & G*(i,n) = p
proof
per cases by A24,A25,A39,TOPREAL1:def 5;
suppose
A40: (f/.i1)`1 = (f/.(i1+1))`1;
G*(io,j)`1 = G*(io,1)`1 by A14,A19,A30,GOBOARD5:2
.= G*(io,jo)`1 by A30,A31,A38,GOBOARD5:2
.= p`1 by A26,A29,A40,GOBOARD7:5
.= G*(i,j)`1 by A20,A9,GOBOARD7:5;
then
io<=i & io>=i by A6,A14,A19,A30,GOBOARD5:3;
then
A41: i=io by XXREAL_0:1;
G*(i0,j)`1 = G*(i0,1)`1 by A14,A19,A35,GOBOARD5:2
.= G*(i0,j0)`1 by A35,A36,A37,GOBOARD5:2
.= p`1 by A26,A34,A40,GOBOARD7:5
.= G*(i,j)`1 by A20,A9,GOBOARD7:5;
then
i0<=i & i0>=i by A6,A14,A19,A35,GOBOARD5:3;
then
A42: i=i0 by XXREAL_0:1;
thus thesis
proof
per cases;
suppose
A43: (f/.i1)`2 <= (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose
A44: (f/.i1) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.i1 in L~f by A25,A32,GOBOARD1:1,XXREAL_0:2;
then f/.i1 in X1 by A44,XBOOLE_0:def 4;
then
A45: p`2 <= (f/.i1)`2 by A10,A12,PSCOMP_1:24;
take n=j0;
A46: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 4;
p`2 >= (f/.i1)`2 by A26,A43,TOPREAL1:4;
then p`2 = (f/.i1)`2 by A45,XXREAL_0:1;
then
A47: p`2 = G*(1,j0)`2 by A34,A35,A36,A37,GOBOARD5:1
.= G*(i,n)`2 by A6,A36,A37,GOBOARD5:1;
A48: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A14,A15,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A46,A47,TOPREAL1:4;
hence j <= n by A6,A19,A36,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k) `2 by A46,A47,A48,TOPREAL1:4;
hence n <= k by A13,A11,A37,GOBOARD5:4;
p`1 = G*(i,j)`1 by A20,A46,GOBOARD7:5
.= G*(i,1)`1 by A6,A14,A19,GOBOARD5:2
.= G*(i,n)`1 by A6,A36,A37,GOBOARD5:2;
hence thesis by A47,TOPREAL3:6;
end;
suppose
A49: not f/.i1 in LSeg(G*(i,j),G*(i,k));
A50: (f/.i1)`1 = p`1 by A26,A40,GOBOARD7:5
.= G*(i,j)`1 by A20,A9,GOBOARD7:5;
thus thesis
proof
per cases by A20,A49,A50,GOBOARD7:7;
suppose
A51: (f/.i1)`2 < G*(i,j)`2;
p`2 <= G*(io,jo)`2 by A26,A29,A43,TOPREAL1:4;
then p`2 <= G*(1,jo)`2 by A30,A31,A38,GOBOARD5:1;
then p`2 <= G*(i,jo)`2 by A6,A31,A38,GOBOARD5:1;
then G*(i,j)`2 <= G*(i,jo)`2 by A17,XXREAL_0:2;
then
A52: j<=jo by A6,A19,A31,GOBOARD5:4;
|.i0-io.|+|.j0-jo.| = 1 by A1,A32,A27,A33,A34,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then
A53: |.-(j0-jo).| = 1 by COMPLEX1:52;
j0<=jo+0 by A34,A29,A35,A37,A31,A42,A41,A43,GOBOARD5:4;
then j0-jo <= 0 by XREAL_1:20;
then jo-j0 = 1 by A53,ABSVALUE:def 1;
then
A54: j0+1=jo+0;
G*(i,j0)`2 < G*(i,j)`2 & j0<=j by A34,A6,A14,A37,A42,A51,
GOBOARD5:4 ;
then j0<j by XXREAL_0:1;
then jo<=j by A54,NAT_1:13;
then
A55: j=jo by A52,XXREAL_0:1;
take n=jo;
A56: p`1 = G*(i,j)`1 by A20,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A14,A19,GOBOARD5:2
.= G*(i,n)`1 by A6,A31,A38,GOBOARD5:2;
p`2 <= G*(io,jo)`2 by A26,A29,A43,TOPREAL1:4;
then p`2 <= G*(1,jo)`2 by A30,A31,A38,GOBOARD5:1;
then p`2 <= G*(i,jo)`2 by A6,A31,A38,GOBOARD5:1;
then p`2 = G*(i,j)`2 by A17,A55,XXREAL_0:1;
hence thesis by A5,A55,A56,TOPREAL3:6;
end;
suppose
A57: (f/.i1)`2 > G*(i,k)`2;
p`2 >= (f/.i1)`2 by A26,A43,TOPREAL1:4;
hence thesis by A18,A57,XXREAL_0:2;
end;
end;
end;
end;
end;
suppose
A58: (f/.i1)`2 > (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose
A59: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.(i1+1) in L~f by A25,A27,GOBOARD1:1,XXREAL_0:2;
then f/.(i1+1) in X1 by A59,XBOOLE_0:def 4;
then
A60: p`2 <= (f/.(i1+1))`2 by A10,A12,PSCOMP_1:24;
take n=jo;
A61: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 4;
p`2 >= (f/.(i1+1))`2 by A26,A58,TOPREAL1:4;
then p`2 = (f/.(i1+1))`2 by A60,XXREAL_0:1;
then
A62: p`2 = G*(1,jo)`2 by A29,A30,A31,A38,GOBOARD5:1
.= G*(i,n)`2 by A6,A31,A38,GOBOARD5:1;
A63: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A14,A15,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A61,A62,TOPREAL1:4;
hence j <= n by A6,A19,A31,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k) `2 by A61,A62,A63,TOPREAL1:4;
hence n <= k by A13,A11,A38,GOBOARD5:4;
p`1 = G*(i,j)`1 by A20,A61,GOBOARD7:5
.= G*(i,1)`1 by A6,A14,A19,GOBOARD5:2
.= G*(i,n)`1 by A6,A31,A38,GOBOARD5:2;
hence thesis by A62,TOPREAL3:6;
end;
suppose
A64: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k));
A65: (f/.(i1+1))`1 = p`1 by A26,A40,GOBOARD7:5
.= G*(i,j)`1 by A20,A9,GOBOARD7:5;
thus thesis
proof
per cases by A20,A64,A65,GOBOARD7:7;
suppose
A66: (f/.(i1+1))`2 < G*(i,j)`2;
p`2 <= G*(i0,j0)`2 by A26,A34,A58,TOPREAL1:4;
then p`2 <= G*(1,j0)`2 by A35,A36,A37,GOBOARD5:1;
then p`2 <= G*(i,j0)`2 by A6,A36,A37,GOBOARD5:1;
then G*(i,j)`2 <= G*(i,j0)`2 by A17,XXREAL_0:2;
then
A67: j<=j0 by A6,A19,A36,GOBOARD5:4;
jo<=j0+0 by A34,A29,A35,A36,A38,A42,A41,A58,GOBOARD5:4;
then jo-j0 <= 0 by XREAL_1:20;
then
A68: -(jo-j0) >= -0;
|.i0-io.|+|.j0-jo.| = 1 by A1,A32,A27,A33,A34,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then j0-jo = 1 by A68,ABSVALUE:def 1;
then
A69: jo+1=j0-0;
G*(i,jo)`2 < G*(i,j)`2 & jo<=j by A29,A6,A14,A38,A41,A66,
GOBOARD5:4 ;
then jo<j by XXREAL_0:1;
then j0<=j by A69,NAT_1:13;
then
A70: j=j0 by A67,XXREAL_0:1;
take n=j0;
A71: p`1 = G*(i,j)`1 by A20,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A14,A19,GOBOARD5:2
.= G*(i,n)`1 by A6,A36,A37,GOBOARD5:2;
p`2 <= G*(i0,j0)`2 by A26,A34,A58,TOPREAL1:4;
then p`2 <= G*(1,j0)`2 by A35,A36,A37,GOBOARD5:1;
then p`2 <= G*(i,j0)`2 by A6,A36,A37,GOBOARD5:1;
then p`2 = G*(i,j)`2 by A17,A70,XXREAL_0:1;
hence thesis by A5,A70,A71,TOPREAL3:6;
end;
suppose
A72: (f/.(i1+1))`2 > G*(i,k)`2;
p`2 >= (f/.(i1+1))`2 by A26,A58,TOPREAL1:4;
hence thesis by A18,A72,XXREAL_0:2;
end;
end;
end;
end;
end;
end;
end;
suppose
A73: (f/.i1)`2 = (f/.(i1+1))`2;
take n=j0;
p`2 = (f/.i1)`2 by A26,A73,GOBOARD7:6;
then
A74: p`2 = G*(1,j0)`2 by A34,A35,A36,A37,GOBOARD5:1
.= G*(i,n)`2 by A6,A36,A37,GOBOARD5:1;
A75: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A14,A15,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A9,A74,TOPREAL1:4;
hence j <= n by A6,A19,A36,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k)`2 by A9,A74,A75,TOPREAL1:4;
hence n <= k by A13,A11,A37,GOBOARD5:4;
p`1 = G*(i,j)`1 by A20,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A14,A19,GOBOARD5:2
.= G*(i,n)`1 by A6,A36,A37,GOBOARD5:2;
hence thesis by A74,TOPREAL3:6;
end;
end;
hence thesis by A12;
end;
theorem
f is_sequence_on G & LSeg(G*(i,j),G*(i,k)) meets L~f & [i,j] in
Indices G & [i,k] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(i,
n)`2 = upper_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f))
proof
set X = LSeg(G*(i,j),G*(i,k)) /\ L~f;
assume that
A1: f is_sequence_on G and
A2: LSeg(G*(i,j),G*(i,k)) meets L~f and
A3: [i,j] in Indices G and
A4: [i,k] in Indices G and
A5: j <= k;
A6: 1 <= i & i <= len G by A3,MATRIX_0:32;
ex x being object st x in LSeg(G*(i,j),G*(i,k)) & x in L~f by A2,XBOOLE_0:3;
then reconsider X1=X as non empty compact Subset of TOP-REAL 2
by XBOOLE_0:def 4;
consider p being object such that
A7: p in N-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A7;
A8: p in X by A7,XBOOLE_0:def 4;
then
A9: p in LSeg(G*(i,j),G*(i,k)) by XBOOLE_0:def 4;
p in L~f by A8,XBOOLE_0:def 4;
then p in union { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TOPREAL1:def 4;
then consider Y being set such that
A10: p in Y and
A11: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TARSKI:def 4;
consider i1 being Nat such that
A12: Y = LSeg(f,i1) and
A13: 1 <= i1 and
A14: i1+1 <= len f by A11;
A15: p in LSeg(f/.i1,f/.(i1+1)) by A10,A12,A13,A14,TOPREAL1:def 3;
proj2.:X = (proj2|X).:X by RELAT_1:129;
then
A16: upper_bound(proj2.:X) = upper_bound((proj2|X).: [#]((TOP-REAL 2)|X))
by PRE_TOPC:def 5
.= N-bound X;
A17: 1 <= k by A4,MATRIX_0:32;
A18: 1 <= j by A3,MATRIX_0:32;
1 < i1+1 by A13,NAT_1:13;
then i1+1 in Seg len f by A14,FINSEQ_1:1;
then
A19: i1+1 in dom f by FINSEQ_1:def 3;
then consider io,jo being Nat such that
A20: [io,jo] in Indices G and
A21: f/.(i1+1) = G*(io,jo) by A1,GOBOARD1:def 9;
A22: 1 <= io & io <= len G by A20,MATRIX_0:32;
A23: 1 <= jo by A20,MATRIX_0:32;
A24: p`2 = (N-min X)`2 by A7,PSCOMP_1:39
.= upper_bound(proj2.:X) by A16,EUCLID:52;
A25: 1 <= i & i <= len G by A3,MATRIX_0:32;
A26: k <= width G by A4,MATRIX_0:32;
then
A27: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A18,SPRECT_3:12;
then
A28: G*(i,j)`2 <= p`2 by A9,TOPREAL1:4;
A29: p`2 <= G*(i,k)`2 by A9,A27,TOPREAL1:4;
A30: j <= width G by A3,MATRIX_0:32;
then
A31: G*(i,j)`1 = G*(i,1)`1 by A6,A18,GOBOARD5:2
.= G*(i,k)`1 by A25,A17,A26,GOBOARD5:2;
A32: jo <= width G by A20,MATRIX_0:32;
i1 <= len f by A14,NAT_1:13;
then i1 in Seg len f by A13,FINSEQ_1:1;
then
A33: i1 in dom f by FINSEQ_1:def 3;
then consider i0,j0 being Nat such that
A34: [i0,j0] in Indices G and
A35: f/.i1 = G*(i0,j0) by A1,GOBOARD1:def 9;
A36: 1 <= i0 & i0 <= len G by A34,MATRIX_0:32;
A37: 1 <= j0 by A34,MATRIX_0:32;
A38: j0 <= width G by A34,MATRIX_0:32;
A39: f is special by A1,A33,JORDAN8:4,RELAT_1:38;
ex n st j <= n & n <= k & G*(i,n) = p
proof
per cases by A13,A14,A39,TOPREAL1:def 5;
suppose
A40: (f/.i1)`1 = (f/.(i1+1))`1;
G*(io,j)`1 = G*(io,1)`1 by A18,A30,A22,GOBOARD5:2
.= G*(io,jo)`1 by A22,A23,A32,GOBOARD5:2
.= p`1 by A15,A21,A40,GOBOARD7:5
.= G*(i,j)`1 by A31,A9,GOBOARD7:5;
then
io<=i & io>=i by A6,A18,A30,A22,GOBOARD5:3;
then
A41: i=io by XXREAL_0:1;
G*(i0,j)`1 = G*(i0,1)`1 by A18,A30,A36,GOBOARD5:2
.= G*(i0,j0)`1 by A36,A37,A38,GOBOARD5:2
.= p`1 by A15,A35,A40,GOBOARD7:5
.= G*(i,j)`1 by A31,A9,GOBOARD7:5;
then
i0<=i & i0>=i by A6,A18,A30,A36,GOBOARD5:3;
then
A42: i=i0 by XXREAL_0:1;
thus thesis
proof
per cases;
suppose
A43: (f/.i1)`2 <= (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose
A44: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A13,XREAL_1:6;
then f/.(i1+1) in L~f by A14,A19,GOBOARD1:1,XXREAL_0:2;
then f/.(i1+1) in X1 by A44,XBOOLE_0:def 4;
then
A45: p`2 >= (f/.(i1+1))`2 by A16,A24,PSCOMP_1:24;
take n=jo;
A46: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 4;
p`2 <= (f/.(i1+1))`2 by A15,A43,TOPREAL1:4;
then p`2 = (f/.(i1+1))`2 by A45,XXREAL_0:1;
then
A47: p`2 = G*(1,jo)`2 by A21,A22,A23,A32,GOBOARD5:1
.= G*(i,n)`2 by A6,A23,A32,GOBOARD5:1;
A48: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A18,A26,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A46,A47,TOPREAL1:4;
hence j <= n by A6,A30,A23,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k) `2 by A46,A47,A48,TOPREAL1:4;
hence n <= k by A25,A17,A32,GOBOARD5:4;
p`1 = G*(i,j)`1 by A31,A46,GOBOARD7:5
.= G*(i,1)`1 by A6,A18,A30,GOBOARD5:2
.= G*(i,n)`1 by A6,A23,A32,GOBOARD5:2;
hence thesis by A47,TOPREAL3:6;
end;
suppose
A49: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k));
A50: (f/.(i1+1))`1 = p`1 by A15,A40,GOBOARD7:5
.= G*(i,j)`1 by A31,A9,GOBOARD7:5;
thus thesis
proof
per cases by A31,A49,A50,GOBOARD7:7;
suppose
A51: (f/.(i1+1))`2 > G*(i,k)`2;
p`2 >= G*(i0,j0)`2 by A15,A35,A43,TOPREAL1:4;
then p`2 >= G*(1,j0)`2 by A36,A37,A38,GOBOARD5:1;
then p`2 >= G*(i,j0)`2 by A6,A37,A38,GOBOARD5:1;
then G*(i,k)`2 >= G*(i,j0)`2 by A29,XXREAL_0:2;
then
A52: k>=j0 by A25,A17,A38,GOBOARD5:4;
|.i0-io.|+|.j0-jo.| = 1 by A1,A33,A19,A34,A35,A20,A21,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then
A53: |.-(j0-jo).| = 1 by COMPLEX1:52;
j0<=jo+0 by A35,A21,A36,A38,A23,A42,A41,A43,GOBOARD5:4;
then j0-jo <= 0 by XREAL_1:20;
then jo-j0 = 1 by A53,ABSVALUE:def 1;
then
A54: j0+1=jo+0;
G*(i,jo)`2 > G*(i,k)`2 & jo>=k by A21,A25,A26,A23,A41,A51,
GOBOARD5:4 ;
then jo>k by XXREAL_0:1;
then j0>=k by A54,NAT_1:13;
then
A55: k=j0 by A52,XXREAL_0:1;
take n=j0;
A56: p`1 = G*(i,j)`1 by A31,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A18,A30,GOBOARD5:2
.= G*(i,n)`1 by A6,A37,A38,GOBOARD5:2;
p`2 >= G*(i0,j0)`2 by A15,A35,A43,TOPREAL1:4;
then p`2 >= G*(1,j0)`2 by A36,A37,A38,GOBOARD5:1;
then p`2 >= G*(i,j0)`2 by A6,A37,A38,GOBOARD5:1;
then p`2 = G*(i,k)`2 by A29,A55,XXREAL_0:1;
hence thesis by A5,A55,A56,TOPREAL3:6;
end;
suppose
A57: (f/.(i1+1))`2 < G*(i,j)`2;
p`2 <= (f/.(i1+1))`2 by A15,A43,TOPREAL1:4;
hence thesis by A28,A57,XXREAL_0:2;
end;
end;
end;
end;
end;
suppose
A58: (f/.i1)`2 > (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose
A59: f/.i1 in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A13,XREAL_1:6;
then f/.i1 in L~f by A14,A33,GOBOARD1:1,XXREAL_0:2;
then f/.i1 in X1 by A59,XBOOLE_0:def 4;
then
A60: p`2 >= (f/.i1)`2 by A16,A24,PSCOMP_1:24;
take n=j0;
A61: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 4;
p`2 <= (f/.i1)`2 by A15,A58,TOPREAL1:4;
then p`2 = (f/.i1)`2 by A60,XXREAL_0:1;
then
A62: p`2 = G*(1,j0)`2 by A35,A36,A37,A38,GOBOARD5:1
.= G*(i,n)`2 by A6,A37,A38,GOBOARD5:1;
A63: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A18,A26,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A61,A62,TOPREAL1:4;
hence j <= n by A6,A30,A37,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k) `2 by A61,A62,A63,TOPREAL1:4;
hence n <= k by A25,A17,A38,GOBOARD5:4;
p`1 = G*(i,j)`1 by A31,A61,GOBOARD7:5
.= G*(i,1)`1 by A6,A18,A30,GOBOARD5:2
.= G*(i,n)`1 by A6,A37,A38,GOBOARD5:2;
hence thesis by A62,TOPREAL3:6;
end;
suppose
A64: not f/.i1 in LSeg(G*(i,j),G*(i,k));
A65: (f/.i1)`1 = p`1 by A15,A40,GOBOARD7:5
.= G*(i,j)`1 by A31,A9,GOBOARD7:5;
thus thesis
proof
per cases by A31,A64,A65,GOBOARD7:7;
suppose
A66: (f/.i1)`2 > G*(i,k)`2;
p`2 >= G*(io,jo)`2 by A15,A21,A58,TOPREAL1:4;
then p`2 >= G*(1,jo)`2 by A22,A23,A32,GOBOARD5:1;
then p`2 >= G*(i,jo)`2 by A6,A23,A32,GOBOARD5:1;
then G*(i,k)`2 >= G*(i,jo)`2 by A29,XXREAL_0:2;
then
A67: k>=jo by A25,A17,A32,GOBOARD5:4;
jo<=j0+0 by A35,A21,A36,A37,A32,A42,A41,A58,GOBOARD5:4;
then jo-j0 <= 0 by XREAL_1:20;
then
A68: -(jo-j0) >= -0;
|.i0-io.|+|.j0-jo.| = 1 by A1,A33,A19,A34,A35,A20,A21,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then j0-jo = 1 by A68,ABSVALUE:def 1;
then
A69: jo+1=j0-0;
G*(i,j0)`2 > G*(i,k)`2 & j0>=k by A35,A25,A26,A37,A42,A66,
GOBOARD5:4 ;
then j0>k by XXREAL_0:1;
then jo>=k by A69,NAT_1:13;
then
A70: k=jo by A67,XXREAL_0:1;
take n=jo;
A71: p`1 = G*(i,j)`1 by A31,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A18,A30,GOBOARD5:2
.= G*(i,n)`1 by A6,A23,A32,GOBOARD5:2;
p`2 >= G*(io,jo)`2 by A15,A21,A58,TOPREAL1:4;
then p`2 >= G*(1,jo)`2 by A22,A23,A32,GOBOARD5:1;
then p`2 >= G*(i,jo)`2 by A6,A23,A32,GOBOARD5:1;
then p`2 = G*(i,k)`2 by A29,A70,XXREAL_0:1;
hence thesis by A5,A70,A71,TOPREAL3:6;
end;
suppose
A72: (f/.i1)`2 < G*(i,j)`2;
p`2 <= (f/.i1)`2 by A15,A58,TOPREAL1:4;
hence thesis by A28,A72,XXREAL_0:2;
end;
end;
end;
end;
end;
end;
end;
suppose
A73: (f/.i1)`2 = (f/.(i1+1))`2;
take n=j0;
p`2 = (f/.i1)`2 by A15,A73,GOBOARD7:6;
then
A74: p`2 = G*(1,j0)`2 by A35,A36,A37,A38,GOBOARD5:1
.= G*(i,n)`2 by A6,A37,A38,GOBOARD5:1;
A75: G*(i,j)`2 <= G*(i,k)`2 by A5,A6,A18,A26,SPRECT_3:12;
then G*(i,j)`2 <= G*(i,n)`2 by A9,A74,TOPREAL1:4;
hence j <= n by A6,A30,A37,GOBOARD5:4;
G*(i,n)`2 <= G*(i,k)`2 by A9,A74,A75,TOPREAL1:4;
hence n <= k by A25,A17,A38,GOBOARD5:4;
p`1 = G*(i,j)`1 by A31,A9,GOBOARD7:5
.= G*(i,1)`1 by A6,A18,A30,GOBOARD5:2
.= G*(i,n)`1 by A6,A37,A38,GOBOARD5:2;
hence thesis by A74,TOPREAL3:6;
end;
end;
hence thesis by A24;
end;
theorem
f is_sequence_on G & LSeg(G*(j,i),G*(k,i)) meets L~f & [j,i] in
Indices G & [k,i] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(n,
i)`1 = lower_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f))
proof
set X = LSeg(G*(j,i),G*(k,i)) /\ L~f;
assume that
A1: f is_sequence_on G and
A2: LSeg(G*(j,i),G*(k,i)) meets L~f and
A3: [j,i] in Indices G and
A4: [k,i] in Indices G and
A5: j <= k;
A6: 1 <= j by A3,MATRIX_0:32;
ex x being object st x in LSeg(G*(j,i),G*(k,i)) & x in L~f by A2,XBOOLE_0:3;
then reconsider X1=X as non empty compact Subset of TOP-REAL 2
by XBOOLE_0:def 4;
consider p being object such that
A7: p in W-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A7;
A8: p in X by A7,XBOOLE_0:def 4;
then
A9: p in LSeg(G*(j,i),G*(k,i)) by XBOOLE_0:def 4;
proj1.:X = (proj1|X).:X by RELAT_1:129;
then
A10: lower_bound(proj1.:X) = lower_bound((proj1|X).: [#]((TOP-REAL 2)|X))
by PRE_TOPC:def 5
.= W-bound X;
A11: 1 <= k & 1 <= i by A4,MATRIX_0:32;
A12: p`1 = (W-min X)`1 by A7,PSCOMP_1:31
.= lower_bound(proj1.:X) by A10,EUCLID:52;
A13: i <= width G by A3,MATRIX_0:32;
A14: 1 <= i & i <= width G by A3,MATRIX_0:32;
A15: k <= len G by A4,MATRIX_0:32;
then
A16: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,SPRECT_3:13;
then
A17: G*(j,i)`1 <= p`1 by A9,TOPREAL1:3;
A18: p`1 <= G*(k,i)`1 by A9,A16,TOPREAL1:3;
A19: j <= len G by A3,MATRIX_0:32;
then
A20: G*(j,i)`2 = G*(1,i)`2 by A6,A14,GOBOARD5:1
.= G*(k,i)`2 by A15,A11,A13,GOBOARD5:1;
p in L~f by A8,XBOOLE_0:def 4;
then p in union { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TOPREAL1:def 4;
then consider Y being set such that
A21: p in Y and
A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TARSKI:def 4;
consider i1 being Nat such that
A23: Y = LSeg(f,i1) and
A24: 1 <= i1 and
A25: i1+1 <= len f by A22;
A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3;
1 < i1+1 by A24,NAT_1:13;
then i1+1 in Seg len f by A25,FINSEQ_1:1;
then
A27: i1+1 in dom f by FINSEQ_1:def 3;
then consider jo,io being Nat such that
A28: [jo,io] in Indices G and
A29: f/.(i1+1) = G*(jo,io) by A1,GOBOARD1:def 9;
A30: 1 <= jo by A28,MATRIX_0:32;
i1 <= len f by A25,NAT_1:13;
then i1 in Seg len f by A24,FINSEQ_1:1;
then
A31: i1 in dom f by FINSEQ_1:def 3;
then consider j0,i0 being Nat such that
A32: [j0,i0] in Indices G and
A33: f/.i1 = G*(j0,i0) by A1,GOBOARD1:def 9;
A34: 1 <= j0 by A32,MATRIX_0:32;
A35: 1 <= i0 & i0 <= width G by A32,MATRIX_0:32;
A36: j0 <= len G by A32,MATRIX_0:32;
A37: 1 <= io & io <= width G by A28,MATRIX_0:32;
A38: jo <= len G by A28,MATRIX_0:32;
A39: f is special by A1,A31,JORDAN8:4,RELAT_1:38;
ex n st j <= n & n <= k & G*(n,i) = p
proof
per cases by A24,A25,A39,TOPREAL1:def 5;
suppose
A40: (f/.i1)`2 = (f/.(i1+1))`2;
G*(j,io)`2 = G*(1,io)`2 by A6,A19,A37,GOBOARD5:1
.= G*(jo,io)`2 by A30,A38,A37,GOBOARD5:1
.= p`2 by A26,A29,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
then
io<=i & io>=i by A6,A19,A14,A37,GOBOARD5:4;
then
A41: i=io by XXREAL_0:1;
G*(j,i0)`2 = G*(1,i0)`2 by A6,A19,A35,GOBOARD5:1
.= G*(j0,i0)`2 by A34,A36,A35,GOBOARD5:1
.= p`2 by A26,A33,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
then
i0<=i & i0>=i by A6,A19,A14,A35,GOBOARD5:4;
then
A42: i=i0 by XXREAL_0:1;
thus thesis
proof
per cases;
suppose
A43: (f/.i1)`1 <= (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose
A44: (f/.i1) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.i1 in L~f by A25,A31,GOBOARD1:1,XXREAL_0:2;
then f/.i1 in X1 by A44,XBOOLE_0:def 4;
then
A45: p`1 <= (f/.i1)`1 by A10,A12,PSCOMP_1:24;
take n=j0;
A46: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 4;
p`1 >= (f/.i1)`1 by A26,A43,TOPREAL1:3;
then p`1 = (f/.i1)`1 by A45,XXREAL_0:1;
then
A47: p`1 = G*(j0,1)`1 by A33,A34,A36,A35,GOBOARD5:2
.= G*(n,i)`1 by A14,A34,A36,GOBOARD5:2;
A48: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A46,A47,TOPREAL1:3;
hence j <= n by A19,A14,A34,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i) `1 by A46,A47,A48,TOPREAL1:3;
hence n <= k by A11,A13,A36,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A46,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
hence thesis by A47,TOPREAL3:6;
end;
suppose
A49: not f/.i1 in LSeg(G*(j,i),G*(k,i));
A50: (f/.i1)`2 = p`2 by A26,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
thus thesis
proof
per cases by A20,A49,A50,GOBOARD7:8;
suppose
A51: (f/.i1)`1 < G*(j,i)`1;
p`1 <= G*(jo,io)`1 by A26,A29,A43,TOPREAL1:3;
then p`1 <= G*(jo,1)`1 by A30,A38,A37,GOBOARD5:2;
then p`1 <= G*(jo,i)`1 by A14,A30,A38,GOBOARD5:2;
then G*(j,i)`1 <= G*(jo,i)`1 by A17,XXREAL_0:2;
then
A52: j<=jo by A19,A14,A30,GOBOARD5:3;
|.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then
A53: |.-(j0-jo).| = 1 by COMPLEX1:52;
j0<=jo+0 by A33,A29,A36,A35,A30,A42,A41,A43,GOBOARD5:3;
then j0-jo <= 0 by XREAL_1:20;
then jo-j0 = 1 by A53,ABSVALUE:def 1;
then
A54: j0+1=jo+0;
G*(j0,i)`1 < G*(j,i)`1 & j0<=j by A33,A6,A14,A36,A42,A51,
GOBOARD5:3 ;
then j0<j by XXREAL_0:1;
then jo<=j by A54,NAT_1:13;
then
A55: j=jo by A52,XXREAL_0:1;
take n=jo;
A56: p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A30,A38,GOBOARD5:1;
p`1 <= G*(jo,io)`1 by A26,A29,A43,TOPREAL1:3;
then p`1 <= G*(jo,1)`1 by A30,A38,A37,GOBOARD5:2;
then p`1 <= G*(jo,i)`1 by A14,A30,A38,GOBOARD5:2;
then p`1 = G*(j,i)`1 by A17,A55,XXREAL_0:1;
hence thesis by A5,A55,A56,TOPREAL3:6;
end;
suppose
A57: (f/.i1)`1 > G*(k,i)`1;
p`1 >= (f/.i1)`1 by A26,A43,TOPREAL1:3;
hence thesis by A18,A57,XXREAL_0:2;
end;
end;
end;
end;
end;
suppose
A58: (f/.i1)`1 > (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose
A59: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.(i1+1) in L~f by A25,A27,GOBOARD1:1,XXREAL_0:2;
then f/.(i1+1) in X1 by A59,XBOOLE_0:def 4;
then
A60: p`1 <= (f/.(i1+1))`1 by A10,A12,PSCOMP_1:24;
take n=jo;
A61: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 4;
p`1 >= (f/.(i1+1))`1 by A26,A58,TOPREAL1:3;
then p`1 = (f/.(i1+1))`1 by A60,XXREAL_0:1;
then
A62: p`1 = G*(jo,1)`1 by A29,A30,A38,A37,GOBOARD5:2
.= G*(n,i)`1 by A14,A30,A38,GOBOARD5:2;
A63: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A61,A62,TOPREAL1:3;
hence j <= n by A19,A14,A30,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i) `1 by A61,A62,A63,TOPREAL1:3;
hence n <= k by A11,A13,A38,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A61,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A30,A38,GOBOARD5:1;
hence thesis by A62,TOPREAL3:6;
end;
suppose
A64: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i));
A65: (f/.(i1+1))`2 = p`2 by A26,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
thus thesis
proof
per cases by A20,A64,A65,GOBOARD7:8;
suppose
A66: (f/.(i1+1))`1 < G*(j,i)`1;
p`1 <= G*(j0,i0)`1 by A26,A33,A58,TOPREAL1:3;
then p`1 <= G*(j0,1)`1 by A34,A36,A35,GOBOARD5:2;
then p`1 <= G*(j0,i)`1 by A14,A34,A36,GOBOARD5:2;
then G*(j,i)`1 <= G*(j0,i)`1 by A17,XXREAL_0:2;
then
A67: j<=j0 by A19,A14,A34,GOBOARD5:3;
jo<=j0+0 by A33,A29,A34,A35,A38,A42,A41,A58,GOBOARD5:3;
then jo-j0 <= 0 by XREAL_1:20;
then
A68: -(jo-j0) >= -0;
|.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then j0-jo = 1 by A68,ABSVALUE:def 1;
then
A69: jo+1=j0-0;
G*(jo,i)`1 < G*(j,i)`1 & jo<=j by A29,A6,A14,A38,A41,A66,
GOBOARD5:3 ;
then jo<j by XXREAL_0:1;
then j0<=j by A69,NAT_1:13;
then
A70: j=j0 by A67,XXREAL_0:1;
take n=j0;
A71: p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
p`1 <= G*(j0,i0)`1 by A26,A33,A58,TOPREAL1:3;
then p`1 <= G*(j0,1)`1 by A34,A36,A35,GOBOARD5:2;
then p`1 <= G*(j0,i)`1 by A14,A34,A36,GOBOARD5:2;
then p`1 = G*(j,i)`1 by A17,A70,XXREAL_0:1;
hence thesis by A5,A70,A71,TOPREAL3:6;
end;
suppose
A72: (f/.(i1+1))`1 > G*(k,i)`1;
p`1 >= (f/.(i1+1))`1 by A26,A58,TOPREAL1:3;
hence thesis by A18,A72,XXREAL_0:2;
end;
end;
end;
end;
end;
end;
end;
suppose
A73: (f/.i1)`1 = (f/.(i1+1))`1;
take n=j0;
p`1 = (f/.i1)`1 by A26,A73,GOBOARD7:5;
then
A74: p`1 = G*(j0,1)`1 by A33,A34,A36,A35,GOBOARD5:2
.= G*(n,i)`1 by A14,A34,A36,GOBOARD5:2;
A75: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A9,A74,TOPREAL1:3;
hence j <= n by A19,A14,A34,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i)`1 by A9,A74,A75,TOPREAL1:3;
hence n <= k by A11,A13,A36,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
hence thesis by A74,TOPREAL3:6;
end;
end;
hence thesis by A12;
end;
theorem
f is_sequence_on G & LSeg(G*(j,i),G*(k,i)) meets L~f & [j,i] in
Indices G & [k,i] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(n,
i)`1 = upper_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f))
proof
set X = LSeg(G*(j,i),G*(k,i)) /\ L~f;
assume that
A1: f is_sequence_on G and
A2: LSeg(G*(j,i),G*(k,i)) meets L~f and
A3: [j,i] in Indices G and
A4: [k,i] in Indices G and
A5: j <= k;
A6: 1 <= j by A3,MATRIX_0:32;
ex x being object st x in LSeg(G*(j,i),G*(k,i)) & x in L~f by A2,XBOOLE_0:3;
then reconsider X1=X as non empty compact Subset of TOP-REAL 2
by XBOOLE_0:def 4;
consider p being object such that
A7: p in E-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A7;
A8: p in X by A7,XBOOLE_0:def 4;
then
A9: p in LSeg(G*(j,i),G*(k,i)) by XBOOLE_0:def 4;
proj1.:X = (proj1|X).:X by RELAT_1:129;
then
A10: upper_bound(proj1.:X) = upper_bound((proj1|X).: [#]((TOP-REAL 2)|X))
by PRE_TOPC:def 5
.= E-bound X;
A11: 1 <= i & i <= width G by A3,MATRIX_0:32;
A12: p`1 = (E-min X)`1 by A7,PSCOMP_1:47
.= upper_bound(proj1.:X) by A10,EUCLID:52;
A13: 1 <= k by A4,MATRIX_0:32;
A14: 1 <= i & i <= width G by A3,MATRIX_0:32;
A15: k <= len G by A4,MATRIX_0:32;
then
A16: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,SPRECT_3:13;
then
A17: G*(j,i)`1 <= p`1 by A9,TOPREAL1:3;
A18: p`1 <= G*(k,i)`1 by A9,A16,TOPREAL1:3;
A19: j <= len G by A3,MATRIX_0:32;
then
A20: G*(j,i)`2 = G*(1,i)`2 by A6,A14,GOBOARD5:1
.= G*(k,i)`2 by A13,A15,A11,GOBOARD5:1;
p in L~f by A8,XBOOLE_0:def 4;
then p in union { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TOPREAL1:def 4;
then consider Y being set such that
A21: p in Y and
A22: Y in { LSeg(f,k1) where k1 is Nat : 1 <= k1 & k1+1 <=
len f} by TARSKI:def 4;
consider i1 being Nat such that
A23: Y = LSeg(f,i1) and
A24: 1 <= i1 and
A25: i1+1 <= len f by A22;
A26: p in LSeg(f/.i1,f/.(i1+1)) by A21,A23,A24,A25,TOPREAL1:def 3;
1 < i1+1 by A24,NAT_1:13;
then i1+1 in Seg len f by A25,FINSEQ_1:1;
then
A27: i1+1 in dom f by FINSEQ_1:def 3;
then consider jo,io being Nat such that
A28: [jo,io] in Indices G and
A29: f/.(i1+1) = G*(jo,io) by A1,GOBOARD1:def 9;
A30: 1 <= jo by A28,MATRIX_0:32;
i1 <= len f by A25,NAT_1:13;
then i1 in Seg len f by A24,FINSEQ_1:1;
then
A31: i1 in dom f by FINSEQ_1:def 3;
then consider j0,i0 being Nat such that
A32: [j0,i0] in Indices G and
A33: f/.i1 = G*(j0,i0) by A1,GOBOARD1:def 9;
A34: 1 <= j0 by A32,MATRIX_0:32;
A35: 1 <= i0 & i0 <= width G by A32,MATRIX_0:32;
A36: j0 <= len G by A32,MATRIX_0:32;
A37: 1 <= io & io <= width G by A28,MATRIX_0:32;
A38: jo <= len G by A28,MATRIX_0:32;
A39: f is special by A1,A31,JORDAN8:4,RELAT_1:38;
ex n st j <= n & n <= k & G*(n,i) = p
proof
per cases by A24,A25,A39,TOPREAL1:def 5;
suppose
A40: (f/.i1)`2 = (f/.(i1+1))`2;
G*(j,io)`2 = G*(1,io)`2 by A6,A19,A37,GOBOARD5:1
.= G*(jo,io)`2 by A30,A38,A37,GOBOARD5:1
.= p`2 by A26,A29,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
then
io<=i & io>=i by A6,A19,A14,A37,GOBOARD5:4;
then
A41: i=io by XXREAL_0:1;
G*(j,i0)`2 = G*(1,i0)`2 by A6,A19,A35,GOBOARD5:1
.= G*(j0,i0)`2 by A34,A36,A35,GOBOARD5:1
.= p`2 by A26,A33,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
then
i0<=i & i0>=i by A6,A19,A14,A35,GOBOARD5:4;
then
A42: i=i0 by XXREAL_0:1;
thus thesis
proof
per cases;
suppose
A43: (f/.i1)`1 <= (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose
A44: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.(i1+1) in L~f by A25,A27,GOBOARD1:1,XXREAL_0:2;
then f/.(i1+1) in X1 by A44,XBOOLE_0:def 4;
then
A45: p`1 >= (f/.(i1+1))`1 by A10,A12,PSCOMP_1:24;
take n=jo;
A46: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 4;
p`1 <= (f/.(i1+1))`1 by A26,A43,TOPREAL1:3;
then p`1 = (f/.(i1+1))`1 by A45,XXREAL_0:1;
then
A47: p`1 = G*(jo,1)`1 by A29,A30,A38,A37,GOBOARD5:2
.= G*(n,i)`1 by A14,A30,A38,GOBOARD5:2;
A48: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A46,A47,TOPREAL1:3;
hence j <= n by A19,A14,A30,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i) `1 by A46,A47,A48,TOPREAL1:3;
hence n <= k by A13,A11,A38,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A46,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A30,A38,GOBOARD5:1;
hence thesis by A47,TOPREAL3:6;
end;
suppose
A49: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i));
A50: (f/.(i1+1))`2 = p`2 by A26,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
thus thesis
proof
per cases by A20,A49,A50,GOBOARD7:8;
suppose
A51: (f/.(i1+1))`1 > G*(k,i)`1;
p`1 >= G*(j0,i0)`1 by A26,A33,A43,TOPREAL1:3;
then p`1 >= G*(j0,1)`1 by A34,A36,A35,GOBOARD5:2;
then p`1 >= G*(j0,i)`1 by A14,A34,A36,GOBOARD5:2;
then G*(k,i)`1 >= G*(j0,i)`1 by A18,XXREAL_0:2;
then
A52: k>=j0 by A13,A11,A36,GOBOARD5:3;
|.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then
A53: |.-(j0-jo).| = 1 by COMPLEX1:52;
j0<=jo+0 by A33,A29,A36,A35,A30,A42,A41,A43,GOBOARD5:3;
then j0-jo <= 0 by XREAL_1:20;
then jo-j0 = 1 by A53,ABSVALUE:def 1;
then
A54: j0+1=jo+0;
G*(jo,i)`1 > G*(k,i)`1 & jo>=k by A29,A15,A11,A30,A41,A51,
GOBOARD5:3 ;
then jo>k by XXREAL_0:1;
then j0>=k by A54,NAT_1:13;
then
A55: k=j0 by A52,XXREAL_0:1;
take n=j0;
A56: p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
p`1 >= G*(j0,i0)`1 by A26,A33,A43,TOPREAL1:3;
then p`1 >= G*(j0,1)`1 by A34,A36,A35,GOBOARD5:2;
then p`1 >= G*(j0,i)`1 by A14,A34,A36,GOBOARD5:2;
then p`1 = G*(k,i)`1 by A18,A55,XXREAL_0:1;
hence thesis by A5,A55,A56,TOPREAL3:6;
end;
suppose
A57: (f/.(i1+1))`1 < G*(j,i)`1;
p`1 <= (f/.(i1+1))`1 by A26,A43,TOPREAL1:3;
hence thesis by A17,A57,XXREAL_0:2;
end;
end;
end;
end;
end;
suppose
A58: (f/.i1)`1 > (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose
A59: f/.i1 in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A24,XREAL_1:6;
then f/.i1 in L~f by A25,A31,GOBOARD1:1,XXREAL_0:2;
then f/.i1 in X1 by A59,XBOOLE_0:def 4;
then
A60: p`1 >= (f/.i1)`1 by A10,A12,PSCOMP_1:24;
take n=j0;
A61: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 4;
p`1 <= (f/.i1)`1 by A26,A58,TOPREAL1:3;
then p`1 = (f/.i1)`1 by A60,XXREAL_0:1;
then
A62: p`1 = G*(j0,1)`1 by A33,A34,A36,A35,GOBOARD5:2
.= G*(n,i)`1 by A14,A34,A36,GOBOARD5:2;
A63: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A61,A62,TOPREAL1:3;
hence j <= n by A19,A14,A34,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i) `1 by A61,A62,A63,TOPREAL1:3;
hence n <= k by A13,A11,A36,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A61,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
hence thesis by A62,TOPREAL3:6;
end;
suppose
A64: not f/.i1 in LSeg(G*(j,i),G*(k,i));
A65: (f/.i1)`2 = p`2 by A26,A40,GOBOARD7:6
.= G*(j,i)`2 by A20,A9,GOBOARD7:6;
thus thesis
proof
per cases by A20,A64,A65,GOBOARD7:8;
suppose
A66: (f/.i1)`1 > G*(k,i)`1;
p`1 >= G*(jo,io)`1 by A26,A29,A58,TOPREAL1:3;
then p`1 >= G*(jo,1)`1 by A30,A38,A37,GOBOARD5:2;
then p`1 >= G*(jo,i)`1 by A14,A30,A38,GOBOARD5:2;
then G*(k,i)`1 >= G*(jo,i)`1 by A18,XXREAL_0:2;
then
A67: k>=jo by A13,A11,A38,GOBOARD5:3;
jo<=j0+0 by A33,A29,A34,A35,A38,A42,A41,A58,GOBOARD5:3;
then jo-j0 <= 0 by XREAL_1:20;
then
A68: -(jo-j0) >= -0;
|.i0-io.|+|.j0-jo.| = 1 by A1,A31,A27,A32,A33,A28,A29,
GOBOARD1:def 9;
then 0+|.j0-jo.| = 1 by A42,A41,ABSVALUE:2;
then j0-jo = 1 by A68,ABSVALUE:def 1;
then
A69: jo+1=j0-0;
G*(j0,i)`1 > G*(k,i)`1 & j0>=k by A33,A15,A11,A34,A42,A66,
GOBOARD5:3 ;
then j0>k by XXREAL_0:1;
then jo>=k by A69,NAT_1:13;
then
A70: k=jo by A67,XXREAL_0:1;
take n=jo;
A71: p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A30,A38,GOBOARD5:1;
p`1 >= G*(jo,io)`1 by A26,A29,A58,TOPREAL1:3;
then p`1 >= G*(jo,1)`1 by A30,A38,A37,GOBOARD5:2;
then p`1 >= G*(jo,i)`1 by A14,A30,A38,GOBOARD5:2;
then p`1 = G*(k,i)`1 by A18,A70,XXREAL_0:1;
hence thesis by A5,A70,A71,TOPREAL3:6;
end;
suppose
A72: (f/.i1)`1 < G*(j,i)`1;
p`1 <= (f/.i1)`1 by A26,A58,TOPREAL1:3;
hence thesis by A17,A72,XXREAL_0:2;
end;
end;
end;
end;
end;
end;
end;
suppose
A73: (f/.i1)`1 = (f/.(i1+1))`1;
take n=j0;
p`1 = (f/.i1)`1 by A26,A73,GOBOARD7:5;
then
A74: p`1 = G*(j0,1)`1 by A33,A34,A36,A35,GOBOARD5:2
.= G*(n,i)`1 by A14,A34,A36,GOBOARD5:2;
A75: G*(j,i)`1 <= G*(k,i)`1 by A5,A6,A14,A15,SPRECT_3:13;
then G*(j,i)`1 <= G*(n,i)`1 by A9,A74,TOPREAL1:3;
hence j <= n by A19,A14,A34,GOBOARD5:3;
G*(n,i)`1 <= G*(k,i)`1 by A9,A74,A75,TOPREAL1:3;
hence n <= k by A13,A11,A36,GOBOARD5:3;
p`2 = G*(j,i)`2 by A20,A9,GOBOARD7:6
.= G*(1,i)`2 by A6,A19,A14,GOBOARD5:1
.= G*(n,i)`2 by A14,A34,A36,GOBOARD5:1;
hence thesis by A74,TOPREAL3:6;
end;
end;
hence thesis by A12;
end;
theorem Th5:
for C being compact non vertical non horizontal Subset of
TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/.1 = W-min(L~Cage(C,
n))
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
& E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,JORDAN1E:def 1,SPRECT_2:43;
then
W-min L~Cage(C,n) in rng Cage(C,n) & Upper_Seq(C,n)/.1 = Rotate(Cage(C,n
), W-min L~Cage(C,n))/.1 by FINSEQ_5:44,SPRECT_2:43;
hence thesis by FINSEQ_6:92;
end;
theorem Th6:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds Lower_Seq(C,n)/.1 = E-max L~Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n )
by JORDAN1E:def 2;
hence thesis by FINSEQ_5:53;
end;
theorem Th7:
for C being compact non vertical non horizontal Subset of
TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/. len Upper_Seq(C,n)
= E-max(L~Cage(C,n))
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
& rng Rotate(Cage(C,n),W-min L~Cage(C,n)) = rng Cage(C,n) by FINSEQ_6:90
,JORDAN1E:def 1,SPRECT_2:43;
then
len Upper_Seq(C,n) = (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(
C,n)) by FINSEQ_5:42,SPRECT_2:46;
hence thesis by A1,FINSEQ_5:45,SPRECT_2:46;
end;
theorem Th8:
for C be compact non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = W-min L~
Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
& E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,JORDAN1E:def 2,SPRECT_2:43;
hence
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Rotate(Cage(C,n),W-min L~Cage(C,
n))/. (len Rotate(Cage(C,n),W-min L~Cage(C,n))) by FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A1,FINSEQ_6:92;
end;
theorem Th9:
for C being compact non vertical non horizontal Subset of
TOP-REAL 2 for n being Nat holds L~Upper_Seq(C,n) = Upper_Arc L~Cage
(C,n) & L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) or L~Upper_Seq(C,n) =
Lower_Arc L~Cage(C,n) & L~Lower_Seq(C,n) = Upper_Arc L~Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set WC = W-min(L~Cage(C,n));
set EC = E-max(L~Cage(C,n));
A1: Lower_Arc(L~Cage(C,n)) is_an_arc_of WC,EC & Upper_Arc(L~Cage(C,n)) \/
Lower_Arc(L~Cage(C,n))=L~Cage(C,n) by JORDAN6:50;
Upper_Seq(C,n)/.1 = WC & Upper_Seq(C,n)/. len Upper_Seq(C,n) = EC by Th5,Th7;
then
A2: L~Upper_Seq(C,n) is_an_arc_of WC,EC by TOPREAL1:25;
Lower_Seq(C,n)/.1 = EC & Lower_Seq(C,n)/. len Lower_Seq(C,n) = WC by Th6,Th8;
then
A3: L~Lower_Seq(C,n) is_an_arc_of WC,EC by JORDAN5B:14,TOPREAL1:25;
L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n)=L~Cage(C,n) & Upper_Arc(L~Cage(C,n)
) is_an_arc_of WC,EC by JORDAN1E:13,JORDAN6:50;
hence thesis by A2,A3,A1,JORDAN6:48;
end;
reserve C for compact non vertical non horizontal non empty
being_simple_closed_curve Subset of TOP-REAL 2,
p for Point of TOP-REAL 2,
i1, j1,i2,j2 for Nat;
theorem Th10:
for C being connected compact non vertical non horizontal Subset
of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n) is_sequence_on
Gauge(C,n)
proof
let C be connected compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A1: Rotate(Cage(C,n),W-min L~Cage(C,n)) is_sequence_on Gauge(C,n) by
REVROT_1:34;
Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by JORDAN1E:def 1
.= Rotate(Cage(C,n),W-min L~Cage(C,n)) | ((E-max L~Cage(C,n))..Rotate(
Cage(C,n),W-min L~Cage(C,n))) by FINSEQ_5:def 1;
hence thesis by A1,GOBOARD1:22;
end;
theorem Th11: :: symmetric to JORDAN8:9
for f being FinSequence of TOP-REAL 2 st f is_sequence_on G & (
ex i,j st [i,j] in Indices G & p = G*(i,j)) & (for i1,j1,i2,j2 st [i1,j1] in
Indices G & [i2,j2] in Indices G & p = G*(i1,j1) & f/.1 = G*(i2,j2)
holds |.i2-i1.|+|.j2-j1.| = 1) holds <*p*>^f is_sequence_on G
proof
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: ex i,j st [i,j] in Indices G & p = G*(i,j) and
A3: for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & p =
G*(i1,j1) & f/.1 = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1;
A4: now
let m,k,i,j such that
A5: [m,k] in Indices G & [i,j] in Indices G & <*p*>/.(len <*p*>)=G*(m
,k) & f/.1=G*(i,j) and
A6: len <*p*> in dom <*p*> and
1 in dom f;
len <*p*> = 1 by FINSEQ_1:40;
then <*p*>.(len <*p*>) = p by FINSEQ_1:40;
then <*p*>/.(len <*p*>) = p by A6,PARTFUN1:def 6;
then |.i-m.|+|.j-k.|=1 by A3,A5;
hence 1 = |.m-i.|+|.j-k.| by UNIFORM1:11
.= |.m-i.|+|.k-j.| by UNIFORM1:11;
end;
A7: now
let n such that
A8: n in dom(<*p*>^f);
per cases by A8,FINSEQ_1:25;
suppose
A9: n in dom <*p*>;
consider i,j such that
A10: [i,j] in Indices G and
A11: p = G*(i,j) by A2;
take i,j;
thus [i,j] in Indices G by A10;
n in Seg 1 by A9,FINSEQ_1:38;
then 1 <= n & n <= 1 by FINSEQ_1:1;
then n=1 by XXREAL_0:1;
then <*p*>.n = p by FINSEQ_1:40;
then <*p*>/.n = p by A9,PARTFUN1:def 6;
hence (<*p*>^f)/.n = G*(i,j) by A9,A11,FINSEQ_4:68;
end;
suppose
ex l be Nat st l in dom f & n = (len <*p*>) + l;
then consider l be Nat such that
A12: l in dom f and
A13: n = (len <*p*>) + l;
consider i,j such that
A14: [i,j] in Indices G and
A15: f/.l = G*(i,j) by A1,A12,GOBOARD1:def 9;
take i,j;
thus [i,j] in Indices G by A14;
thus (<*p*>^f)/.n = G*(i,j) by A12,A13,A15,FINSEQ_4:69;
end;
end;
A16: now
let n;
assume that
A17: n in dom <*p*> and
A18: n+1 in dom <*p*>;
n+1 <= len <*p*> by A18,FINSEQ_3:25;
then
A19: n+1 <= 1 by FINSEQ_1:39;
1 <= n by A17,FINSEQ_3:25;
then 1+1 <= n+1 by XREAL_1:6;
hence
for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & <*p*>/.n=G*(
m,k) & <*p*>/.(n+1)=G*(i,j) holds |.m-i.|+|.k-j.|=1 by A19,XXREAL_0:2;
end;
for n st n in dom f & n+1 in dom f holds for m,k,i,j st [m,k] in Indices
G & [i,j] in Indices G & f/.n=G*(m,k) & f/.(n+1)=G*(i,j)
holds |.m-i.|+|.k-j.|=1 by A1,GOBOARD1:def 9;
then
for n st n in dom(<*p*>^f) & n+1 in dom(<*p*>^f) holds for m,k,i,j st [
m,k] in Indices G & [i,j] in Indices G & (<*p*>^f)/.n =G*(m,k) & (<*p*>^f)/.(n+
1)=G*(i,j) holds |.m-i.|+|.k-j.|=1 by A16,A4,GOBOARD1:24;
hence thesis by A7,GOBOARD1:def 9;
end;
theorem Th12:
for C being connected compact non vertical non horizontal Subset
of TOP-REAL 2 for n being Nat holds Lower_Seq(C,n) is_sequence_on
Gauge(C,n)
proof
let C be connected compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
consider j such that
A1: 1 <= j & j <= width Gauge(C,n) and
A2: E-max L~Cage(C,n)=Gauge(C,n)*(len Gauge(C,n),j) by JORDAN1D:25;
set E1 = ((Rotate(Cage(C,n),W-min L~Cage(C,n))/^ (E-max L~Cage(C,n))..Rotate
(Cage(C,n),W-min L~Cage(C,n))))/.1;
set i = len Gauge(C,n);
A3: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by JORDAN1E:def 2
.= <*E-max L~Cage(C,n)*>^(Rotate(Cage(C,n),W-min L~Cage(C,n))/^ (E-max
L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))) by FINSEQ_5:def 2;
A4: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then Rotate(Cage(C,n),W-min L~Cage(C,n)) is_sequence_on Gauge(C,n) by
REVROT_1:34;
then
A5: (Rotate(Cage(C,n),W-min L~Cage(C,n))/^ (E-max L~Cage(C,n))..Rotate(Cage(
C,n),W-min L~Cage(C,n))) is_sequence_on Gauge(C,n) by JORDAN8:2;
A6: for i1,j1,i2,j2 st [i1,j1] in Indices Gauge(C,n) & [i2,j2] in Indices
Gauge(C,n) & E-max L~Cage(C,n) = Gauge(C,n)*(i1,j1) & E1 = Gauge(C,n)*(i2,j2)
holds |.i2-i1.|+|.j2-j1.| = 1
proof
set en = (E-max L~Cage(C,n))..Cage(C,n);
let i1,j1,i2,j2;
assume
A7: [i1,j1] in Indices Gauge(C,n) & [i2,j2] in Indices Gauge(C,n) &
E-max L~Cage(C,n) = Gauge(C,n)*(i1,j1) & E1 = Gauge(C,n)*(i2,j2);
en < len Cage(C,n) by SPRECT_5:16;
then 1<=en+1 & en+1 <= len Cage(C,n) by NAT_1:11,13;
then
A8: en+1 in dom Cage(C,n) by FINSEQ_3:25;
A9: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
A10: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n) by
SPRECT_2:71;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n) by A10
,SPRECT_2:72,XXREAL_0:2;
then (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n) by A10
,SPRECT_2:73,XXREAL_0:2;
then
A11: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n) by A10,
SPRECT_2:74,XXREAL_0:2;
then
A12: (E-max L~Cage(C,n))..Cage(C,n)+1 <= (W-min L~Cage(C,n))..Cage(C,n) by
NAT_1:13;
A13: len Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n) > 0 by SPRECT_5:20
,XREAL_1:50;
then
A14: ((E-max L~Cage(C,n))..Cage(C,n) + 1 + (len Cage(C,n) - (W-min L~Cage(
C,n))..Cage(C,n))) >= 0+0;
A15: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then 1 <= (E-max L~Cage(C,n))..Cage(C,n) by FINSEQ_4:21;
then
A16: 1 < (E-max L~Cage(C,n))..Cage(C,n)+1 by NAT_1:13;
E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by A15,
FINSEQ_6:90,SPRECT_2:43;
then
A17: (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= len
Rotate( Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_4:21;
now
assume (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) = len
(Rotate(Cage(C,n),W-min L~Cage(C,n)));
then
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) = len Cage
(C,n) by FINSEQ_6:179;
then len Upper_Seq(C,n) = len Cage(C,n) by JORDAN1E:8;
then len Cage(C,n) + len Lower_Seq(C,n) = len Cage(C,n)+1 by JORDAN1E:10;
hence contradiction by JORDAN1E:15;
end;
then (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) < len (
Rotate(Cage(C,n),W-min L~Cage(C,n))) by A17,XXREAL_0:1;
then
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) + 1 <= len (
Rotate(Cage(C,n),W-min L~Cage(C,n))) by NAT_1:13;
then
1 + (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) - (E-max
L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= len (Rotate(Cage(C,n),
W-min L~Cage(C,n))) - (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))
by XREAL_1:9;
then
1 <= len (Rotate(Cage(C,n),W-min L~Cage(C,n))/^ (E-max L~Cage(C,n))..
Rotate(Cage(C,n),W-min L~Cage(C,n))) by A17,RFINSEQ:def 1;
then
1 in dom (Rotate(Cage(C,n),W-min L~Cage(C,n))/^ (E-max L~Cage(C,n))..
Rotate(Cage(C,n),W-min L~Cage(C,n))) by FINSEQ_3:25;
then E1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..
Rotate(Cage(C,n),W-min L~Cage(C,n))+1) by FINSEQ_5:27
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. (len Cage(C,n) + (E-max L~
Cage(C,n))..Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n)+1) by A15,A9,A11,
SPRECT_5:9
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+ (len Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n))+1)
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+ (len Cage(C,n) -' (W-min L~Cage(C,n))..Cage(C,n))+1) by A13,XREAL_0:def 2
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+1+ (len Cage(C,n) -'(W-min L~Cage(C,n))..Cage(C,n)))
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+1+ (len Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n))) by A13,XREAL_0:def 2
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+1+ len Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n))
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. ((E-max L~Cage(C,n))..Cage(C,
n)+1+ len Cage(C,n) -' (W-min L~Cage(C,n))..Cage(C,n)) by A14,XREAL_0:def 2;
then
A18: E1=Cage(C,n)/.(en+1) by A9,A16,A12,FINSEQ_6:178;
E-max L~Cage(C,n)=Cage(C,n)/.en & en in dom Cage(C,n) by A15,FINSEQ_4:20
,FINSEQ_5:38;
then |.i1-i2.|+|.j1-j2.| = 1 by A4,A7,A8,A18,GOBOARD1:def 9;
then |.i1-i2.|+|.j2-j1.| = 1 by UNIFORM1:11;
hence thesis by UNIFORM1:11;
end;
i >=4 by JORDAN8:10;
then 1<=i by XXREAL_0:2;
then [i,j] in Indices Gauge(C,n) by A1,MATRIX_0:30;
hence thesis by A5,A2,A6,A3,Th11;
end;
theorem
p`1 = (W-bound C + E-bound C)/2 & p`2 = lower_bound(proj2.:(LSeg(Gauge(C,1)*(
Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\
Upper_Arc L~Cage(C,i+1))) implies ex j st 1 <= j & j <= width Gauge(C,i+1) & p
= Gauge(C,i+1)*(Center Gauge(C,i+1),j)
proof
assume that
A1: p`1 = (W-bound C + E-bound C)/2 and
A2: p`2 = lower_bound(proj2.:(LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*
(Center Gauge(C,1),width Gauge(C,1))) /\ Upper_Arc L~Cage(C,i+1)));
per cases by Th9;
suppose
A3: L~Upper_Seq(C,i+1) = Upper_Arc L~Cage(C,i+1) & L~Lower_Seq(C,i+1)
= Lower_Arc L~Cage(C,i+1);
A4: 1 <= Center Gauge(C,1) by JORDAN1B:11;
set k = width Gauge(C,i+1);
set l = Center Gauge(C,i+1);
set G = Gauge(C,i+1);
set f = Upper_Seq (C,i+1);
A5: 1 <= l by JORDAN1B:11;
A6: width Gauge(C,i+1) = len Gauge(C,i+1) by JORDAN8:def 1;
then k >= 4 by JORDAN8:10;
then
A7: 1 <= k by XXREAL_0:2;
then
A8: l <= len G by A6,JORDAN1B:12;
then
A9: [l,1] in Indices G & [l,k] in Indices G by A7,A5,MATRIX_0:30;
A10: width Gauge(C,1) = len Gauge(C,1) by JORDAN8:def 1;
then width Gauge(C,1) >= 4 by JORDAN8:10;
then
A11: 1 <= width Gauge(C,1) by XXREAL_0:2;
then
A12: Center Gauge(C,1) <= len Gauge(C,1) by A10,JORDAN1B:12;
A13: LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))) /\ L~f c= LSeg(G*(l,1),G*(l,k)) /\ L~f
proof
let a be object;
A14: Upper_Arc L~Cage(C,i+1) c= L~Cage(C,i+1) by JORDAN6:61;
assume
A15: a in LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center
Gauge(C,1),width Gauge(C,1))) /\ L~f;
then reconsider a1=a as Point of TOP-REAL 2;
A16: a1 in LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center
Gauge(C,1),width Gauge(C,1))) by A15,XBOOLE_0:def 4;
a1 in Upper_Arc L~Cage(C,i+1) by A3,A15,XBOOLE_0:def 4;
then
A17: a1`2 <= N-bound L~Cage(C,i+1) by A14,PSCOMP_1:24;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A6,A7,A5,JORDAN1A:20
,JORDAN1B:12;
then
A18: a1`2 <= G*(l,k)`2 by A17,XXREAL_0:2;
a1 in Upper_Arc L~Cage(C,i+1) by A3,A15,XBOOLE_0:def 4;
then
A19: a1`2 >= S-bound L~Cage(C,i+1) by A14,PSCOMP_1:24;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A6,A7,A5,JORDAN1A:22
,JORDAN1B:12;
then
A20: a1`2 >= G*(l,1)`2 by A19,XXREAL_0:2;
A21: a1 in L~f by A15,XBOOLE_0:def 4;
Gauge(C,1)*(Center Gauge(C,1),1)`1 = Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))`1 by A11,A12,A4,GOBOARD5:2;
then
A22: a1`1 = Gauge(C,1)*(Center Gauge(C,1),1)`1 by A16,GOBOARD7:5
.= G*(l,1)`1 by A6,A10,A7,A11,JORDAN1A:36;
then a1`1 = G*(l,k)`1 by A7,A8,A5,GOBOARD5:2;
then a1 in LSeg(G*(l,1),G*(l,k)) by A22,A20,A18,GOBOARD7:7;
hence thesis by A21,XBOOLE_0:def 4;
end;
1 <= i+1 by NAT_1:11;
then
LSeg(G*(l,1),G*(l,k)) /\ L~f c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1)
, Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\ L~f by A6,A10,JORDAN1A:44
,XBOOLE_1:26;
then
A23: LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))) /\ L~f = LSeg(G*(l,1),G*(l,k)) /\ L~f by A13,
XBOOLE_0:def 10;
LSeg(G*(l,1),G*(l,k)) meets L~f by A3,A6,A7,A5,JORDAN1B:12,29;
then consider n such that
A24: 1 <= n & n <= k and
A25: G*(l,n)`2 = lower_bound(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f))
by A7,A9,Th1,Th10;
take n;
thus 1 <= n & n <= width Gauge(C,i+1) by A24;
len Gauge(C,1) >= 4 by JORDAN8:10;
then
A26: 1 <= len Gauge(C,1) by XXREAL_0:2;
then p`1 = (Gauge(C,1)*(Center Gauge(C,1),1))`1 by A1,JORDAN1A:38
.= Gauge(C,i+1)*(Center Gauge(C,i+1),n)`1 by A6,A24,A26,JORDAN1A:36;
hence thesis by A2,A3,A25,A23,TOPREAL3:6;
end;
suppose
A27: L~Upper_Seq(C,i+1) = Lower_Arc L~Cage(C,i+1) & L~Lower_Seq(C,i+1)
= Upper_Arc L~Cage(C,i+1);
A28: 1 <= Center Gauge(C,1) by JORDAN1B:11;
set k = width Gauge(C,i+1);
set l = Center Gauge(C,i+1);
set G = Gauge(C,i+1);
set f = Lower_Seq (C,i+1);
A29: 1 <= l by JORDAN1B:11;
A30: width Gauge(C,i+1) = len Gauge(C,i+1) by JORDAN8:def 1;
then k >= 4 by JORDAN8:10;
then
A31: 1 <= k by XXREAL_0:2;
then
A32: l <= len G by A30,JORDAN1B:12;
then
A33: [l,1] in Indices G & [l,k] in Indices G by A31,A29,MATRIX_0:30;
A34: width Gauge(C,1) = len Gauge(C,1) by JORDAN8:def 1;
then width Gauge(C,1) >= 4 by JORDAN8:10;
then
A35: 1 <= width Gauge(C,1) by XXREAL_0:2;
then
A36: Center Gauge(C,1) <= len Gauge(C,1) by A34,JORDAN1B:12;
A37: LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))) /\ L~f c= LSeg(G*(l,1),G*(l,k)) /\ L~f
proof
let a be object;
A38: Upper_Arc L~Cage(C,i+1) c= L~Cage(C,i+1) by JORDAN6:61;
assume
A39: a in LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center
Gauge(C,1),width Gauge(C,1))) /\ L~f;
then reconsider a1=a as Point of TOP-REAL 2;
A40: a1 in LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center
Gauge(C,1),width Gauge(C,1))) by A39,XBOOLE_0:def 4;
a1 in Upper_Arc L~Cage(C,i+1) by A27,A39,XBOOLE_0:def 4;
then
A41: a1`2 <= N-bound L~Cage(C,i+1) by A38,PSCOMP_1:24;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A30,A31,A29,JORDAN1A:20
,JORDAN1B:12;
then
A42: a1`2 <= G*(l,k)`2 by A41,XXREAL_0:2;
a1 in Upper_Arc L~Cage(C,i+1) by A27,A39,XBOOLE_0:def 4;
then
A43: a1`2 >= S-bound L~Cage(C,i+1) by A38,PSCOMP_1:24;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A30,A31,A29,JORDAN1A:22
,JORDAN1B:12;
then
A44: a1`2 >= G*(l,1)`2 by A43,XXREAL_0:2;
A45: a1 in L~f by A39,XBOOLE_0:def 4;
Gauge(C,1)*(Center Gauge(C,1),1)`1 = Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))`1 by A35,A36,A28,GOBOARD5:2;
then
A46: a1`1 = Gauge(C,1)*(Center Gauge(C,1),1)`1 by A40,GOBOARD7:5
.= G*(l,1)`1 by A30,A34,A31,A35,JORDAN1A:36;
then a1`1 = G*(l,k)`1 by A31,A32,A29,GOBOARD5:2;
then a1 in LSeg(G*(l,1),G*(l,k)) by A46,A44,A42,GOBOARD7:7;
hence thesis by A45,XBOOLE_0:def 4;
end;
1 <= i+1 by NAT_1:11;
then
LSeg(G*(l,1),G*(l,k)) /\ L~f c= LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\ L~f by A30,A34,
JORDAN1A:44,XBOOLE_1:26;
then
A47: LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),
width Gauge(C,1))) /\ L~f = LSeg(G*(l,1),G*(l,k)) /\ L~f by A37,
XBOOLE_0:def 10;
LSeg(G*(l,1),G*(l,k)) meets L~f by A27,A30,A31,A29,JORDAN1B:12,29;
then consider n such that
A48: 1 <= n & n <= k and
A49: G*(l,n)`2 = lower_bound(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f))
by A31,A33,Th1,Th12;
take n;
thus 1 <= n & n <= width Gauge(C,i+1) by A48;
len Gauge(C,1) >= 4 by JORDAN8:10;
then
A50: 1 <= len Gauge(C,1) by XXREAL_0:2;
then p`1 = (Gauge(C,1)*(Center Gauge(C,1),1))`1 by A1,JORDAN1A:38
.= Gauge(C,i+1)*(Center Gauge(C,i+1),n)`1 by A30,A48,A50,JORDAN1A:36;
hence thesis by A2,A27,A49,A47,TOPREAL3:6;
end;
end;