Copyright (c) 2001 Association of Mizar Users
environ
vocabulary FINSEQ_1, EUCLID, GOBOARD1, TOPREAL1, BOOLE, MATRIX_1, MCART_1,
ORDINAL2, FUNCT_5, RELAT_1, REALSET1, SUBSET_1, PSCOMP_1, COMPTS_1,
PRE_TOPC, TARSKI, FINSEQ_4, TREES_1, ARYTM_1, ABSVALUE, SPPOL_1,
JORDAN1E, JORDAN9, FINSEQ_6, FINSEQ_5, JORDAN6, TOPREAL2, RELAT_2,
JORDAN8, FUNCT_1, RFINSEQ, ARYTM_3, JORDAN1A;
notation TARSKI, XBOOLE_0, XCMPLX_0, XREAL_0, NAT_1, ABSVALUE, RELAT_1,
FUNCT_1, BINARITH, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQ_6,
MATRIX_1, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, RFINSEQ, EUCLID,
TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8,
JORDAN9, JORDAN1A, JORDAN1E;
constructors TOPREAL2, FINSEQ_4, REALSET1, GOBOARD9, GOBRD13, PSCOMP_1,
CONNSP_1, GROUP_1, REAL_1, JORDAN6, JORDAN9, JORDAN5C, JORDAN1E,
JORDAN1A, JORDAN8, CARD_4, BINARITH, RFINSEQ;
clusters RELSET_1, SPRECT_1, SPRECT_3, TOPREAL6, XREAL_0, PSCOMP_1, REVROT_1,
JORDAN1A, JORDAN1E, JORDAN8, NAT_1, MEMBERED;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, JORDAN8, REAL_1, 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, EXTENS_1, JORDAN1A, REVROT_1, JORDAN9, JORDAN1B, FINSEQ_3,
UNIFORM1, FINSEQ_4, GROUP_5, JORDAN1D, SPRECT_5, RFINSEQ, BINARITH,
XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1;
begin
reserve i,j,k,m,n,l 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 = inf(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 & [i,k] in Indices G and
A4: j <= k;
proj2.:X = (proj2|X).:X by EXTENS_1:1
.= (proj2||X).:X by PSCOMP_1:def 26;
then A5: inf(proj2.:X) = inf((proj2||X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def
10
.= inf((proj2||X).: the carrier of ((TOP-REAL 2)|X)) by PRE_TOPC:12
.= inf(proj2||X) by PSCOMP_1:def 20
.= S-bound X by PSCOMP_1:def 33;
ex x being set 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 PSCOMP_1:
64,XBOOLE_0:def 3;
consider p being set such that
A6: p in S-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A6;
A7: p`2 = (S-min X)`2 by A6,PSCOMP_1:118
.= inf(proj2.:X) by A5,PSCOMP_1:114;
p in LSeg(SW-corner X, SE-corner X)/\X by A6,PSCOMP_1:def 41;
then A8: p in X by XBOOLE_0:def 3;
then p in L~f by XBOOLE_0:def 3;
then p in union { LSeg(f,k1) where k1 is Nat :
1 <= k1 & k1+1 <= len f} by TOPREAL1:def 6;
then consider Y being set such that
A9: p in Y and
A10: 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
A11: Y = LSeg(f,i1) and
A12: 1 <= i1 and
A13: i1+1 <= len f by A10;
A14: p in LSeg(f/.i1,f/.(i1+1)) by A9,A11,A12,A13,TOPREAL1:def 5;
i1 <= len f by A13,NAT_1:38;
then i1 in Seg len f by A12,FINSEQ_1:3;
then A15: i1 in dom f by FINSEQ_1:def 3;
then A16: f is special by A1,JORDAN8:7,RELAT_1:60;
1 < i1+1 by A12,NAT_1:38;
then i1+1 in Seg len f by A13,FINSEQ_1:3;
then A17: i1+1 in dom f by FINSEQ_1:def 3;
consider i0,j0 being Nat such that
A18: [i0,j0] in Indices G & f/.i1 = G*(i0,j0) by A1,A15,GOBOARD1:def 11;
consider io,jo being Nat such that
A19: [io,jo] in Indices G & f/.(i1+1) = G*(io,jo) by A1,A17,GOBOARD1:def 11;
A20: 1 <= i & i <= len G & 1 <= j & j <= width G by A3,GOBOARD5:1;
A21: 1 <= i & i <= len G & 1 <= k & k <= width G by A3,GOBOARD5:1;
A22: 1 <= i0 & i0 <= len G & 1 <= j0 & j0 <= width G by A18,GOBOARD5:1;
A23: 1 <= io & io <= len G & 1 <= jo & jo <= width G by A19,GOBOARD5:1;
A24: G*(i,j)`1 = G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,k)`1 by A21,GOBOARD5:3;
A25: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A26: G*(i,j)`2 <= p`2 & p`2 <= G*(i,k)`2 by A25,TOPREAL1:10;
ex n st j <= n & n <= k & G*(i,n) = p
proof
per cases by A12,A13,A16,TOPREAL1:def 7;
suppose A27: (f/.i1)`1 = (f/.(i1+1))`1;
G*(i0,j)`1 = G*(i0,1)`1 by A20,A22,GOBOARD5:3
.= G*(i0,j0)`1 by A22,GOBOARD5:3
.= p`1 by A14,A18,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
then A28: i0<=i & i0>=i by A20,A22,GOBOARD5:4;
then A29: i=i0 by AXIOMS:21;
G*(io,j)`1 = G*(io,1)`1 by A20,A23,GOBOARD5:3
.= G*(io,jo)`1 by A23,GOBOARD5:3
.= p`1 by A14,A19,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
then A30: io<=i & io>=i by A20,A23,GOBOARD5:4;
then A31: i=io by AXIOMS:21;
thus thesis
proof
per cases;
suppose A32: (f/.i1)`2 <= (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose A33: (f/.i1) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.i1 in L~f by A15,GOBOARD1:16;
then f/.i1 in X1 by A33,XBOOLE_0:def 3;
then A34: p`2 <= (f/.i1)`2 by A5,A7,PSCOMP_1:71;
p`2 >= (f/.i1)`2 by A14,A32,TOPREAL1:10;
then A35: p`2 = (f/.i1)`2 by A34,AXIOMS:21;
take n=j0;
A36: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
then A37: p`1 = G*(i,j)`1 by A24,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
A38: p`2 = G*(1,j0)`2 by A18,A22,A35,GOBOARD5:2
.= G*(i,n)`2 by A20,A22,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A39: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A36,A38,
TOPREAL1:10;
hence j <= n by A20,A22,GOBOARD5:5;
thus n <= k by A21,A22,A39,GOBOARD5:5;
thus thesis by A37,A38,TOPREAL3:11;
suppose A40: not f/.i1 in LSeg(G*(i,j),G*(i,k));
A41: (f/.i1)`1 = p`1 by A14,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
thus thesis
proof
per cases by A24,A40,A41,GOBOARD7:8;
suppose A42: (f/.i1)`2 < G*(i,j)`2;
then A43: G*(i,j0)`2 < G*(i,j)`2 by A18,A28,AXIOMS:21;
j0<=j by A18,A20,A22,A29,A42,GOBOARD5:5;
then A44: j0<j by A43,AXIOMS:21;
j0<=jo+0 by A18,A19,A22,A23,A29,A31,A32,GOBOARD5:5;
then j0-jo <= 0 by REAL_1:86;
then -(j0-jo) >= -0 by REAL_1:50;
then A45: jo-j0 >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0) + abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then abs(-(j0-jo)) = 1 by ABSVALUE:17;
then abs(jo-j0) = 1 by XCMPLX_1:143;
then jo-j0 = 1 by A45,ABSVALUE:def 1;
then j0+jo-j0 = j0+1 by XCMPLX_1:29;
then jo+(j0-j0) = j0+1 by XCMPLX_1:29;
then j0+1=jo+0 by XCMPLX_1:14;
then A46: jo<=j by A44,NAT_1:38;
p`2 <= G*(io,jo)`2 by A14,A19,A32,TOPREAL1:10;
then p`2 <= G*(1,jo)`2 by A23,GOBOARD5:2;
then p`2 <= G*(i,jo)`2 by A20,A23,GOBOARD5:2;
then G*(i,j)`2 <= G*(i,jo)`2 by A26,AXIOMS:22;
then j<=jo by A20,A23,GOBOARD5:5;
then A47: j=jo by A46,AXIOMS:21;
take n=jo;
A48: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A23,GOBOARD5:3;
p`2 <= G*(io,jo)`2 by A14,A19,A32,TOPREAL1:10;
then p`2 <= G*(1,jo)`2 by A23,GOBOARD5:2;
then p`2 <= G*(i,jo)`2 by A20,A23,GOBOARD5:2;
then p`2 = G*(i,j)`2 by A26,A47,AXIOMS:21;
hence thesis by A4,A47,A48,TOPREAL3:11;
suppose A49: (f/.i1)`2 > G*(i,k)`2;
p`2 >= (f/.i1)`2 by A14,A32,TOPREAL1:10;
hence thesis by A26,A49,AXIOMS:22;
end;
end;
suppose A50: (f/.i1)`2 > (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose A51: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.(i1+1) in L~f by A17,GOBOARD1:16;
then f/.(i1+1) in X1 by A51,XBOOLE_0:def 3;
then A52: p`2 <= (f/.(i1+1))`2 by A5,A7,PSCOMP_1:71;
p`2 >= (f/.(i1+1))`2 by A14,A50,TOPREAL1:10;
then A53: p`2 = (f/.(i1+1))`2 by A52,AXIOMS:21;
take n=jo;
A54: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
then A55: p`1 = G*(i,j)`1 by A24,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A23,GOBOARD5:3;
A56: p`2 = G*(1,jo)`2 by A19,A23,A53,GOBOARD5:2
.= G*(i,n)`2 by A20,A23,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A57: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A54,A56,
TOPREAL1:10;
hence j <= n by A20,A23,GOBOARD5:5;
thus n <= k by A21,A23,A57,GOBOARD5:5;
thus thesis by A55,A56,TOPREAL3:11;
suppose A58: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k));
A59: (f/.(i1+1))`1 = p`1 by A14,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
thus thesis
proof
per cases by A24,A58,A59,GOBOARD7:8;
suppose A60: (f/.(i1+1))`2 < G*(i,j)`2;
then A61: G*(i,jo)`2 < G*(i,j)`2 by A19,A30,AXIOMS:21;
jo<=j by A19,A20,A23,A31,A60,GOBOARD5:5;
then A62: jo<j by A61,AXIOMS:21;
jo<=j0+0 by A18,A19,A22,A23,A29,A31,A50,GOBOARD5:5;
then jo-j0 <= 0 by REAL_1:86;
then -(jo-j0) >= -0 by REAL_1:50;
then A63: j0-jo >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then j0-jo = 1 by A63,ABSVALUE:def 1;
then j0-(jo-jo) = jo+1 by XCMPLX_1:37;
then jo+1=j0-0 by XCMPLX_1:14;
then A64: j0<=j by A62,NAT_1:38;
p`2 <= G*(i0,j0)`2 by A14,A18,A50,TOPREAL1:10;
then p`2 <= G*(1,j0)`2 by A22,GOBOARD5:2;
then p`2 <= G*(i,j0)`2 by A20,A22,GOBOARD5:2;
then G*(i,j)`2 <= G*(i,j0)`2 by A26,AXIOMS:22;
then j<=j0 by A20,A22,GOBOARD5:5;
then A65: j=j0 by A64,AXIOMS:21;
take n=j0;
A66: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
p`2 <= G*(i0,j0)`2 by A14,A18,A50,TOPREAL1:10;
then p`2 <= G*(1,j0)`2 by A22,GOBOARD5:2;
then p`2 <= G*(i,j0)`2 by A20,A22,GOBOARD5:2;
then p`2 = G*(i,j)`2 by A26,A65,AXIOMS:21;
hence thesis by A4,A65,A66,TOPREAL3:11;
suppose A67: (f/.(i1+1))`2 > G*(i,k)`2;
p`2 >= (f/.(i1+1))`2 by A14,A50,TOPREAL1:10;
hence thesis by A26,A67,AXIOMS:22;
end;
end;
end;
suppose (f/.i1)`2 = (f/.(i1+1))`2;
then A68: p`2 = (f/.i1)`2 by A14,GOBOARD7:6;
take n=j0;
A69: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
A70: p`2 = G*(1,j0)`2 by A18,A22,A68,GOBOARD5:2
.= G*(i,n)`2 by A20,A22,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A71: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A25,A70,TOPREAL1:
10;
hence j <= n by A20,A22,GOBOARD5:5;
thus n <= k by A21,A22,A71,GOBOARD5:5;
thus thesis by A69,A70,TOPREAL3:11;
end;
hence ex n st j <= n & n <= k & G*(i,n)`2 = inf(proj2.:X) by A7;
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 = sup(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 & [i,k] in Indices G and
A4: j <= k;
proj2.:X = (proj2|X).:X by EXTENS_1:1
.= (proj2||X).:X by PSCOMP_1:def 26;
then A5: sup(proj2.:X) = sup((proj2||X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def
10
.= sup((proj2||X).: the carrier of ((TOP-REAL 2)|X)) by PRE_TOPC:12
.= sup(proj2||X) by PSCOMP_1:def 21
.= N-bound X by PSCOMP_1:def 31;
ex x being set 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 PSCOMP_1:
64,XBOOLE_0:def 3;
consider p being set such that
A6: p in N-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A6;
A7: p`2 = (N-min X)`2 by A6,PSCOMP_1:98
.= sup(proj2.:X) by A5,PSCOMP_1:94;
p in LSeg(NW-corner X, NE-corner X)/\X by A6,PSCOMP_1:def 39;
then A8: p in X by XBOOLE_0:def 3;
then p in L~f by XBOOLE_0:def 3;
then p in union { LSeg(f,k1) where k1 is Nat :
1 <= k1 & k1+1 <= len f} by TOPREAL1:def 6;
then consider Y being set such that
A9: p in Y and
A10: 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
A11: Y = LSeg(f,i1) and
A12: 1 <= i1 and
A13: i1+1 <= len f by A10;
A14: p in LSeg(f/.i1,f/.(i1+1)) by A9,A11,A12,A13,TOPREAL1:def 5;
i1 <= len f by A13,NAT_1:38;
then i1 in Seg len f by A12,FINSEQ_1:3;
then A15: i1 in dom f by FINSEQ_1:def 3;
then A16: f is special by A1,JORDAN8:7,RELAT_1:60;
1 < i1+1 by A12,NAT_1:38;
then i1+1 in Seg len f by A13,FINSEQ_1:3;
then A17: i1+1 in dom f by FINSEQ_1:def 3;
consider i0,j0 being Nat such that
A18: [i0,j0] in Indices G & f/.i1 = G*(i0,j0) by A1,A15,GOBOARD1:def 11;
consider io,jo being Nat such that
A19: [io,jo] in Indices G & f/.(i1+1) = G*(io,jo) by A1,A17,GOBOARD1:def 11;
A20: 1 <= i & i <= len G & 1 <= j & j <= width G by A3,GOBOARD5:1;
A21: 1 <= i & i <= len G & 1 <= k & k <= width G by A3,GOBOARD5:1;
A22: 1 <= i0 & i0 <= len G & 1 <= j0 & j0 <= width G by A18,GOBOARD5:1;
A23: 1 <= io & io <= len G & 1 <= jo & jo <= width G by A19,GOBOARD5:1;
A24: G*(i,j)`1 = G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,k)`1 by A21,GOBOARD5:3;
A25: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A26: G*(i,j)`2 <= p`2 & p`2 <= G*(i,k)`2 by A25,TOPREAL1:10;
ex n st j <= n & n <= k & G*(i,n) = p
proof
per cases by A12,A13,A16,TOPREAL1:def 7;
suppose A27: (f/.i1)`1 = (f/.(i1+1))`1;
G*(i0,j)`1 = G*(i0,1)`1 by A20,A22,GOBOARD5:3
.= G*(i0,j0)`1 by A22,GOBOARD5:3
.= p`1 by A14,A18,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
then A28: i0<=i & i0>=i by A20,A22,GOBOARD5:4;
then A29: i=i0 by AXIOMS:21;
G*(io,j)`1 = G*(io,1)`1 by A20,A23,GOBOARD5:3
.= G*(io,jo)`1 by A23,GOBOARD5:3
.= p`1 by A14,A19,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
then A30: io<=i & io>=i by A20,A23,GOBOARD5:4;
then A31: i=io by AXIOMS:21;
thus thesis
proof
per cases;
suppose A32: (f/.i1)`2 <= (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose A33: (f/.(i1+1)) in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.(i1+1) in L~f by A17,GOBOARD1:16;
then f/.(i1+1) in X1 by A33,XBOOLE_0:def 3;
then A34: p`2 >= (f/.(i1+1))`2 by A5,A7,PSCOMP_1:71;
p`2 <= (f/.(i1+1))`2 by A14,A32,TOPREAL1:10;
then A35: p`2 = (f/.(i1+1))`2 by A34,AXIOMS:21;
take n=jo;
A36: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
then A37: p`1 = G*(i,j)`1 by A24,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A23,GOBOARD5:3;
A38: p`2 = G*(1,jo)`2 by A19,A23,A35,GOBOARD5:2
.= G*(i,n)`2 by A20,A23,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A39: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A36,A38,
TOPREAL1:10;
hence j <= n by A20,A23,GOBOARD5:5;
thus n <= k by A21,A23,A39,GOBOARD5:5;
thus thesis by A37,A38,TOPREAL3:11;
suppose A40: not f/.(i1+1) in LSeg(G*(i,j),G*(i,k));
A41: (f/.(i1+1))`1 = p`1 by A14,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
thus thesis
proof
per cases by A24,A40,A41,GOBOARD7:8;
suppose A42: (f/.(i1+1))`2 > G*(i,k)`2;
then A43: G*(i,jo)`2 > G*(i,k)`2 by A19,A30,AXIOMS:21;
jo>=k by A19,A21,A23,A31,A42,GOBOARD5:5;
then A44: jo>k by A43,AXIOMS:21;
j0<=jo+0 by A18,A19,A22,A23,A29,A31,A32,GOBOARD5:5;
then j0-jo <= 0 by REAL_1:86;
then -(j0-jo) >= -0 by REAL_1:50;
then A45: jo-j0 >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then abs(-(j0-jo)) = 1 by ABSVALUE:17;
then abs(jo-j0) = 1 by XCMPLX_1:143;
then jo-j0 = 1 by A45,ABSVALUE:def 1;
then j0+jo-j0 = j0+1 by XCMPLX_1:29;
then jo+(j0-j0) = j0+1 by XCMPLX_1:29;
then j0+1=jo+0 by XCMPLX_1:14;
then A46: j0>=k by A44,NAT_1:38;
p`2 >= G*(i0,j0)`2 by A14,A18,A32,TOPREAL1:10;
then p`2 >= G*(1,j0)`2 by A22,GOBOARD5:2;
then p`2 >= G*(i,j0)`2 by A20,A22,GOBOARD5:2;
then G*(i,k)`2 >= G*(i,j0)`2 by A26,AXIOMS:22;
then k>=j0 by A21,A22,GOBOARD5:5;
then A47: k=j0 by A46,AXIOMS:21;
take n=j0;
A48: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
p`2 >= G*(i0,j0)`2 by A14,A18,A32,TOPREAL1:10;
then p`2 >= G*(1,j0)`2 by A22,GOBOARD5:2;
then p`2 >= G*(i,j0)`2 by A20,A22,GOBOARD5:2;
then p`2 = G*(i,k)`2 by A26,A47,AXIOMS:21;
hence thesis by A4,A47,A48,TOPREAL3:11;
suppose A49: (f/.(i1+1))`2 < G*(i,j)`2;
p`2 <= (f/.(i1+1))`2 by A14,A32,TOPREAL1:10;
hence thesis by A26,A49,AXIOMS:22;
end;
end;
suppose A50: (f/.i1)`2 > (f/.(i1+1))`2;
thus thesis
proof
per cases;
suppose A51: f/.i1 in LSeg(G*(i,j),G*(i,k));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.i1 in L~f by A15,GOBOARD1:16;
then f/.i1 in X1 by A51,XBOOLE_0:def 3;
then A52: p`2 >= (f/.i1)`2 by A5,A7,PSCOMP_1:71;
p`2 <= (f/.i1)`2 by A14,A50,TOPREAL1:10;
then A53: p`2 = (f/.i1)`2 by A52,AXIOMS:21;
take n=j0;
A54: p in LSeg(G*(i,j),G*(i,k)) by A8,XBOOLE_0:def 3;
then A55: p`1 = G*(i,j)`1 by A24,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
A56: p`2 = G*(1,j0)`2 by A18,A22,A53,GOBOARD5:2
.= G*(i,n)`2 by A20,A22,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A57: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A54,A56,
TOPREAL1:10;
hence j <= n by A20,A22,GOBOARD5:5;
thus n <= k by A21,A22,A57,GOBOARD5:5;
thus thesis by A55,A56,TOPREAL3:11;
suppose A58: not f/.i1 in LSeg(G*(i,j),G*(i,k));
A59: (f/.i1)`1 = p`1 by A14,A27,GOBOARD7:5
.= G*(i,j)`1 by A24,A25,GOBOARD7:5;
thus thesis
proof
per cases by A24,A58,A59,GOBOARD7:8;
suppose A60: (f/.i1)`2 > G*(i,k)`2;
then A61: G*(i,j0)`2 > G*(i,k)`2 by A18,A28,AXIOMS:21;
j0>=k by A18,A21,A22,A29,A60,GOBOARD5:5;
then A62: j0>k by A61,AXIOMS:21;
jo<=j0+0 by A18,A19,A22,A23,A29,A31,A50,GOBOARD5:5;
then jo-j0 <= 0 by REAL_1:86;
then -(jo-j0) >= -0 by REAL_1:50;
then A63: j0-jo >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then j0-jo = 1 by A63,ABSVALUE:def 1;
then j0-(jo-jo) = jo+1 by XCMPLX_1:37;
then jo+1=j0-0 by XCMPLX_1:14;
then A64: jo>=k by A62,NAT_1:38;
p`2 >= G*(io,jo)`2 by A14,A19,A50,TOPREAL1:10;
then p`2 >= G*(1,jo)`2 by A23,GOBOARD5:2;
then p`2 >= G*(i,jo)`2 by A20,A23,GOBOARD5:2;
then G*(i,k)`2 >= G*(i,jo)`2 by A26,AXIOMS:22;
then k>=jo by A21,A23,GOBOARD5:5;
then A65: k=jo by A64,AXIOMS:21;
take n=jo;
A66: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A23,GOBOARD5:3;
p`2 >= G*(io,jo)`2 by A14,A19,A50,TOPREAL1:10;
then p`2 >= G*(1,jo)`2 by A23,GOBOARD5:2;
then p`2 >= G*(i,jo)`2 by A20,A23,GOBOARD5:2;
then p`2 = G*(i,k)`2 by A26,A65,AXIOMS:21;
hence thesis by A4,A65,A66,TOPREAL3:11;
suppose A67: (f/.i1)`2 < G*(i,j)`2;
p`2 <= (f/.i1)`2 by A14,A50,TOPREAL1:10;
hence thesis by A26,A67,AXIOMS:22;
end;
end;
end;
suppose (f/.i1)`2 = (f/.(i1+1))`2;
then A68: p`2 = (f/.i1)`2 by A14,GOBOARD7:6;
take n=j0;
A69: p`1 = G*(i,j)`1 by A24,A25,GOBOARD7:5
.= G*(i,1)`1 by A20,GOBOARD5:3
.= G*(i,n)`1 by A20,A22,GOBOARD5:3;
A70: p`2 = G*(1,j0)`2 by A18,A22,A68,GOBOARD5:2
.= G*(i,n)`2 by A20,A22,GOBOARD5:2;
G*(i,j)`2 <= G*(i,k)`2 by A4,A20,A21,SPRECT_3:24;
then A71: G*(i,j)`2 <= G*(i,n)`2 & G*(i,n)`2 <= G*(i,k)`2 by A25,A70,TOPREAL1:
10;
hence j <= n by A20,A22,GOBOARD5:5;
thus n <= k by A21,A22,A71,GOBOARD5:5;
thus thesis by A69,A70,TOPREAL3:11;
end;
hence ex n st j <= n & n <= k & G*(i,n)`2 = sup(proj2.:X) by A7;
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 = inf(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 & [k,i] in Indices G and
A4: j <= k;
proj1.:X = (proj1|X).:X by EXTENS_1:1
.= (proj1||X).:X by PSCOMP_1:def 26;
then A5: inf(proj1.:X) = inf((proj1||X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def
10
.= inf((proj1||X).: the carrier of ((TOP-REAL 2)|X)) by PRE_TOPC:12
.= inf(proj1||X) by PSCOMP_1:def 20
.= W-bound X by PSCOMP_1:def 30;
ex x being set 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 PSCOMP_1:
64,XBOOLE_0:def 3;
consider p being set such that
A6: p in W-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A6;
A7: p`1 = (W-min X)`1 by A6,PSCOMP_1:88
.= inf(proj1.:X) by A5,PSCOMP_1:84;
p in LSeg(SW-corner X, NW-corner X)/\X by A6,PSCOMP_1:def 38;
then A8: p in X by XBOOLE_0:def 3;
then p in L~f by XBOOLE_0:def 3;
then p in union { LSeg(f,k1) where k1 is Nat :
1 <= k1 & k1+1 <= len f} by TOPREAL1:def 6;
then consider Y being set such that
A9: p in Y and
A10: 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
A11: Y = LSeg(f,i1) and
A12: 1 <= i1 and
A13: i1+1 <= len f by A10;
A14: p in LSeg(f/.i1,f/.(i1+1)) by A9,A11,A12,A13,TOPREAL1:def 5;
i1 <= len f by A13,NAT_1:38;
then i1 in Seg len f by A12,FINSEQ_1:3;
then A15: i1 in dom f by FINSEQ_1:def 3;
then A16: f is special by A1,JORDAN8:7,RELAT_1:60;
1 < i1+1 by A12,NAT_1:38;
then i1+1 in Seg len f by A13,FINSEQ_1:3;
then A17: i1+1 in dom f by FINSEQ_1:def 3;
consider j0,i0 being Nat such that
A18: [j0,i0] in Indices G & f/.i1 = G*(j0,i0) by A1,A15,GOBOARD1:def 11;
consider jo,io being Nat such that
A19: [jo,io] in Indices G & f/.(i1+1) = G*(jo,io) by A1,A17,GOBOARD1:def 11;
A20: 1 <= j & j <= len G & 1 <= i & i <= width G by A3,GOBOARD5:1;
A21: 1 <= k & k <= len G & 1 <= i & i <= width G by A3,GOBOARD5:1;
A22: 1 <= j0 & j0 <= len G & 1 <= i0 & i0 <= width G by A18,GOBOARD5:1;
A23: 1 <= jo & jo <= len G & 1 <= io & io <= width G by A19,GOBOARD5:1;
A24: G*(j,i)`2 = G*(1,i)`2 by A20,GOBOARD5:2
.= G*(k,i)`2 by A21,GOBOARD5:2;
A25: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A26: G*(j,i)`1 <= p`1 & p`1 <= G*(k,i)`1 by A25,TOPREAL1:9;
ex n st j <= n & n <= k & G*(n,i) = p
proof
per cases by A12,A13,A16,TOPREAL1:def 7;
suppose A27: (f/.i1)`2 = (f/.(i1+1))`2;
G*(j,i0)`2 = G*(1,i0)`2 by A20,A22,GOBOARD5:2
.= G*(j0,i0)`2 by A22,GOBOARD5:2
.= p`2 by A14,A18,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
then A28: i0<=i & i0>=i by A20,A22,GOBOARD5:5;
then A29: i=i0 by AXIOMS:21;
G*(j,io)`2 = G*(1,io)`2 by A20,A23,GOBOARD5:2
.= G*(jo,io)`2 by A23,GOBOARD5:2
.= p`2 by A14,A19,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
then A30: io<=i & io>=i by A20,A23,GOBOARD5:5;
then A31: i=io by AXIOMS:21;
thus thesis
proof
per cases;
suppose A32: (f/.i1)`1 <= (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose A33: (f/.i1) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.i1 in L~f by A15,GOBOARD1:16;
then f/.i1 in X1 by A33,XBOOLE_0:def 3;
then A34: p`1 <= (f/.i1)`1 by A5,A7,PSCOMP_1:71;
p`1 >= (f/.i1)`1 by A14,A32,TOPREAL1:9;
then A35: p`1 = (f/.i1)`1 by A34,AXIOMS:21;
take n=j0;
A36: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
then A37: p`2 = G*(j,i)`2 by A24,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
A38: p`1 = G*(j0,1)`1 by A18,A22,A35,GOBOARD5:3
.= G*(n,i)`1 by A20,A22,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A39: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A36,A38,
TOPREAL1:9;
hence j <= n by A20,A22,GOBOARD5:4;
thus n <= k by A21,A22,A39,GOBOARD5:4;
thus thesis by A37,A38,TOPREAL3:11;
suppose A40: not f/.i1 in LSeg(G*(j,i),G*(k,i));
A41: (f/.i1)`2 = p`2 by A14,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
thus thesis
proof
per cases by A24,A40,A41,GOBOARD7:9;
suppose A42: (f/.i1)`1 < G*(j,i)`1;
then A43: G*(j0,i)`1 < G*(j,i)`1 by A18,A28,AXIOMS:21;
j0<=j by A18,A20,A22,A29,A42,GOBOARD5:4;
then A44: j0<j by A43,AXIOMS:21;
j0<=jo+0 by A18,A19,A22,A23,A29,A31,A32,GOBOARD5:4;
then j0-jo <= 0 by REAL_1:86;
then -(j0-jo) >= -0 by REAL_1:50;
then A45: jo-j0 >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then abs(-(j0-jo)) = 1 by ABSVALUE:17;
then abs(jo-j0) = 1 by XCMPLX_1:143;
then jo-j0 = 1 by A45,ABSVALUE:def 1;
then j0+jo-j0 = j0+1 by XCMPLX_1:29;
then jo+(j0-j0) = j0+1 by XCMPLX_1:29;
then j0+1=jo+0 by XCMPLX_1:14;
then A46: jo<=j by A44,NAT_1:38;
p`1 <= G*(jo,io)`1 by A14,A19,A32,TOPREAL1:9;
then p`1 <= G*(jo,1)`1 by A23,GOBOARD5:3;
then p`1 <= G*(jo,i)`1 by A20,A23,GOBOARD5:3;
then G*(j,i)`1 <= G*(jo,i)`1 by A26,AXIOMS:22;
then j<=jo by A20,A23,GOBOARD5:4;
then A47: j=jo by A46,AXIOMS:21;
take n=jo;
A48: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A23,GOBOARD5:2;
p`1 <= G*(jo,io)`1 by A14,A19,A32,TOPREAL1:9;
then p`1 <= G*(jo,1)`1 by A23,GOBOARD5:3;
then p`1 <= G*(jo,i)`1 by A20,A23,GOBOARD5:3;
then p`1 = G*(j,i)`1 by A26,A47,AXIOMS:21;
hence thesis by A4,A47,A48,TOPREAL3:11;
suppose A49: (f/.i1)`1 > G*(k,i)`1;
p`1 >= (f/.i1)`1 by A14,A32,TOPREAL1:9;
hence thesis by A26,A49,AXIOMS:22;
end;
end;
suppose A50: (f/.i1)`1 > (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose A51: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.(i1+1) in L~f by A17,GOBOARD1:16;
then f/.(i1+1) in X1 by A51,XBOOLE_0:def 3;
then A52: p`1 <= (f/.(i1+1))`1 by A5,A7,PSCOMP_1:71;
p`1 >= (f/.(i1+1))`1 by A14,A50,TOPREAL1:9;
then A53: p`1 = (f/.(i1+1))`1 by A52,AXIOMS:21;
take n=jo;
A54: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
then A55: p`2 = G*(j,i)`2 by A24,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A23,GOBOARD5:2;
A56: p`1 = G*(jo,1)`1 by A19,A23,A53,GOBOARD5:3
.= G*(n,i)`1 by A20,A23,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A57: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A54,A56,
TOPREAL1:9;
hence j <= n by A20,A23,GOBOARD5:4;
thus n <= k by A21,A23,A57,GOBOARD5:4;
thus thesis by A55,A56,TOPREAL3:11;
suppose A58: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i));
A59: (f/.(i1+1))`2 = p`2 by A14,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
thus thesis
proof
per cases by A24,A58,A59,GOBOARD7:9;
suppose A60: (f/.(i1+1))`1 < G*(j,i)`1;
then A61: G*(jo,i)`1 < G*(j,i)`1 by A19,A30,AXIOMS:21;
jo<=j by A19,A20,A23,A31,A60,GOBOARD5:4;
then A62: jo<j by A61,AXIOMS:21;
jo<=j0+0 by A18,A19,A22,A23,A29,A31,A50,GOBOARD5:4;
then jo-j0 <= 0 by REAL_1:86;
then -(jo-j0) >= -0 by REAL_1:50;
then A63: j0-jo >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then j0-jo = 1 by A63,ABSVALUE:def 1;
then j0-(jo-jo) = jo+1 by XCMPLX_1:37;
then jo+1=j0-0 by XCMPLX_1:14;
then A64: j0<=j by A62,NAT_1:38;
p`1 <= G*(j0,i0)`1 by A14,A18,A50,TOPREAL1:9;
then p`1 <= G*(j0,1)`1 by A22,GOBOARD5:3;
then p`1 <= G*(j0,i)`1 by A20,A22,GOBOARD5:3;
then G*(j,i)`1 <= G*(j0,i)`1 by A26,AXIOMS:22;
then j<=j0 by A20,A22,GOBOARD5:4;
then A65: j=j0 by A64,AXIOMS:21;
take n=j0;
A66: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
p`1 <= G*(j0,i0)`1 by A14,A18,A50,TOPREAL1:9;
then p`1 <= G*(j0,1)`1 by A22,GOBOARD5:3;
then p`1 <= G*(j0,i)`1 by A20,A22,GOBOARD5:3;
then p`1 = G*(j,i)`1 by A26,A65,AXIOMS:21;
hence thesis by A4,A65,A66,TOPREAL3:11;
suppose A67: (f/.(i1+1))`1 > G*(k,i)`1;
p`1 >= (f/.(i1+1))`1 by A14,A50,TOPREAL1:9;
hence thesis by A26,A67,AXIOMS:22;
end;
end;
end;
suppose (f/.i1)`1 = (f/.(i1+1))`1;
then A68: p`1 = (f/.i1)`1 by A14,GOBOARD7:5;
take n=j0;
A69: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
A70: p`1 = G*(j0,1)`1 by A18,A22,A68,GOBOARD5:3
.= G*(n,i)`1 by A20,A22,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A71: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A25,A70,TOPREAL1:
9;
hence j <= n by A20,A22,GOBOARD5:4;
thus n <= k by A21,A22,A71,GOBOARD5:4;
thus thesis by A69,A70,TOPREAL3:11;
end;
hence ex n st j <= n & n <= k & G*(n,i)`1 = inf(proj1.:X) by A7;
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 = sup(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 & [k,i] in Indices G and
A4: j <= k;
proj1.:X = (proj1|X).:X by EXTENS_1:1
.= (proj1||X).:X by PSCOMP_1:def 26;
then A5: sup(proj1.:X) = sup((proj1||X).: [#]((TOP-REAL 2)|X)) by PRE_TOPC:def
10
.= sup((proj1||X).: the carrier of ((TOP-REAL 2)|X)) by PRE_TOPC:12
.= sup(proj1||X) by PSCOMP_1:def 21
.= E-bound X by PSCOMP_1:def 32;
ex x being set 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 PSCOMP_1:
64,XBOOLE_0:def 3;
consider p being set such that
A6: p in E-most X1 by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A6;
A7: p`1 = (E-min X)`1 by A6,PSCOMP_1:108
.= sup(proj1.:X) by A5,PSCOMP_1:104;
p in LSeg(SE-corner X, NE-corner X)/\X by A6,PSCOMP_1:def 40;
then A8: p in X by XBOOLE_0:def 3;
then p in L~f by XBOOLE_0:def 3;
then p in union { LSeg(f,k1) where k1 is Nat :
1 <= k1 & k1+1 <= len f} by TOPREAL1:def 6;
then consider Y being set such that
A9: p in Y and
A10: 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
A11: Y = LSeg(f,i1) and
A12: 1 <= i1 and
A13: i1+1 <= len f by A10;
A14: p in LSeg(f/.i1,f/.(i1+1)) by A9,A11,A12,A13,TOPREAL1:def 5;
i1 <= len f by A13,NAT_1:38;
then i1 in Seg len f by A12,FINSEQ_1:3;
then A15: i1 in dom f by FINSEQ_1:def 3;
then A16: f is special by A1,JORDAN8:7,RELAT_1:60;
1 < i1+1 by A12,NAT_1:38;
then i1+1 in Seg len f by A13,FINSEQ_1:3;
then A17: i1+1 in dom f by FINSEQ_1:def 3;
consider j0,i0 being Nat such that
A18: [j0,i0] in Indices G & f/.i1 = G*(j0,i0) by A1,A15,GOBOARD1:def 11;
consider jo,io being Nat such that
A19: [jo,io] in Indices G & f/.(i1+1) = G*(jo,io) by A1,A17,GOBOARD1:def 11;
A20: 1 <= j & j <= len G & 1 <= i & i <= width G by A3,GOBOARD5:1;
A21: 1 <= k & k <= len G & 1 <= i & i <= width G by A3,GOBOARD5:1;
A22: 1 <= j0 & j0 <= len G & 1 <= i0 & i0 <= width G by A18,GOBOARD5:1;
A23: 1 <= jo & jo <= len G & 1 <= io & io <= width G by A19,GOBOARD5:1;
A24: G*(j,i)`2 = G*(1,i)`2 by A20,GOBOARD5:2
.= G*(k,i)`2 by A21,GOBOARD5:2;
A25: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A26: G*(j,i)`1 <= p`1 & p`1 <= G*(k,i)`1 by A25,TOPREAL1:9;
ex n st j <= n & n <= k & G*(n,i) = p
proof
per cases by A12,A13,A16,TOPREAL1:def 7;
suppose A27: (f/.i1)`2 = (f/.(i1+1))`2;
G*(j,i0)`2 = G*(1,i0)`2 by A20,A22,GOBOARD5:2
.= G*(j0,i0)`2 by A22,GOBOARD5:2
.= p`2 by A14,A18,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
then A28: i0<=i & i0>=i by A20,A22,GOBOARD5:5;
then A29: i=i0 by AXIOMS:21;
G*(j,io)`2 = G*(1,io)`2 by A20,A23,GOBOARD5:2
.= G*(jo,io)`2 by A23,GOBOARD5:2
.= p`2 by A14,A19,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
then A30: io<=i & io>=i by A20,A23,GOBOARD5:5;
then A31: i=io by AXIOMS:21;
thus thesis
proof
per cases;
suppose A32: (f/.i1)`1 <= (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose A33: (f/.(i1+1)) in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.(i1+1) in L~f by A17,GOBOARD1:16;
then f/.(i1+1) in X1 by A33,XBOOLE_0:def 3;
then A34: p`1 >= (f/.(i1+1))`1 by A5,A7,PSCOMP_1:71;
p`1 <= (f/.(i1+1))`1 by A14,A32,TOPREAL1:9;
then A35: p`1 = (f/.(i1+1))`1 by A34,AXIOMS:21;
take n=jo;
A36: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
then A37: p`2 = G*(j,i)`2 by A24,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A23,GOBOARD5:2;
A38: p`1 = G*(jo,1)`1 by A19,A23,A35,GOBOARD5:3
.= G*(n,i)`1 by A20,A23,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A39: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A36,A38,
TOPREAL1:9;
hence j <= n by A20,A23,GOBOARD5:4;
thus n <= k by A21,A23,A39,GOBOARD5:4;
thus thesis by A37,A38,TOPREAL3:11;
suppose A40: not f/.(i1+1) in LSeg(G*(j,i),G*(k,i));
A41: (f/.(i1+1))`2 = p`2 by A14,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
thus thesis
proof
per cases by A24,A40,A41,GOBOARD7:9;
suppose A42: (f/.(i1+1))`1 > G*(k,i)`1;
then A43: G*(jo,i)`1 > G*(k,i)`1 by A19,A30,AXIOMS:21;
jo>=k by A19,A21,A23,A31,A42,GOBOARD5:4;
then A44: jo>k by A43,AXIOMS:21;
j0<=jo+0 by A18,A19,A22,A23,A29,A31,A32,GOBOARD5:4;
then j0-jo <= 0 by REAL_1:86;
then -(j0-jo) >= -0 by REAL_1:50;
then A45: jo-j0 >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then abs(-(j0-jo)) = 1 by ABSVALUE:17;
then abs(jo-j0) = 1 by XCMPLX_1:143;
then jo-j0 = 1 by A45,ABSVALUE:def 1;
then j0+jo-j0 = j0+1 by XCMPLX_1:29;
then jo+(j0-j0) = j0+1 by XCMPLX_1:29;
then j0+1=jo+0 by XCMPLX_1:14;
then A46: j0>=k by A44,NAT_1:38;
p`1 >= G*(j0,i0)`1 by A14,A18,A32,TOPREAL1:9;
then p`1 >= G*(j0,1)`1 by A22,GOBOARD5:3;
then p`1 >= G*(j0,i)`1 by A20,A22,GOBOARD5:3;
then G*(k,i)`1 >= G*(j0,i)`1 by A26,AXIOMS:22;
then k>=j0 by A21,A22,GOBOARD5:4;
then A47: k=j0 by A46,AXIOMS:21;
take n=j0;
A48: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
p`1 >= G*(j0,i0)`1 by A14,A18,A32,TOPREAL1:9;
then p`1 >= G*(j0,1)`1 by A22,GOBOARD5:3;
then p`1 >= G*(j0,i)`1 by A20,A22,GOBOARD5:3;
then p`1 = G*(k,i)`1 by A26,A47,AXIOMS:21;
hence thesis by A4,A47,A48,TOPREAL3:11;
suppose A49: (f/.(i1+1))`1 < G*(j,i)`1;
p`1 <= (f/.(i1+1))`1 by A14,A32,TOPREAL1:9;
hence thesis by A26,A49,AXIOMS:22;
end;
end;
suppose A50: (f/.i1)`1 > (f/.(i1+1))`1;
thus thesis
proof
per cases;
suppose A51: f/.i1 in LSeg(G*(j,i),G*(k,i));
1+1<=i1+1 by A12,AXIOMS:24;
then 2<=len f by A13,AXIOMS:22;
then f/.i1 in L~f by A15,GOBOARD1:16;
then f/.i1 in X1 by A51,XBOOLE_0:def 3;
then A52: p`1 >= (f/.i1)`1 by A5,A7,PSCOMP_1:71;
p`1 <= (f/.i1)`1 by A14,A50,TOPREAL1:9;
then A53: p`1 = (f/.i1)`1 by A52,AXIOMS:21;
take n=j0;
A54: p in LSeg(G*(j,i),G*(k,i)) by A8,XBOOLE_0:def 3;
then A55: p`2 = G*(j,i)`2 by A24,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
A56: p`1 = G*(j0,1)`1 by A18,A22,A53,GOBOARD5:3
.= G*(n,i)`1 by A20,A22,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A57: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A54,A56,
TOPREAL1:9;
hence j <= n by A20,A22,GOBOARD5:4;
thus n <= k by A21,A22,A57,GOBOARD5:4;
thus thesis by A55,A56,TOPREAL3:11;
suppose A58: not f/.i1 in LSeg(G*(j,i),G*(k,i));
A59: (f/.i1)`2 = p`2 by A14,A27,GOBOARD7:6
.= G*(j,i)`2 by A24,A25,GOBOARD7:6;
thus thesis
proof
per cases by A24,A58,A59,GOBOARD7:9;
suppose A60: (f/.i1)`1 > G*(k,i)`1;
then A61: G*(j0,i)`1 > G*(k,i)`1 by A18,A28,AXIOMS:21;
j0>=k by A18,A21,A22,A29,A60,GOBOARD5:4;
then A62: j0>k by A61,AXIOMS:21;
jo<=j0+0 by A18,A19,A22,A23,A29,A31,A50,GOBOARD5:4;
then jo-j0 <= 0 by REAL_1:86;
then -(jo-j0) >= -0 by REAL_1:50;
then A63: j0-jo >= 0 by XCMPLX_1:143;
abs(i0-io)+abs(j0-jo) = 1 by A1,A15,A17,A18,A19,GOBOARD1:def 11
;
then abs(0)+abs(j0-jo) = 1 by A29,A31,XCMPLX_1:14;
then 0+abs(j0-jo) = 1 by ABSVALUE:7;
then j0-jo = 1 by A63,ABSVALUE:def 1;
then j0-(jo-jo) = jo+1 by XCMPLX_1:37;
then jo+1=j0-0 by XCMPLX_1:14;
then A64: jo>=k by A62,NAT_1:38;
p`1 >= G*(jo,io)`1 by A14,A19,A50,TOPREAL1:9;
then p`1 >= G*(jo,1)`1 by A23,GOBOARD5:3;
then p`1 >= G*(jo,i)`1 by A20,A23,GOBOARD5:3;
then G*(k,i)`1 >= G*(jo,i)`1 by A26,AXIOMS:22;
then k>=jo by A21,A23,GOBOARD5:4;
then A65: k=jo by A64,AXIOMS:21;
take n=jo;
A66: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A23,GOBOARD5:2;
p`1 >= G*(jo,io)`1 by A14,A19,A50,TOPREAL1:9;
then p`1 >= G*(jo,1)`1 by A23,GOBOARD5:3;
then p`1 >= G*(jo,i)`1 by A20,A23,GOBOARD5:3;
then p`1 = G*(k,i)`1 by A26,A65,AXIOMS:21;
hence thesis by A4,A65,A66,TOPREAL3:11;
suppose A67: (f/.i1)`1 < G*(j,i)`1;
p`1 <= (f/.i1)`1 by A14,A50,TOPREAL1:9;
hence thesis by A26,A67,AXIOMS:22;
end;
end;
end;
suppose (f/.i1)`1 = (f/.(i1+1))`1;
then A68: p`1 = (f/.i1)`1 by A14,GOBOARD7:5;
take n=j0;
A69: p`2 = G*(j,i)`2 by A24,A25,GOBOARD7:6
.= G*(1,i)`2 by A20,GOBOARD5:2
.= G*(n,i)`2 by A20,A22,GOBOARD5:2;
A70: p`1 = G*(j0,1)`1 by A18,A22,A68,GOBOARD5:3
.= G*(n,i)`1 by A20,A22,GOBOARD5:3;
G*(j,i)`1 <= G*(k,i)`1 by A4,A20,A21,SPRECT_3:25;
then A71: G*(j,i)`1 <= G*(n,i)`1 & G*(n,i)`1 <= G*(k,i)`1 by A25,A70,TOPREAL1:
9;
hence j <= n by A20,A22,GOBOARD5:4;
thus n <= k by A21,A22,A71,GOBOARD5:4;
thus thesis by A69,A70,TOPREAL3:11;
end;
hence ex n st j <= n & n <= k & G*(n,i)`1 = sup(proj1.:X) by A7;
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;
A1: Upper_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)
by JORDAN1E:def 1;
A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A2,FINSEQ_6:96;
then Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1
by A1,FINSEQ_5:47;
hence Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by A2,FINSEQ_6:98;
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 Lower_Seq(C,n)/.1 = E-max L~Cage(C,n) by FINSEQ_5:56;
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)
by JORDAN1E:def 1;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
then rng Rotate(Cage(C,n),W-min L~Cage(C,n)) = rng Cage(C,n) by FINSEQ_6:96
;
then A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by SPRECT_2:50;
then len Upper_Seq(C,n) =
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A1,FINSEQ_5:45;
hence Upper_Seq(C,n)/.len Upper_Seq(C,n) =
E-max L~Cage(C,n) by A1,A2,FINSEQ_5:48;
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: Lower_Seq(C,n) = Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)
by JORDAN1E:def 2;
A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A2,FINSEQ_6:96;
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 A1,FINSEQ_5:57
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A2,FINSEQ_6:98;
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: Upper_Seq(C,n)/.1 = WC by Th5;
A2: Upper_Seq(C,n)/. len Upper_Seq(C,n) = EC by Th7;
A3: Lower_Seq(C,n)/.1 = EC by Th6;
A4: Lower_Seq(C,n)/. len Lower_Seq(C,n) = WC by Th8;
A5: L~Upper_Seq(C,n) is_an_arc_of WC,EC by A1,A2,TOPREAL1:31;
L~Lower_Seq(C,n) is_an_arc_of EC,WC by A3,A4,TOPREAL1:31;
then A6: L~Lower_Seq(C,n) is_an_arc_of WC,EC by JORDAN5B:14;
A7: L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n)=L~Cage(C,n) by JORDAN1E:17;
Upper_Arc(L~Cage(C,n)) is_an_arc_of WC,EC &
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) &
Upper_Arc(L~Cage(C,n)) /\ Lower_Arc(L~Cage(C,n))=
{WC,EC} by JORDAN6:65;
hence thesis by A5,A6,A7,JORDAN6:61;
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:38;
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 abs(i2-i1)+abs(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 abs(i2-i1)+abs(j2-j1) = 1;
A4: 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 abs(m-i)+abs(k-j)=1
by A1,GOBOARD1:def 11;
A5: now let n;
assume n in dom <*p*> & n+1 in dom <*p*>;
then 1 <= n & n+1 <= len <*p*> by FINSEQ_3:27;
then 1+1 <= n+1 & n+1 <= 1 by AXIOMS:24,FINSEQ_1:56;
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 abs(m-i)+abs(k-j)=1 by AXIOMS:22;
end;
now let m,k,i,j such that
A6: [m,k] in Indices G & [i,j] in Indices G & <*p*>/.(len <*p*>)=G*(m,k) &
f/.1=G*(i,j) and
A7: len <*p*> in dom <*p*> & 1 in dom f;
len <*p*> = 1 by FINSEQ_1:57;
then <*p*>.(len <*p*>) = p by FINSEQ_1:57;
then <*p*>/.(len <*p*>) = p by A7,FINSEQ_4:def 4;
then abs(i-m)+abs(j-k)=1 by A3,A6;
hence 1 = abs(m-i)+abs(j-k) by UNIFORM1:13
.= abs(m-i)+abs(k-j) by UNIFORM1:13;
end;
then A8: 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 abs(m-i)+abs(k-j)=1 by A4,A5,GOBOARD1:40;
now let n such that
A9: n in dom(<*p*>^f);
per cases by A9,FINSEQ_1:38;
suppose
A10: n in dom <*p*>; then n in Seg 1 by FINSEQ_1:55;
then 1 <= n & n <= 1 by FINSEQ_1:3;
then n=1 by AXIOMS:21;
then <*p*>.n = p by FINSEQ_1:57;
then A11: <*p*>/.n = p by A10,FINSEQ_4:def 4;
consider i,j such that
A12: [i,j] in Indices G and
A13: p = G*(i,j) by A2;
take i,j;
thus [i,j] in Indices G by A12;
thus (<*p*>^f)/.n = G*(i,j) by A10,A11,A13,GROUP_5:95;
suppose ex l st l in dom f & n = (len <*p*>) + l;
then consider l such that
A14: l in dom f and
A15: n = (len <*p*>) + l;
consider i,j such that
A16: [i,j] in Indices G and
A17: f/.l = G*(i,j) by A1,A14,GOBOARD1:def 11;
take i,j;
thus [i,j] in Indices G by A16;
thus (<*p*>^f)/.n = G*(i,j) by A14,A15,A17,GROUP_5:96;
end;
hence <*p*>^f is_sequence_on G by A8,GOBOARD1:def 11;
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;
A1: 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 A2: (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:5;
consider j such that
A3: 1 <= j & j <= width Gauge(C,n) &
E-max L~Cage(C,n)=Gauge(C,n)*(len Gauge(C,n),j) by JORDAN1D:29;
set i = len Gauge(C,n);
i >=4 by JORDAN8:13;
then 1<=i by AXIOMS:22;
then A4: [i,j] in Indices Gauge(C,n) by A3,GOBOARD7:10;
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;
A5: 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 abs(i2-i1)+abs(j2-j1) = 1
proof
let i1,j1,i2,j2;
assume that
A6: [i1,j1] in Indices Gauge(C,n) and
A7: [i2,j2] in Indices Gauge(C,n) and
A8: E-max L~Cage(C,n) = Gauge(C,n)*(i1,j1) and
A9: E1 = Gauge(C,n)*(i2,j2);
set en = (E-max L~Cage(C,n))..Cage(C,n);
A10: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
A11: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
A12: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:34;
then A13: (E-max L~Cage(C,n))..Cage(C,n) < (E-min L~Cage(C,n))..Cage(C,n)
by SPRECT_2:75;
(E-min L~Cage(C,n))..Cage(C,n) <= (S-max L~Cage(C,n))..Cage(C,n)
by A12,SPRECT_2:76;
then A14: (E-max L~Cage(C,n))..Cage(C,n) < (S-max L~Cage(C,n))..Cage(C,n)
by A13,AXIOMS:22;
(S-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A12,SPRECT_2:77;
then A15: (E-max L~Cage(C,n))..Cage(C,n) < (S-min L~Cage(C,n))..Cage(C,n)
by A14,AXIOMS:22;
(S-min L~Cage(C,n))..Cage(C,n) <= (W-min L~Cage(C,n))..Cage(C,n)
by A12,SPRECT_2:78;
then A16: (E-max L~Cage(C,n))..Cage(C,n) < (W-min L~Cage(C,n))..Cage(C,n)
by A15,AXIOMS:22;
A17: E-max L~Cage(C,n)=Cage(C,n)/.en by A10,FINSEQ_5:41;
A18: en in dom Cage(C,n) by A10,FINSEQ_4:30;
A19: 1<=en+1 by NAT_1:29;
en < len Cage(C,n) by SPRECT_5:17;
then en+1 <= len Cage(C,n) by NAT_1:38;
then A20: en+1 in dom Cage(C,n) by A19,FINSEQ_3:27;
1 <= (E-max L~Cage(C,n))..Cage(C,n) by A10,FINSEQ_4:31;
then A21: 1 < (E-max L~Cage(C,n))..Cage(C,n)+1 by NAT_1:38;
A22: (E-max L~Cage(C,n))..Cage(C,n)+1 <= (W-min L~Cage(C,n))..Cage(C,n)
by A16,NAT_1:38;
(W-min L~Cage(C,n))..Cage(C,n) < len Cage(C,n) by SPRECT_5:21;
then A23: len Cage(C,n) - (W-min L~Cage(C,n))..Cage(C,n) > 0 by SQUARE_1:11;
(E-max L~Cage(C,n))..Cage(C,n) + 1 >= 0 by NAT_1:18;
then ((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 by A23,REAL_1:67;
then A24: ((E-max L~Cage(C,n))..Cage(C,n) + 1 + len Cage(C,n) -
(W-min L~Cage(C,n))..Cage(C,n)) >= 0 by XCMPLX_1:29;
E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n))
by A10,A11,FINSEQ_6:96;
then A25: 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)) by FINSEQ_4:31;
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 REVROT_1:14;
then len Upper_Seq(C,n) = len Cage(C,n) by JORDAN1E:12;
then len Cage(C,n) + len Lower_Seq(C,n) = len Cage(C,n)+1 by JORDAN1E:14
;
then len Lower_Seq(C,n) = 1 by XCMPLX_1:2;
hence contradiction by JORDAN1E:19;
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 A25,AXIOMS:21;
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:38;
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 REAL_1:49;
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 XCMPLX_1:26;
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 A25,RFINSEQ:def 2;
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:27;
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:30
.= 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 A10,A11,A16,SPRECT_5:10
.= 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 XCMPLX_1:29
.= 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 A23,BINARITH:def
3
.= 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 XCMPLX_1:1
.= 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 A23,BINARITH:def 3
.= 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 XCMPLX_1:29
.= 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 A24,BINARITH:def 3;
then E1=Cage(C,n)/.(en+1) by A11,A21,A22,REVROT_1:13;
then abs(i1-i2)+abs(j1-j2) = 1 by A1,A6,A7,A8,A9,A17,A18,A20,GOBOARD1:def
11;
then abs(i1-i2)+abs(j2-j1) = 1 by UNIFORM1:13;
hence abs(i2-i1)+abs(j2-j1) = 1 by UNIFORM1:13;
end;
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;
hence thesis by A2,A3,A4,A5,Th11;
end;
theorem
p`1 = (W-bound C + E-bound C)/2 &
p`2 = inf(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 = inf(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);
set f = Upper_Seq (C,i+1);
set G = Gauge(C,i+1);
set l = Center Gauge(C,i+1);
set k = width Gauge(C,i+1);
A4: width Gauge(C,i+1) = len Gauge(C,i+1) &
width Gauge(C,1) = len Gauge(C,1) by JORDAN8:def 1;
A5: f is_sequence_on G by Th10;
k >= 4 by A4,JORDAN8:13;
then A6: 1 <= k by AXIOMS:22;
then A7: l <= len G by A4,JORDAN1B:13;
width Gauge(C,1) >= 4 by A4,JORDAN8:13;
then A8: 1 <= width Gauge(C,1) by AXIOMS:22;
then A9: Center Gauge(C,1) <= len Gauge(C,1) by A4,JORDAN1B:13;
A10: 1 <= l by JORDAN1B:12;
A11: 1 <= Center Gauge(C,1) by JORDAN1B:12;
A12: LSeg(G*(l,1),G*(l,k)) meets L~f by A3,A4,A7,A10,JORDAN1B:32;
A13: [l,1] in Indices G by A6,A7,A10,GOBOARD7:10;
[l,k] in Indices G by A6,A7,A10,GOBOARD7:10;
then consider n such that
A14: 1 <= n & n <= k and
A15: G*(l,n)`2 = inf(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f)) by A5,A6,A12,A13,
Th1;
take n;
thus 1 <= n & n <= width Gauge(C,i+1) by A14;
A16: i+1 > 0 & 1 > 0 by NAT_1:19;
len Gauge(C,1) >= 4 by JORDAN8:13;
then A17: 1 <= len Gauge(C,1) by AXIOMS:22;
then A18: p`1 = (Gauge(C,1)*(Center Gauge(C,1),1))`1 by A1,JORDAN1A:59
.= Gauge(C,i+1)*(Center Gauge(C,i+1),n)`1 by A4,A14,A16,A17,JORDAN1A:57;
1 <= i+1 by NAT_1:29;
then A19: LSeg(G*(l,1),G*(l,k)) c=
LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) by A4,JORDAN1A:65;
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
proof
thus 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 set;
assume A20: 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;
A21: a1 in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)))
& a1 in L~f by A20,XBOOLE_0:def 3;
Gauge(C,1)*(Center Gauge(C,1),1)`1 =
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))`1
by A8,A9,A11,GOBOARD5:3;
then A22: a1`1 = Gauge(C,1)*(Center Gauge(C,1),1)`1 by A21,GOBOARD7:5
.= G*(l,1)`1 by A4,A6,A8,A16,JORDAN1A:57;
then A23: a1`1 = G*(l,k)`1 by A6,A7,A10,GOBOARD5:3;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then A24: G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A7,A10,JORDAN1A:43;
A25: Upper_Arc L~Cage(C,i+1) c= L~Cage(C,i+1) by JORDAN1A:16;
a1 in Upper_Arc L~Cage(C,i+1) by A3,A20,XBOOLE_0:def 3;
then a1`2 >= S-bound L~Cage(C,i+1) by A25,PSCOMP_1:71;
then A26: a1`2 >= G*(l,1)`2 by A24,AXIOMS:22;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then A27: G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A7,A10,JORDAN1A:41;
a1 in Upper_Arc L~Cage(C,i+1) by A3,A20,XBOOLE_0:def 3;
then a1`2 <= N-bound L~Cage(C,i+1) by A25,PSCOMP_1:71;
then a1`2 <= G*(l,k)`2 by A27,AXIOMS:22;
then a1 in LSeg(G*(l,1),G*(l,k)) by A22,A23,A26,GOBOARD7:8;
hence a in LSeg(G*(l,1),G*(l,k)) /\ L~f by A21,XBOOLE_0:def 3;
end;
thus thesis by A19,XBOOLE_1:26;
end;
hence p = Gauge(C,i+1)*(Center Gauge(C,i+1),n) by A2,A3,A15,A18,TOPREAL3:11
;
suppose A28: 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);
set f = Lower_Seq (C,i+1);
set G = Gauge(C,i+1);
set l = Center Gauge(C,i+1);
set k = width Gauge(C,i+1);
A29: width Gauge(C,i+1) = len Gauge(C,i+1) &
width Gauge(C,1) = len Gauge(C,1) by JORDAN8:def 1;
A30: f is_sequence_on G by Th12;
k >= 4 by A29,JORDAN8:13;
then A31: 1 <= k by AXIOMS:22;
then A32: l <= len G by A29,JORDAN1B:13;
width Gauge(C,1) >= 4 by A29,JORDAN8:13;
then A33: 1 <= width Gauge(C,1) by AXIOMS:22;
then A34: Center Gauge(C,1) <= len Gauge(C,1) by A29,JORDAN1B:13;
A35: 1 <= l by JORDAN1B:12;
A36: 1 <= Center Gauge(C,1) by JORDAN1B:12;
A37: LSeg(G*(l,1),G*(l,k)) meets L~f by A28,A29,A32,A35,JORDAN1B:32;
A38: [l,1] in Indices G by A31,A32,A35,GOBOARD7:10;
[l,k] in Indices G by A31,A32,A35,GOBOARD7:10;
then consider n such that
A39: 1 <= n & n <= k and
A40: G*(l,n)`2 = inf(proj2.:(LSeg(G*(l,1),G*(l,k)) /\ L~f)) by A30,A31,A37,A38,
Th1;
take n;
thus 1 <= n & n <= width Gauge(C,i+1) by A39;
A41: i+1 > 0 & 1 > 0 by NAT_1:19;
len Gauge(C,1) >= 4 by JORDAN8:13;
then A42: 1 <= len Gauge(C,1) by AXIOMS:22;
then A43: p`1 = (Gauge(C,1)*(Center Gauge(C,1),1))`1 by A1,JORDAN1A:59
.= Gauge(C,i+1)*(Center Gauge(C,i+1),n)`1 by A29,A39,A41,A42,JORDAN1A:57
;
1 <= i+1 by NAT_1:29;
then A44: LSeg(G*(l,1),G*(l,k)) c=
LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) by A29,JORDAN1A:65;
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
proof
thus 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 set;
assume A45: 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;
A46: a1 in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)))
& a1 in L~f by A45,XBOOLE_0:def 3;
Gauge(C,1)*(Center Gauge(C,1),1)`1 =
Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))`1
by A33,A34,A36,GOBOARD5:3;
then A47: a1`1 = Gauge(C,1)*(Center Gauge(C,1),1)`1 by A46,GOBOARD7:5
.= G*(l,1)`1 by A29,A31,A33,A41,JORDAN1A:57;
then A48: a1`1 = G*(l,k)`1 by A31,A32,A35,GOBOARD5:3;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then A49: G*(l,1)`2 <= S-bound L~Cage(C,i+1) by A32,A35,JORDAN1A:43;
A50: Upper_Arc L~Cage(C,i+1) c= L~Cage(C,i+1) by JORDAN1A:16;
a1 in Upper_Arc L~Cage(C,i+1) by A28,A45,XBOOLE_0:def 3;
then a1`2 >= S-bound L~Cage(C,i+1) by A50,PSCOMP_1:71;
then A51: a1`2 >= G*(l,1)`2 by A49,AXIOMS:22;
Cage(C,i+1) is_sequence_on G by JORDAN9:def 1;
then A52: G*(l,k)`2 >= N-bound L~Cage(C,i+1) by A32,A35,JORDAN1A:41;
a1 in Upper_Arc L~Cage(C,i+1) by A28,A45,XBOOLE_0:def 3;
then a1`2 <= N-bound L~Cage(C,i+1) by A50,PSCOMP_1:71;
then a1`2 <= G*(l,k)`2 by A52,AXIOMS:22;
then a1 in LSeg(G*(l,1),G*(l,k)) by A47,A48,A51,GOBOARD7:8;
hence a in LSeg(G*(l,1),G*(l,k)) /\ L~f by A46,XBOOLE_0:def 3;
end;
thus thesis by A44,XBOOLE_1:26;
end;
hence p = Gauge(C,i+1)*(Center Gauge(C,i+1),n) by A2,A28,A40,A43,TOPREAL3:11
;
end;