:: On the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997-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, XBOOLE_0, FINSEQ_1, XXREAL_0, RELAT_1,
JORDAN3, ARYTM_3, ARYTM_1, CARD_1, PARTFUN1, FUNCT_1, RCOMP_1, EUCLID,
PRE_TOPC, MCART_1, PSCOMP_1, RLTOPSP1, TOPREAL1, TARSKI, GOBOARD1,
REAL_1, SUPINF_2, ZFMISC_1, ORDINAL4, NAT_1, GOBOARD4, FINSEQ_6,
GOBOARD5, STRUCT_0, SPPOL_1, SPRECT_1, SPPOL_2, FINSEQ_5, FINSEQ_4,
TOPREAL2, SPRECT_2, SEQ_4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, STRUCT_0, FINSEQ_4,
FINSEQ_5, ZFMISC_1, FINSEQ_6, NAT_1, NAT_D, PRE_TOPC, COMPTS_1, RLVECT_1,
RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD4, SPPOL_1,
SPPOL_2, GOBOARD5, PSCOMP_1, SPRECT_1, XXREAL_0;
constructors REAL_1, FINSEQ_4, NAT_D, FINSEQ_5, COMPTS_1, TOPREAL2, GOBOARD1,
GOBOARD4, SPPOL_1, GOBOARD5, PSCOMP_1, SPRECT_1, SEQ_4, RELSET_1,
CONVEX1;
registrations RELSET_1, NUMBERS, XREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC,
EUCLID, GOBOARD2, SPPOL_2, SPRECT_1, XBOOLE_0, VALUED_0, FUNCT_1,
RLTOPSP1, MEASURE6, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, GOBOARD4, XBOOLE_0;
equalities TOPREAL1, PSCOMP_1, STRUCT_0, RLTOPSP1;
expansions XBOOLE_0;
theorems FINSEQ_6, FINSEQ_4, FINSEQ_5, GOBOARD4, GOBOARD1, PSCOMP_1, FINSEQ_3,
JORDAN3, NAT_1, SPPOL_1, FINSEQ_1, JORDAN4, ZFMISC_1, SPPOL_2, TOPREAL3,
TARSKI, FUNCT_1, TOPREAL1, GOBOARD2, GOBOARD7, PARTFUN2, GOBOARD5,
EUCLID, TOPREAL2, FUNCT_2, PRE_TOPC, RELAT_1, SPRECT_1, TOPREAL5,
XBOOLE_0, XBOOLE_1, XCMPLX_1, SEQ_4, XREAL_1, XXREAL_0, PARTFUN1, CARD_1,
NAT_D, RLTOPSP1, RLVECT_1;
begin :: Finite sequences
reserve i,j,k,l,m,n for Nat,
D for non empty set,
f for FinSequence of D;
theorem Th1:
i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies k+
i-'1 in dom f
proof
assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f;
A4: j <= len f by A3,FINSEQ_3:25;
A5: 1+0 <= i by A2,FINSEQ_3:25;
then i-1 >= 0 by XREAL_1:19;
then
A6: k+0 <= k+(i-1) by XREAL_1:6;
assume
A7: k in dom mid(f,i,j);
then
A8: k <= len mid(f,i,j) by FINSEQ_3:25;
i <= len f & 1 <= j by A2,A3,FINSEQ_3:25;
then len mid(f,i,j) = j -' i +1 by A1,A5,A4,FINSEQ_6:118;
then k <= j - i +1 by A1,A8,XREAL_1:233;
then k <= j +1 - i;
then k+i <= j +1 by XREAL_1:19;
then k+i >= i & k+i - 1 <= j by NAT_1:11,XREAL_1:20;
then k+i -' 1 <= j by A5,XREAL_1:233,XXREAL_0:2;
then
A9: k+i-'1 <= len f by A4,XXREAL_0:2;
1 <= k by A7,FINSEQ_3:25;
then 1 <= k+i-1 by A6,XXREAL_0:2;
then 1 <= k+i-'1 by NAT_D:39;
hence thesis by A9,FINSEQ_3:25;
end;
theorem Th2:
i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies i
-' k + 1 in dom f
proof
assume that
A1: i > j and
A2: i in dom f and
A3: j in dom f;
A4: i <= len f by A2,FINSEQ_3:25;
A5: 1+0 <= j by A3,FINSEQ_3:25;
then 1 - j <= 0 by XREAL_1:47;
then
A6: i +(1 - j) <= i + 0 by XREAL_1:6;
assume
A7: k in dom mid(f,i,j);
then
A8: k <= len mid(f,i,j) by FINSEQ_3:25;
k >= 1 by A7,FINSEQ_3:25;
then 1 - k <= 0 by XREAL_1:47;
then i + (1 - k) <= i+0 by XREAL_1:6;
then
A9: i - k + 1 <= i;
1+0 <= i & j <= len f by A2,A3,FINSEQ_3:25;
then len mid(f,i,j) = i -' j +1 by A1,A4,A5,FINSEQ_6:118;
then k <= i - j +1 by A1,A8,XREAL_1:233;
then i -' k + 1 <= i by A6,A9,XREAL_1:233,XXREAL_0:2;
then
A10: i -' k + 1 <= len f by A4,XXREAL_0:2;
1 <= i -' k + 1 by NAT_1:11;
hence thesis by A10,FINSEQ_3:25;
end;
theorem Th3:
i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies (
mid(f,i,j))/.k = f/.(k+i-'1)
proof
assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f and
A4: k in dom mid(f,i,j);
A5: 1 <= i & i <= len f by A2,FINSEQ_3:25;
A6: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:25;
A7: 1 <= j & j <= len f by A3,FINSEQ_3:25;
thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,PARTFUN1:def 6
.= f.(k+i-'1) by A1,A5,A7,A6,FINSEQ_6:118
.= f/.(k+i-'1) by A1,A2,A3,A4,Th1,PARTFUN1:def 6;
end;
theorem Th4:
i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies (
mid(f,i,j))/.k = f/.(i-' k +1)
proof
assume that
A1: i > j and
A2: i in dom f and
A3: j in dom f and
A4: k in dom mid(f,i,j);
A5: 1 <= i & i <= len f by A2,FINSEQ_3:25;
A6: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:25;
A7: 1 <= j & j <= len f by A3,FINSEQ_3:25;
thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,PARTFUN1:def 6
.= f.(i -' k +1) by A1,A5,A7,A6,FINSEQ_6:118
.= f/.(i-' k +1) by A1,A2,A3,A4,Th2,PARTFUN1:def 6;
end;
theorem Th5:
i in dom f & j in dom f implies len mid(f,i,j) >= 1
proof
A1: i <= j or j < i;
assume i in dom f;
then
A2: 1 <= i & i <= len f by FINSEQ_3:25;
assume j in dom f;
then 1 <= j & j <= len f by FINSEQ_3:25;
then len mid(f,i,j)=i-'j+1 or len mid(f,i,j)=j-'i+1 by A2,A1,FINSEQ_6:118;
hence thesis by NAT_1:11;
end;
theorem Th6:
i in dom f & j in dom f & len mid(f,i,j) = 1 implies i = j
proof
assume
A1: i in dom f;
then
A2: 1 <= i by FINSEQ_3:25;
A3: i <= len f by A1,FINSEQ_3:25;
assume
A4: j in dom f;
then
A5: 1 <= j by FINSEQ_3:25;
A6: j <= len f by A4,FINSEQ_3:25;
assume
A7: len mid(f,i,j) = 1;
per cases;
suppose
A8: i <= j;
then 0 + 1 = j -' i + 1 by A2,A6,A7,FINSEQ_6:186;
then 0 = j - i by A8,XREAL_1:233;
hence thesis;
end;
suppose
A9: i >= j;
then 0 + 1 = i -' j + 1 by A3,A5,A7,FINSEQ_6:187;
then 0 = i - j by A9,XREAL_1:233;
hence thesis;
end;
end;
theorem Th7:
i in dom f & j in dom f implies mid(f,i,j) is non empty
proof
assume i in dom f & j in dom f;
then len mid(f,i,j) >= 1 by Th5;
hence thesis by FINSEQ_3:25,RELAT_1:38;
end;
theorem Th8:
i in dom f & j in dom f implies (mid(f,i,j))/.1 = f/.i
proof
assume
A1: i in dom f;
then
A2: 1 <= i & i <= len f by FINSEQ_3:25;
assume
A3: j in dom f;
then
A4: 1 <= j & j <= len f by FINSEQ_3:25;
mid(f,i,j) is non empty by A1,A3,Th7;
then 1 in dom mid(f,i,j) by FINSEQ_5:6;
hence (mid(f,i,j))/.1 = mid(f,i,j).1 by PARTFUN1:def 6
.= f.i by A2,A4,FINSEQ_6:118
.= f/.i by A1,PARTFUN1:def 6;
end;
theorem Th9:
i in dom f & j in dom f implies (mid(f,i,j))/.len mid(f,i,j) = f /.j
proof
assume
A1: i in dom f;
then
A2: 1 <= i & i <= len f by FINSEQ_3:25;
assume
A3: j in dom f;
then
A4: 1 <= j & j <= len f by FINSEQ_3:25;
mid(f,i,j) is non empty by A1,A3,Th7;
then len mid(f,i,j) in dom mid(f,i,j) by FINSEQ_5:6;
hence (mid(f,i,j))/.len mid(f,i,j) = mid(f,i,j).len mid(f,i,j) by
PARTFUN1:def 6
.= f.j by A2,A4,FINSEQ_6:189
.= f/.j by A3,PARTFUN1:def 6;
end;
begin :: Compact sets on the plane
reserve X for compact Subset of TOP-REAL 2;
theorem Th10:
for p being Point of TOP-REAL 2 st p in X & p`2 = N-bound X
holds p in N-most X
proof
let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`2 = N-bound X;
A3: (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
A4: (NW-corner X)`1 = W-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:24;
then p in LSeg(NW-corner X, NE-corner X) by A2,A3,A4,GOBOARD7:8;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th11:
for p being Point of TOP-REAL 2 st p in X & p`2 = S-bound X
holds p in S-most X
proof
let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`2 = S-bound X;
A3: (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by EUCLID:52;
A4: (SW-corner X)`1 = W-bound X & (SE-corner X)`1 = E-bound X by EUCLID:52;
W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:24;
then p in LSeg(SW-corner X, SE-corner X) by A2,A3,A4,GOBOARD7:8;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th12:
for p being Point of TOP-REAL 2 st p in X & p`1 = W-bound X
holds p in W-most X
proof
let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`1 = W-bound X;
A3: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by EUCLID:52;
A4: (SW-corner X)`2 = S-bound X & (NW-corner X)`2 = N-bound X by EUCLID:52;
S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:24;
then p in LSeg(SW-corner X, NW-corner X) by A2,A3,A4,GOBOARD7:7;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th13:
for p being Point of TOP-REAL 2 st p in X & p`1 = E-bound X
holds p in E-most X
proof
let p be Point of TOP-REAL 2 such that
A1: p in X and
A2: p`1 = E-bound X;
A3: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
A4: (SE-corner X)`2 = S-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:24;
then p in LSeg(SE-corner X, NE-corner X) by A2,A3,A4,GOBOARD7:7;
hence thesis by A1,XBOOLE_0:def 4;
end;
begin :: Finite sequences on the plane
theorem Th14:
for f being FinSequence of TOP-REAL 2 st 1 <= i & i <= j & j <=
len f holds L~mid(f,i,j) = union{ LSeg(f,k): i <= k & k < j}
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: 1 <= i and
A2: i <= j and
A3: j <= len f;
set A = { LSeg(mid(f,i,j),m) : 1 <= m & m+1 <= len mid(f,i,j) }, B = { LSeg(
f,l): i <= l & l < j};
per cases by A2,XXREAL_0:1;
suppose
A4: i = j;
A5: B = {}
proof
assume B <> {};
then consider z being object such that
A6: z in B by XBOOLE_0:def 1;
ex l st z = LSeg(f,l) & i <= l & l < j by A6;
hence contradiction by A4;
end;
AA: i in dom f by FINSEQ_3:25,A1,A3,A4; then
mid(f,i,j) = <*f.i*> by A4,FINSEQ_6:193
.= <*f/.i*> by AA,PARTFUN1:def 6;
hence thesis by A5,SPPOL_2:12,ZFMISC_1:2;
end;
suppose
A7: i < j;
A = B
proof
hereby
let x be object;
assume x in A;
then consider m such that
A8: x = LSeg(mid(f,i,j),m) and
A9: 0+1 <= m and
A10: m+1 <= len mid(f,i,j);
i < m+i by A9,XREAL_1:29;
then
A11: i <= m+i-'1 by NAT_D:49;
len mid(f,i,j) = j -' i + 1 by A1,A3,A7,FINSEQ_6:186;
then
A12: m < j -' i + 1 by A10,NAT_1:13;
then m <= j -' i by NAT_1:13;
then m <= j - i by A7,XREAL_1:233;
then m+i >= m & m+i <= j by NAT_1:11,XREAL_1:19;
then m+i-'1+1 <= j by A9,XREAL_1:235,XXREAL_0:2;
then
A13: m+i-'1 < j by NAT_1:13;
x = LSeg(f,m+i-'1) by A1,A3,A7,A8,A9,A12,JORDAN4:19;
hence x in B by A13,A11;
end;
let x be object;
assume x in B;
then consider l such that
A14: x = LSeg(f,l) and
A15: i <= l and
A16: l < j;
set m = l -' i + 1;
A17: l - i < j - i by A16,XREAL_1:9;
l -' i = l - i & j -' i = j - i by A15,A16,XREAL_1:233,XXREAL_0:2;
then
A18: m < j-'i+1 by A17,XREAL_1:6;
len mid(f,i,j) = j -' i + 1 by A1,A3,A7,FINSEQ_6:186;
then
A19: m+1 <= len mid(f,i,j) by A18,NAT_1:13;
A20: 1 <= m by NAT_1:11;
m+i-'1 = l -' i + i + 1 -' 1 .= l + 1 -' 1 by A15,XREAL_1:235
.= l by NAT_D:34;
then x = LSeg(mid(f,i,j),m) by A1,A3,A7,A14,A20,A18,JORDAN4:19;
hence thesis by A20,A19;
end;
hence thesis;
end;
end;
theorem Th15:
for f being FinSequence of TOP-REAL 2 holds dom X_axis f = dom f
proof
let f be FinSequence of TOP-REAL 2;
len X_axis f = len f by GOBOARD1:def 1;
hence thesis by FINSEQ_3:29;
end;
theorem Th16:
for f being FinSequence of TOP-REAL 2 holds dom Y_axis f = dom f
proof
let f be FinSequence of TOP-REAL 2;
len Y_axis f = len f by GOBOARD1:def 2;
hence thesis by FINSEQ_3:29;
end;
reserve r for Real;
theorem Th17:
for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`1 <= b
`1 & c`1 <= b`1 holds a = b or b = c or a`1 = b`1 & c`1 = b`1
proof
let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`1 <= b`1 & c`1 <= b`1;
consider r such that
A3: b = (1-r)*a + r*c and
0 <= r and
r <= 1 by A1;
per cases by A2,XXREAL_0:1;
suppose that
A4: a`1 = b`1 and
A5: c`1 < b`1;
b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:2
.= ((1-r)*a)`1 + r*c`1 by TOPREAL3:4
.= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:4
.= b`1 + (r*c`1-r*b`1);
then
A6: 0 = r*(c`1-b`1);
c`1-b`1 < 0 by A5,XREAL_1:49;
then r = 0 by A6,XCMPLX_1:6;
then b = 1*a + 0.TOP-REAL 2 by A3,RLVECT_1:10
.= 1*a by RLVECT_1:4
.= a by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A7: a`1 < b`1 and
A8: c`1 = b`1;
b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:2
.= ((1-r)*a)`1 + r*c`1 by TOPREAL3:4
.= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:4;
then
A9: 0 = (1-r)*(a`1-b`1);
a`1-b`1 < 0 by A7,XREAL_1:49;
then 1 - r = 0 by A9,XCMPLX_1:6;
then b = 0.TOP-REAL 2 + 1*c by A3,RLVECT_1:10
.= 1*c by RLVECT_1:4
.= c by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A10: a`1 < b`1 & c`1 < b`1;
a`1 <= c`1 or c`1 <= a`1;
hence thesis by A1,A10,TOPREAL1:3;
end;
suppose
a`1 = b`1 & c`1 = b`1;
hence thesis;
end;
end;
theorem Th18:
for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`2 <= b
`2 & c`2 <= b`2 holds a = b or b = c or a`2 = b`2 & c`2 = b`2
proof
let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`2 <= b`2 & c`2 <= b`2;
consider r such that
A3: b = (1-r)*a + r*c and
0 <= r and
r <= 1 by A1;
per cases by A2,XXREAL_0:1;
suppose that
A4: a`2 = b`2 and
A5: c`2 < b`2;
b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:2
.= ((1-r)*a)`2 + r*c`2 by TOPREAL3:4
.= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:4
.= b`2 + (r*c`2-r*b`2);
then
A6: 0 = r*(c`2-b`2);
c`2-b`2 < 0 by A5,XREAL_1:49;
then r = 0 by A6,XCMPLX_1:6;
then b = 1*a + 0.TOP-REAL 2 by A3,RLVECT_1:10
.= 1*a by RLVECT_1:4
.= a by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A7: a`2 < b`2 and
A8: c`2 = b`2;
b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:2
.= ((1-r)*a)`2 + r*c`2 by TOPREAL3:4
.= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:4;
then
A9: 0 = (1-r)*(a`2-b`2);
a`2-b`2 < 0 by A7,XREAL_1:49;
then 1 - r = 0 by A9,XCMPLX_1:6;
then b = 0.TOP-REAL 2 + 1*c by A3,RLVECT_1:10
.= 1*c by RLVECT_1:4
.= c by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A10: a`2 < b`2 & c`2 < b`2;
a`2 <= c`2 or c`2 <= a`2;
hence thesis by A1,A10,TOPREAL1:4;
end;
suppose
a`2 = b`2 & c`2 = b`2;
hence thesis;
end;
end;
theorem Th19:
for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`1 >= b
`1 & c`1 >= b`1 holds a = b or b = c or a`1 = b`1 & c`1 = b`1
proof
let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`1 >= b`1 & c`1 >= b`1;
consider r such that
A3: b = (1-r)*a + r*c and
0 <= r and
r <= 1 by A1;
per cases by A2,XXREAL_0:1;
suppose that
A4: a`1 = b`1 and
A5: c`1 > b`1;
b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:2
.= ((1-r)*a)`1 + r*c`1 by TOPREAL3:4
.= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:4
.= b`1 + (r*c`1-r*b`1);
then
A6: 0 = r*(c`1-b`1);
c`1-b`1 > 0 by A5,XREAL_1:50;
then r = 0 by A6,XCMPLX_1:6;
then b = 1*a + 0.TOP-REAL 2 by A3,RLVECT_1:10
.= 1*a by RLVECT_1:4
.= a by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A7: a`1 > b`1 and
A8: c`1 = b`1;
b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:2
.= ((1-r)*a)`1 + r*c`1 by TOPREAL3:4
.= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:4;
then
A9: 0 = (1-r)*(a`1-b`1);
a`1-b`1 > 0 by A7,XREAL_1:50;
then 1 - r = 0 by A9,XCMPLX_1:6;
then b = 0.TOP-REAL 2 + 1*c by A3,RLVECT_1:10
.= 1*c by RLVECT_1:4
.= c by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A10: a`1 > b`1 & c`1 > b`1;
a`1 >= c`1 or c`1 >= a`1;
hence thesis by A1,A10,TOPREAL1:3;
end;
suppose
a`1 = b`1 & c`1 = b`1;
hence thesis;
end;
end;
theorem Th20:
for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`2 >= b
`2 & c`2 >= b`2 holds a = b or b = c or a`2 = b`2 & c`2 = b`2
proof
let a,b,c be Point of TOP-REAL 2 such that
A1: b in LSeg(a,c) and
A2: a`2 >= b`2 & c`2 >= b`2;
consider r such that
A3: b = (1-r)*a + r*c and
0 <= r and
r <= 1 by A1;
per cases by A2,XXREAL_0:1;
suppose that
A4: a`2 = b`2 and
A5: c`2 > b`2;
b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:2
.= ((1-r)*a)`2 + r*c`2 by TOPREAL3:4
.= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:4
.= b`2 + (r*c`2-r*b`2);
then
A6: 0 = r*(c`2-b`2);
c`2-b`2 > 0 by A5,XREAL_1:50;
then r = 0 by A6,XCMPLX_1:6;
then b = 1*a + 0.TOP-REAL 2 by A3,RLVECT_1:10
.= 1*a by RLVECT_1:4
.= a by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A7: a`2 > b`2 and
A8: c`2 = b`2;
b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:2
.= ((1-r)*a)`2 + r*c`2 by TOPREAL3:4
.= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:4;
then
A9: 0 = (1-r)*(a`2-b`2);
a`2-b`2 > 0 by A7,XREAL_1:50;
then 1 - r = 0 by A9,XCMPLX_1:6;
then b = 0.TOP-REAL 2 + 1*c by A3,RLVECT_1:10
.= 1*c by RLVECT_1:4
.= c by RLVECT_1:def 8;
hence thesis;
end;
suppose that
A10: a`2 > b`2 & c`2 > b`2;
a`2 >= c`2 or c`2 >= a`2;
hence thesis by A1,A10,TOPREAL1:4;
end;
suppose
a`2 = b`2 & c`2 = b`2;
hence thesis;
end;
end;
begin :: The area of a sequence
definition
let f, g be FinSequence of TOP-REAL 2;
pred g is_in_the_area_of f means
for n st n in dom g holds W-bound L~
f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <=
N-bound L~f;
end;
theorem Th21:
for f being non trivial FinSequence of TOP-REAL 2 holds f is_in_the_area_of f
proof
let f be non trivial FinSequence of TOP-REAL 2;
let n;
assume
A1: n in dom f;
len f >= 2 by NAT_D:60;
then f/.n in L~f by A1,GOBOARD1:1;
hence thesis by PSCOMP_1:24;
end;
theorem Th22:
for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of
f for i,j st i in dom g & j in dom g holds mid(g,i,j) is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2 such that
A1: for n st n in dom g holds W-bound L~f <= (g/.n)`1 & (g/.n)`1 <=
E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f;
let i,j such that
A2: i in dom g & j in dom g;
set h = mid(g,i,j);
per cases;
suppose
A3: i <= j;
let n;
assume n in dom h;
then n+i-'1 in dom g & h/.n = g/.(n+i-'1) by A2,A3,Th1,Th3;
hence thesis by A1;
end;
suppose
A4: i > j;
let n;
assume n in dom h;
then i -' n + 1 in dom g & h/.n = g/.(i -' n + 1) by A2,A4,Th2,Th4;
hence thesis by A1;
end;
end;
theorem
for f being non trivial FinSequence of TOP-REAL 2 for i,j st i in dom
f & j in dom f holds mid(f,i,j) is_in_the_area_of f by Th21,Th22;
theorem Th24:
for f,g,h being FinSequence of TOP-REAL 2 st g is_in_the_area_of
f & h is_in_the_area_of f holds g^h is_in_the_area_of f
proof
let f,g,h be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: h is_in_the_area_of f;
let n;
assume
A3: n in dom(g^h);
per cases by A3,FINSEQ_1:25;
suppose
A4: n in dom g;
then (g^h)/.n = g/.n by FINSEQ_4:68;
hence thesis by A1,A4;
end;
suppose
ex i be Nat st i in dom h & n = len g + i;
then consider i be Nat such that
A5: i in dom h and
A6: n = len g + i;
(g^h)/.n = h/.i by A5,A6,FINSEQ_4:69;
hence thesis by A2,A5;
end;
end;
theorem Th25:
for f being non trivial FinSequence of TOP-REAL 2 holds <*
NE-corner L~f*> is_in_the_area_of f
proof
let f be non trivial FinSequence of TOP-REAL 2;
set g = <*NE-corner L~f*>;
let n;
assume
A1: n in dom g;
dom g = {1} by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
then g/.n = |[E-bound L~f, N-bound L~f]| by FINSEQ_4:16;
then (g/.n)`1 = E-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:52;
hence thesis by SPRECT_1:21,22;
end;
theorem Th26:
for f being non trivial FinSequence of TOP-REAL 2 holds <*
NW-corner L~f*> is_in_the_area_of f
proof
let f be non trivial FinSequence of TOP-REAL 2;
set g = <*NW-corner L~f*>;
let n;
assume
A1: n in dom g;
dom g = {1} by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
then g/.n = |[W-bound L~f, N-bound L~f]| by FINSEQ_4:16;
then (g/.n)`1 = W-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:52;
hence thesis by SPRECT_1:21,22;
end;
theorem Th27:
for f being non trivial FinSequence of TOP-REAL 2 holds <*
SE-corner L~f*> is_in_the_area_of f
proof
let f be non trivial FinSequence of TOP-REAL 2;
set g = <*SE-corner L~f*>;
let n;
assume
A1: n in dom g;
dom g = {1} by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
then g/.n = |[E-bound L~f, S-bound L~f]| by FINSEQ_4:16;
then (g/.n)`1 = E-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:52;
hence thesis by SPRECT_1:21,22;
end;
theorem Th28:
for f being non trivial FinSequence of TOP-REAL 2 holds <*
SW-corner L~f*> is_in_the_area_of f
proof
let f be non trivial FinSequence of TOP-REAL 2;
set g = <*SW-corner L~f*>;
let n;
assume
A1: n in dom g;
dom g = {1} by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
then g/.n = |[W-bound L~f, S-bound L~f]| by FINSEQ_4:16;
then (g/.n)`1 = W-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:52;
hence thesis by SPRECT_1:21,22;
end;
begin :: Horizontal and vertical connections
definition
let f, g be FinSequence of TOP-REAL 2;
pred g is_a_h.c._for f means
g is_in_the_area_of f & (g/.1)`1 = W-bound L~f & (g/.len g)`1 = E-bound L~f;
pred g is_a_v.c._for f means
g is_in_the_area_of f & (g/.1)`2 = S-bound L~f & (g/.len g)`2 = N-bound L~f;
end;
theorem Th29:
for f being FinSequence of TOP-REAL 2, g,h being one-to-one
special FinSequence of TOP-REAL 2 st 2 <= len g & 2 <= len h & g is_a_h.c._for
f & h is_a_v.c._for f holds L~g meets L~h
proof
let f be FinSequence of TOP-REAL 2, g,h being one-to-one special FinSequence
of TOP-REAL 2 such that
A1: 2 <= len g & 2 <= len h and
A2: for n st n in dom g holds W-bound L~f <= (g/.n)`1 & (g/.n)`1 <=
E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f and
A3: (g/.1)`1 = W-bound L~f and
A4: (g/.len g)`1 = E-bound L~f and
A5: for n st n in dom h holds W-bound L~f <= (h/.n)`1 & (h/.n)`1 <=
E-bound L~f & S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f and
A6: (h/.1)`2 = S-bound L~f and
A7: (h/.len h)`2 = N-bound L~f;
reconsider g,h as non empty one-to-one special FinSequence of TOP-REAL 2 by
A1,CARD_1:27;
A8: X_axis(h) lies_between (X_axis(g)).1, (X_axis(g)).(len g)
proof
let n;
set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g), H = X_axis
h;
assume n in dom H;
then
A9: n in dom h & H.n = (h/.n)`1 by Th15,GOBOARD1:def 1;
1 in dom F by FINSEQ_5:6;
then r = W-bound L~f by A3,GOBOARD1:def 1;
hence r <= H.n by A5,A9;
len F = len g & len F in dom F by FINSEQ_5:6,GOBOARD1:def 1;
then s = E-bound L~f by A4,GOBOARD1:def 1;
hence thesis by A5,A9;
end;
A10: Y_axis(h) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h)
proof
let n;
set F = Y_axis h, r = (Y_axis h).1, s = (Y_axis h).(len h);
assume n in dom F;
then
A11: n in dom h & F.n = (h/.n)`2 by Th16,GOBOARD1:def 2;
1 in dom F by FINSEQ_5:6;
then r = S-bound L~f by A6,GOBOARD1:def 2;
hence r <= F.n by A5,A11;
len F = len h & len F in dom F by FINSEQ_5:6,GOBOARD1:def 2;
then s = N-bound L~f by A7,GOBOARD1:def 2;
hence thesis by A5,A11;
end;
A12: Y_axis(g) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h)
proof
let n;
set F = Y_axis(h), r = (Y_axis(h)).1, s = (Y_axis(h)).(len h), G = Y_axis
g;
assume n in dom G;
then
A13: n in dom g & G.n = (g/.n)`2 by Th16,GOBOARD1:def 2;
1 in dom F by FINSEQ_5:6;
then r = S-bound L~f by A6,GOBOARD1:def 2;
hence r <= G.n by A2,A13;
len F = len h & len F in dom F by FINSEQ_5:6,GOBOARD1:def 2;
then s = N-bound L~f by A7,GOBOARD1:def 2;
hence thesis by A2,A13;
end;
X_axis(g) lies_between (X_axis(g)).1, (X_axis(g)).(len g)
proof
let n;
set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g);
assume n in dom F;
then
A14: n in dom g & F.n = (g/.n)`1 by Th15,GOBOARD1:def 1;
1 in dom F by FINSEQ_5:6;
then r = W-bound L~f by A3,GOBOARD1:def 1;
hence r <= F.n by A2,A14;
len F = len g & len F in dom F by FINSEQ_5:6,GOBOARD1:def 1;
then s = E-bound L~f by A4,GOBOARD1:def 1;
hence thesis by A2,A14;
end;
hence thesis by A1,A8,A12,A10,GOBOARD4:5;
end;
begin :: Orientation
definition
let f be FinSequence of TOP-REAL 2;
attr f is clockwise_oriented means
(Rotate(f,N-min L~f))/.2 in N-most L~f;
end;
theorem Th30:
for f being non constant standard special_circular_sequence st f
/.1 = N-min L~f holds f is clockwise_oriented iff f/.2 in N-most L~f
by FINSEQ_6:89;
registration
cluster R^2-unit_square -> compact;
coherence by TOPREAL2:2;
end;
theorem Th31:
N-bound R^2-unit_square = 1
proof
set X = R^2-unit_square;
reconsider Z = (proj2|X).:(the carrier of (TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2)|X);
A2: for q being Real st for p being Real st p in Z holds p <=
q holds 1 <= q
proof
let q be Real such that
A3: for p being Real st p in Z holds p <= q;
|[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by RLTOPSP1:68;
then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
by XBOOLE_0:def 3;
then
A4: |[1,1]| in X by XBOOLE_0:def 3;
then (proj2|X). |[1,1]| = |[1,1]|`2 by PSCOMP_1:23
.= 1 by EUCLID:52;
hence thesis by A1,A3,A4,FUNCT_2:35;
end;
for p be Real st p in Z holds p <= 1
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A1,A5;
ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2
>= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 =
1 & q`2 <= 1 & q`2 >= 0) by A1,A5,TOPREAL1:14;
hence thesis by A1,A5,A6,PSCOMP_1:23;
end;
hence thesis by A2,SEQ_4:46;
end;
theorem Th32:
W-bound R^2-unit_square = 0
proof
set X = R^2-unit_square;
reconsider Z = (proj1|X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2)|X);
A2: for q be Real st for p be Real st p in Z holds p >= q
holds 0 >= q
proof
let q be Real such that
A3: for p be Real st p in Z holds p >= q;
|[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) by RLTOPSP1:68;
then |[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
by XBOOLE_0:def 3;
then
A4: |[0,0]| in X by XBOOLE_0:def 3;
then (proj1|X). |[0,0]| = |[0,0]|`1 by PSCOMP_1:22
.= 0 by EUCLID:52;
hence thesis by A1,A3,A4,FUNCT_2:35;
end;
for p be Real st p in Z holds p >= 0
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj1|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A1,A5;
ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2
>= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 =
1 & q`2 <= 1 & q`2 >= 0) by A1,A5,TOPREAL1:14;
hence thesis by A1,A5,A6,PSCOMP_1:22;
end;
hence thesis by A2,SEQ_4:44;
end;
theorem Th33:
E-bound R^2-unit_square = 1
proof
set X = R^2-unit_square;
reconsider Z = (proj1|X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2)|X);
A2: for q being Real st for p being Real st p in Z holds p <=
q holds 1 <= q
proof
let q be Real such that
A3: for p be Real st p in Z holds p <= q;
|[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by RLTOPSP1:68;
then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
by XBOOLE_0:def 3;
then
A4: |[1,1]| in X by XBOOLE_0:def 3;
then (proj1|X). |[1,1]| = |[1,1]|`1 by PSCOMP_1:22
.= 1 by EUCLID:52;
hence thesis by A1,A3,A4,FUNCT_2:35;
end;
for p be Real st p in Z holds p <= 1
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj1|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A1,A5;
ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2
>= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 =
1 & q`2 <= 1 & q`2 >= 0) by A1,A5,TOPREAL1:14;
hence thesis by A1,A5,A6,PSCOMP_1:22;
end;
hence thesis by A2,SEQ_4:46;
end;
theorem
S-bound R^2-unit_square = 0
proof
set X = R^2-unit_square;
reconsider Z = (proj2|X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2)|X);
A2: for q be Real st for p be Real st p in Z holds p >= q
holds 0 >= q
proof
let q be Real such that
A3: for p be Real st p in Z holds p >= q;
|[1,0]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by RLTOPSP1:68;
then |[1,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|)
by XBOOLE_0:def 3;
then
A4: |[1,0]| in X by XBOOLE_0:def 3;
then (proj2|X). |[1,0]| = |[1,0]|`2 by PSCOMP_1:23
.= 0 by EUCLID:52;
hence thesis by A1,A3,A4,FUNCT_2:35;
end;
for p be Real st p in Z holds p >= 0
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A1,A5;
ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2
>= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 =
1 & q`2 <= 1 & q`2 >= 0) by A1,A5,TOPREAL1:14;
hence thesis by A1,A5,A6,PSCOMP_1:23;
end;
hence thesis by A2,SEQ_4:44;
end;
theorem Th35:
N-most R^2-unit_square = LSeg(|[0,1]|,|[1,1]|)
proof
set X = R^2-unit_square;
LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) c= X & LSeg(|[0
,1]| ,|[1,1]|) c= LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|)
by XBOOLE_1:7;
hence thesis by Th31,Th32,Th33,XBOOLE_1:1,28;
end;
theorem
N-min R^2-unit_square = |[0,1]|
proof
lower_bound (proj1|LSeg(|[0,1]|,|[1,1]|)) = 0
proof
set X = LSeg(|[0,1]|,|[1,1]|);
reconsider Z = (proj1|X).:the carrier of ((TOP-REAL 2)|X) as Subset of
REAL;
A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2)|X);
A2: for p be Real st p in Z holds p >= 0
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A3: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A4: p = (proj1|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A1,A3;
|[0,1]|`1 = 0 & |[1,1]|`1 = 1 by EUCLID:52;
then p0`1 >= 0 by A1,A3,TOPREAL1:3;
hence thesis by A1,A3,A4,PSCOMP_1:22;
end;
for q be Real st for p be Real st p in Z holds p >= q
holds 0 >= q
proof
A5: (proj1|X). |[0,1]| = |[0,1]|`1 by PSCOMP_1:22,RLTOPSP1:68
.= 0 by EUCLID:52;
A6: |[0,1]| in X by RLTOPSP1:68;
let q be Real;
assume for p be Real st p in Z holds p >= q;
hence thesis by A1,A6,A5,FUNCT_2:35;
end;
hence thesis by A2,SEQ_4:44;
end;
hence thesis by Th31,Th35;
end;
registration
let X be non vertical non horizontal non empty compact Subset of TOP-REAL 2;
cluster SpStSeq X -> clockwise_oriented;
coherence
proof
set f = SpStSeq X;
f/.2 = N-max L~f by SPRECT_1:84;
then f/.1 = N-min L~f & f/.2 in N-most L~f by PSCOMP_1:42,SPRECT_1:83;
hence thesis by Th30;
end;
end;
registration
cluster clockwise_oriented for
non constant standard special_circular_sequence;
existence
proof
set X = the non vertical non horizontal non empty compact Subset of TOP-REAL 2;
take SpStSeq X;
thus thesis;
end;
end;
theorem Th37:
for f being non constant standard special_circular_sequence, i,j
st i > j & (1 < j & i <= len f or 1 <= j & i < len f) holds mid(f,i,j) is
S-Sequence_in_R2
proof
let f be non constant standard special_circular_sequence, i,j such that
A1: i > j and
A2: 1 < j & i <= len f or 1 <= j & i < len f;
A3: Rev mid(f,j,i) = mid(f,i,j) by FINSEQ_6:196;
per cases by A2;
suppose
1 < j & i <= len f;
then mid(f,j,i) is S-Sequence_in_R2 by A1,JORDAN4:40;
hence thesis by A3;
end;
suppose
A4: 1 <= j & i < len f;
then i+1 <= len f by NAT_1:13;
then mid(f,j,i) is S-Sequence_in_R2 by A1,A4,JORDAN4:39;
hence thesis by A3;
end;
end;
theorem Th38:
for f being non constant standard special_circular_sequence, i,j
st i < j & (1 < i & j <= len f or 1 <= i & j < len f) holds mid(f,i,j) is
S-Sequence_in_R2
proof
let f be non constant standard special_circular_sequence,i,j;
assume i < j &( 1 < i & j <= len f or 1 <= i & j < len f);
then mid(f,j,i) is S-Sequence_in_R2 by Th37;
then
Rev Rev mid(f,i,j) = mid(f,i,j) & Rev mid(f,i,j) is S-Sequence_in_R2 by
FINSEQ_6:196;
hence thesis;
end;
reserve f for non trivial FinSequence of TOP-REAL 2;
theorem Th39:
N-min L~f in rng f
proof
set p = N-min L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:11;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`2 <= N-bound L~f by PSCOMP_1:24;
A7: p`2 = N-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`2 <= N-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th18;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
then f/.(i+1) in N-most L~f by A1,A5,A7,Th10,GOBOARD1:1;
then
A11: (f/.(i+1))`1 >= p`1 by PSCOMP_1:39;
(f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1;
then
A12: (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A4,TOPREAL1:3;
f/.i in N-most L~f by A1,A8,A7,A10,Th10,GOBOARD1:1;
then (f/.i)`1 >= p`1 by PSCOMP_1:39;
then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th40:
N-max L~f in rng f
proof
set p = N-max L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:11;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`2 <= N-bound L~f by PSCOMP_1:24;
A7: p`2 = N-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`2 <= N-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th18;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
then f/.(i+1) in N-most L~f by A1,A5,A7,Th10,GOBOARD1:1;
then
A11: (f/.(i+1))`1 <= p`1 by PSCOMP_1:39;
(f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1;
then
A12: (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A4,TOPREAL1:3;
f/.i in N-most L~f by A1,A8,A7,A10,Th10,GOBOARD1:1;
then (f/.i)`1 <= p`1 by PSCOMP_1:39;
then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th41:
S-min L~f in rng f
proof
set p = S-min L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:12;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`2 >= S-bound L~f by PSCOMP_1:24;
A7: p`2 = S-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`2 >= S-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th20;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
then f/.(i+1) in S-most L~f by A1,A5,A7,Th11,GOBOARD1:1;
then
A11: (f/.(i+1))`1 >= p`1 by PSCOMP_1:55;
(f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1;
then
A12: (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A4,TOPREAL1:3;
f/.i in S-most L~f by A1,A8,A7,A10,Th11,GOBOARD1:1;
then (f/.i)`1 >= p`1 by PSCOMP_1:55;
then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th42:
S-max L~f in rng f
proof
set p = S-max L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:12;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`2 >= S-bound L~f by PSCOMP_1:24;
A7: p`2 = S-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`2 >= S-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th20;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2;
then f/.(i+1) in S-most L~f by A1,A5,A7,Th11,GOBOARD1:1;
then
A11: (f/.(i+1))`1 <= p`1 by PSCOMP_1:55;
(f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1;
then
A12: (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A4,TOPREAL1:3;
f/.i in S-most L~f by A1,A8,A7,A10,Th11,GOBOARD1:1;
then (f/.i)`1 <= p`1 by PSCOMP_1:55;
then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th43:
W-min L~f in rng f
proof
set p = W-min L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:13;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`1 >= W-bound L~f by PSCOMP_1:24;
A7: p`1 = W-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`1 >= W-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th19;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
then f/.(i+1) in W-most L~f by A1,A5,A7,Th12,GOBOARD1:1;
then
A11: (f/.(i+1))`2 >= p`2 by PSCOMP_1:31;
(f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2;
then
A12: (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A4,TOPREAL1:4;
f/.i in W-most L~f by A1,A8,A7,A10,Th12,GOBOARD1:1;
then (f/.i)`2 >= p`2 by PSCOMP_1:31;
then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th44:
W-max L~f in rng f
proof
set p = W-max L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:13;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`1 >= W-bound L~f by PSCOMP_1:24;
A7: p`1 = W-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`1 >= W-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th19;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
then f/.(i+1) in W-most L~f by A1,A5,A7,Th12,GOBOARD1:1;
then
A11: (f/.(i+1))`2 <= p`2 by PSCOMP_1:31;
(f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2;
then
A12: (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A4,TOPREAL1:4;
f/.i in W-most L~f by A1,A8,A7,A10,Th12,GOBOARD1:1;
then (f/.i)`2 <= p`2 by PSCOMP_1:31;
then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th45:
E-min L~f in rng f
proof
set p = E-min L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:14;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`1 <= E-bound L~f by PSCOMP_1:24;
A7: p`1 = E-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`1 <= E-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th17;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
then f/.(i+1) in E-most L~f by A1,A5,A7,Th13,GOBOARD1:1;
then
A11: (f/.(i+1))`2 >= p`2 by PSCOMP_1:47;
(f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2;
then
A12: (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A4,TOPREAL1:4;
f/.i in E-most L~f by A1,A8,A7,A10,Th13,GOBOARD1:1;
then (f/.i)`2 >= p`2 by PSCOMP_1:47;
then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
theorem Th46:
E-max L~f in rng f
proof
set p = E-max L~f;
A1: len f >= 2 by NAT_D:60;
consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
A4: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14,SPRECT_1:14;
i+1 >= 1 by NAT_1:11;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
then f/.(i+1) in L~f by A1,GOBOARD1:1;
then
A6: (f/.(i+1))`1 <= E-bound L~f by PSCOMP_1:24;
A7: p`1 = E-bound L~f by EUCLID:52;
i <= i+1 by NAT_1:11;
then i <= len f by A3,XXREAL_0:2;
then
A8: i in dom f by A2,FINSEQ_3:25;
then f/.i in L~f by A1,GOBOARD1:1;
then
A9: (f/.i)`1 <= E-bound L~f by PSCOMP_1:24;
now
per cases by A4,A9,A6,A7,Th17;
suppose
p = f/.i;
hence thesis by A8,PARTFUN2:2;
end;
suppose
p = f/.(i+1);
hence thesis by A5,PARTFUN2:2;
end;
suppose
A10: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1;
then f/.(i+1) in E-most L~f by A1,A5,A7,Th13,GOBOARD1:1;
then
A11: (f/.(i+1))`2 <= p`2 by PSCOMP_1:47;
(f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2;
then
A12: (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A4,TOPREAL1:4;
f/.i in E-most L~f by A1,A8,A7,A10,Th13,GOBOARD1:1;
then (f/.i)`2 <= p`2 by PSCOMP_1:47;
then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A11,A12,XXREAL_0:1;
then p = (f/.i) or p = (f/.(i+1)) by A10,TOPREAL3:6;
hence thesis by A8,A5,PARTFUN2:2;
end;
end;
hence thesis;
end;
reserve f for non constant standard special_circular_sequence;
theorem Th47:
1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n <
len f) implies L~mid(f,i,j) misses L~mid(f,m,n)
proof
assume that
A1: 1 <= i & i <= j and
A2: j < m and
A3: m <= n and
A4: n <= len f and
A5: 1 < i or n < len f;
set A = { LSeg(f,k): i <= k & k < j}, B = { LSeg(f,l): m <= l & l < n};
1 <= j by A1,XXREAL_0:2;
then 1 < m by A2,XXREAL_0:2;
then
A6: L~mid(f,m,n) = union B by A3,A4,Th14;
A7: for x,y being set st x in A & y in B holds x misses y
proof
let x,y be set;
assume x in A;
then consider k such that
A8: x = LSeg(f,k) and
A9: i <= k and
A10: k < j;
assume y in B;
then consider l such that
A11: y = LSeg(f,l) and
A12: m <= l and
A13: l < n;
A14: l < len f by A4,A13,XXREAL_0:2;
l+1 <= n by A13,NAT_1:13;
then
A15: k > 1 or l+1 < len f by A5,A9,XXREAL_0:2;
k+1 <= j by A10,NAT_1:13;
then k+1 < m by A2,XXREAL_0:2;
then k+1 < l by A12,XXREAL_0:2;
hence thesis by A8,A11,A14,A15,GOBOARD5:def 4;
end;
m <= len f by A3,A4,XXREAL_0:2;
then j < len f by A2,XXREAL_0:2;
then L~mid(f,i,j) = union A by A1,Th14;
hence thesis by A6,A7,ZFMISC_1:126;
end;
theorem Th48:
1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n <
len f) implies L~mid(f,i,j) misses L~mid(f,n,m)
proof
mid(f,n,m) = Rev mid(f,m,n) by FINSEQ_6:196;
then L~mid(f,n,m) = L~mid(f,m,n) by SPPOL_2:22;
hence thesis by Th47;
end;
theorem Th49:
1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n <
len f) implies L~mid(f,j,i) misses L~mid(f,n,m)
proof
mid(f,i,j) = Rev mid(f,j,i) by FINSEQ_6:196;
then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22;
hence thesis by Th48;
end;
theorem Th50:
1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n <
len f) implies L~mid(f,j,i) misses L~mid(f,m,n)
proof
mid(f,i,j) = Rev mid(f,j,i) by FINSEQ_6:196;
then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22;
hence thesis by Th47;
end;
theorem Th51:
(N-min L~f)`1 < (N-max L~f)`1
proof
set p = N-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:34;
A2: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
A3: p in rng f by Th39;
then
A4: i in dom f by FINSEQ_4:20;
then
A5: 1 <= i & i <= len f by FINSEQ_3:25;
A6: p = f.i by A3,FINSEQ_4:19
.= f/.i by A4,PARTFUN1:def 6;
A7: p`2 = N-bound L~f by EUCLID:52;
per cases by A5,XXREAL_0:1;
suppose
A8: i = 1 or i = len f;
then p = f/.1 by A6,FINSEQ_6:def 1;
then
A9: p in LSeg(f,1) by A2,TOPREAL1:21;
A10: 1+1 in dom f by A2,FINSEQ_3:25;
then
A11: f/.(1+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A12: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:21;
A13: len f -' 1+1 = len f by A1,XREAL_1:235,XXREAL_0:2;
then len f -' 1 > 3 by A1,XREAL_1:6;
then
A14: len f -' 1 > 1 by XXREAL_0:2;
then
A15: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,TOPREAL1:21;
len f -' 1 <= len f by A13,NAT_1:11;
then
A16: len f -' 1 in dom f by A14,FINSEQ_3:25;
then
A17: f/.(len f -' 1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A18: f/.1 = f/.len f by FINSEQ_6:def 1;
then
A19: p in LSeg(f,len f -' 1) by A6,A8,A13,A14,TOPREAL1:21;
A20: 1 in dom f by FINSEQ_5:6;
then
A21: p <> f/.(1+1) by A6,A8,A18,A10,GOBOARD7:29;
A22: len f in dom f by FINSEQ_5:6;
then
A23: p <> f/.(len f -' 1) by A6,A8,A18,A13,A16,GOBOARD7:29;
A24: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical)
proof
assume LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical;
then
A25: p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1 by A19,A9,A15,A12,
SPPOL_1:def 3;
A26: (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or (f/.(1+1))`2 >= (f/.(len f
-' 1))`2;
A27: p`2 >= (f/.(1+1))`2 & p`2 >= (f/.(len f -' 1))`2 by A7,A17,A11,
PSCOMP_1:24;
LSeg(f,1) = LSeg(f/.1,f/.(1+1)) & LSeg(f,len f -' 1) = LSeg(f/.1,f
/.(len f -' 1)) by A2,A18,A13,A14,TOPREAL1:def 3;
then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A6
,A8,A18,A25,A27,A26,GOBOARD7:7;
then f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in
LSeg(f,len f -' 1) /\ LSeg(f,1) by A15,A12,XBOOLE_0:def 4;
then
A28: LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A6,A8,A18,A23,A21,
TARSKI:def 1;
f.1 = f/.1 by A20,PARTFUN1:def 6;
hence contradiction by A28,JORDAN4:42;
end;
now
per cases by A24,SPPOL_1:19;
suppose
LSeg(f,len f -' 1) is horizontal;
then
A29: p`2 = (f/.(len f -' 1))`2 by A19,A15,SPPOL_1:def 2;
then
A30: f/.(len f -' 1) in N-most L~f by A2,A7,A16,Th10,GOBOARD1:1;
then
A31: (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:39;
(f/.(len f -' 1))`1 <> p`1 by A6,A8,A22,A18,A13,A16,A29,GOBOARD7:29
,TOPREAL3:6;
then
A32: (f/.(len f -' 1))`1 > p`1 by A31,XXREAL_0:1;
(f/.(len f -' 1))`1 <= (N-max L~f)`1 by A30,PSCOMP_1:39;
hence thesis by A32,XXREAL_0:2;
end;
suppose
LSeg(f,1) is horizontal;
then
A33: p`2 = (f/.(1+1))`2 by A9,A12,SPPOL_1:def 2;
then
A34: f/.(1+1) in N-most L~f by A2,A7,A10,Th10,GOBOARD1:1;
then
A35: (f/.(1+1))`1 >= p`1 by PSCOMP_1:39;
(f/.(1+1))`1 <> p`1 by A6,A8,A20,A18,A10,A33,GOBOARD7:29,TOPREAL3:6;
then
A36: (f/.(1+1))`1 > p`1 by A35,XXREAL_0:1;
(f/.(1+1))`1 <= (N-max L~f)`1 by A34,PSCOMP_1:39;
hence thesis by A36,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose that
A37: 1 < i and
A38: i < len f;
A39: i-'1+1 = i by A37,XREAL_1:235;
then
A40: i-'1 >= 1 by A37,NAT_1:13;
then
A41: f/.(i-'1) in LSeg(f,i-'1) by A38,A39,TOPREAL1:21;
i-'1 <= i by A39,NAT_1:11;
then i-'1 <= len f by A38,XXREAL_0:2;
then
A42: i-'1 in dom f by A40,FINSEQ_3:25;
then
A43: f/.(i-'1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A44: i+1 <= len f by A38,NAT_1:13;
then
A45: f/.(i+1) in LSeg(f,i) by A37,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A46: i+1 in dom f by A44,FINSEQ_3:25;
then
A47: f/.(i+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A48: p <> f/.(i+1) by A3,A6,A46,FINSEQ_4:20,GOBOARD7:29;
A49: p in LSeg(f,i) by A6,A37,A44,TOPREAL1:21;
A50: p in LSeg(f,i-'1) by A6,A38,A39,A40,TOPREAL1:21;
A51: p <> f/.(i-'1) by A4,A6,A39,A42,GOBOARD7:29;
A52: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical;
then
A53: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A50,A49,A41,A45,SPPOL_1:def 3
;
A54: (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
A55: p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2 by A7,A43,A47,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A37,A38,A39,A40,A44,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A6,A53,A55,A54
,GOBOARD7:7;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
/\ LSeg(f,i) by A41,A45,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A6
,A51,A48,TARSKI:def 1;
hence contradiction by A39,A40,A44,TOPREAL1:def 6;
end;
now
per cases by A52,SPPOL_1:19;
suppose
LSeg(f,i-'1) is horizontal;
then
A56: p`2 = (f/.(i-'1))`2 by A50,A41,SPPOL_1:def 2;
then
A57: f/.(i-'1) in N-most L~f by A2,A7,A42,Th10,GOBOARD1:1;
then
A58: (f/.(i-'1))`1 >= p`1 by PSCOMP_1:39;
(f/.(i-'1))`1 <> p`1 by A4,A6,A39,A42,A56,GOBOARD7:29,TOPREAL3:6;
then
A59: (f/.(i-'1))`1 > p`1 by A58,XXREAL_0:1;
(f/.(i-'1))`1 <= (N-max L~f)`1 by A57,PSCOMP_1:39;
hence thesis by A59,XXREAL_0:2;
end;
suppose
LSeg(f,i) is horizontal;
then
A60: p`2 = (f/.(i+1))`2 by A49,A45,SPPOL_1:def 2;
then
A61: f/.(i+1) in N-most L~f by A2,A7,A46,Th10,GOBOARD1:1;
then
A62: (f/.(i+1))`1 >= p`1 by PSCOMP_1:39;
(f/.(i+1))`1 <> p`1 by A4,A6,A46,A60,GOBOARD7:29,TOPREAL3:6;
then
A63: (f/.(i+1))`1 > p`1 by A62,XXREAL_0:1;
(f/.(i+1))`1 <= (N-max L~f)`1 by A61,PSCOMP_1:39;
hence thesis by A63,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
theorem Th52:
N-min L~f <> N-max L~f
proof
(N-min L~f)`1 < (N-max L~f)`1 by Th51;
hence thesis;
end;
theorem Th53:
(E-min L~f)`2 < (E-max L~f)`2
proof
set p = E-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:34;
A2: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
A3: p in rng f by Th45;
then
A4: i in dom f by FINSEQ_4:20;
then
A5: 1 <= i & i <= len f by FINSEQ_3:25;
A6: p = f.i by A3,FINSEQ_4:19
.= f/.i by A4,PARTFUN1:def 6;
A7: p`1 = E-bound L~f by EUCLID:52;
per cases by A5,XXREAL_0:1;
suppose
A8: i = 1 or i = len f;
then p = f/.1 by A6,FINSEQ_6:def 1;
then
A9: p in LSeg(f,1) by A2,TOPREAL1:21;
A10: 1+1 in dom f by A2,FINSEQ_3:25;
then
A11: f/.(1+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A12: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:21;
A13: len f -' 1+1 = len f by A1,XREAL_1:235,XXREAL_0:2;
then len f -' 1 > 3 by A1,XREAL_1:6;
then
A14: len f -' 1 > 1 by XXREAL_0:2;
then
A15: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,TOPREAL1:21;
len f -' 1 <= len f by A13,NAT_1:11;
then
A16: len f -' 1 in dom f by A14,FINSEQ_3:25;
then
A17: f/.(len f -' 1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A18: f/.1 = f/.len f by FINSEQ_6:def 1;
then
A19: p in LSeg(f,len f -' 1) by A6,A8,A13,A14,TOPREAL1:21;
A20: 1 in dom f by FINSEQ_5:6;
then
A21: p <> f/.(1+1) by A6,A8,A18,A10,GOBOARD7:29;
A22: len f in dom f by FINSEQ_5:6;
then
A23: p <> f/.(len f -' 1) by A6,A8,A18,A13,A16,GOBOARD7:29;
A24: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal)
proof
assume LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal;
then
A25: p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2 by A19,A9,A15,A12,
SPPOL_1:def 2;
A26: (f/.(1+1))`1 <= (f/.(len f -' 1))`1 or (f/.(1+1))`1 >= (f/.(len f
-' 1))`1;
A27: p`1 >= (f/.(1+1))`1 & p`1 >= (f/.(len f -' 1))`1 by A7,A17,A11,
PSCOMP_1:24;
LSeg(f,1) = LSeg(f/.1,f/.(1+1)) & LSeg(f,len f -' 1) = LSeg(f/.1,f
/.(len f -' 1)) by A2,A18,A13,A14,TOPREAL1:def 3;
then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A6
,A8,A18,A25,A27,A26,GOBOARD7:8;
then f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in
LSeg(f,len f -' 1) /\ LSeg(f,1) by A15,A12,XBOOLE_0:def 4;
then
A28: LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A6,A8,A18,A23,A21,
TARSKI:def 1;
f.1 = f/.1 by A20,PARTFUN1:def 6;
hence contradiction by A28,JORDAN4:42;
end;
now
per cases by A24,SPPOL_1:19;
suppose
LSeg(f,len f -' 1) is vertical;
then
A29: p`1 = (f/.(len f -' 1))`1 by A19,A15,SPPOL_1:def 3;
then
A30: f/.(len f -' 1) in E-most L~f by A2,A7,A16,Th13,GOBOARD1:1;
then
A31: (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:47;
(f/.(len f -' 1))`2 <> p`2 by A6,A8,A22,A18,A13,A16,A29,GOBOARD7:29
,TOPREAL3:6;
then
A32: (f/.(len f -' 1))`2 > p`2 by A31,XXREAL_0:1;
(f/.(len f -' 1))`2 <= (E-max L~f)`2 by A30,PSCOMP_1:47;
hence thesis by A32,XXREAL_0:2;
end;
suppose
LSeg(f,1) is vertical;
then
A33: p`1 = (f/.(1+1))`1 by A9,A12,SPPOL_1:def 3;
then
A34: f/.(1+1) in E-most L~f by A2,A7,A10,Th13,GOBOARD1:1;
then
A35: (f/.(1+1))`2 >= p`2 by PSCOMP_1:47;
(f/.(1+1))`2 <> p`2 by A6,A8,A20,A18,A10,A33,GOBOARD7:29,TOPREAL3:6;
then
A36: (f/.(1+1))`2 > p`2 by A35,XXREAL_0:1;
(f/.(1+1))`2 <= (E-max L~f)`2 by A34,PSCOMP_1:47;
hence thesis by A36,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose that
A37: 1 < i and
A38: i < len f;
A39: i-'1+1 = i by A37,XREAL_1:235;
then
A40: i-'1 >= 1 by A37,NAT_1:13;
then
A41: f/.(i-'1) in LSeg(f,i-'1) by A38,A39,TOPREAL1:21;
i-'1 <= i by A39,NAT_1:11;
then i-'1 <= len f by A38,XXREAL_0:2;
then
A42: i-'1 in dom f by A40,FINSEQ_3:25;
then
A43: f/.(i-'1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A44: i+1 <= len f by A38,NAT_1:13;
then
A45: f/.(i+1) in LSeg(f,i) by A37,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A46: i+1 in dom f by A44,FINSEQ_3:25;
then
A47: f/.(i+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A48: p <> f/.(i+1) by A3,A6,A46,FINSEQ_4:20,GOBOARD7:29;
A49: p in LSeg(f,i) by A6,A37,A44,TOPREAL1:21;
A50: p in LSeg(f,i-'1) by A6,A38,A39,A40,TOPREAL1:21;
A51: p <> f/.(i-'1) by A4,A6,A39,A42,GOBOARD7:29;
A52: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal;
then
A53: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A50,A49,A41,A45,SPPOL_1:def 2
;
A54: (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
A55: p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1 by A7,A43,A47,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A37,A38,A39,A40,A44,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A6,A53,A55,A54
,GOBOARD7:8;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
/\ LSeg(f,i) by A41,A45,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A6
,A51,A48,TARSKI:def 1;
hence contradiction by A39,A40,A44,TOPREAL1:def 6;
end;
now
per cases by A52,SPPOL_1:19;
suppose
LSeg(f,i-'1) is vertical;
then
A56: p`1 = (f/.(i-'1))`1 by A50,A41,SPPOL_1:def 3;
then
A57: f/.(i-'1) in E-most L~f by A2,A7,A42,Th13,GOBOARD1:1;
then
A58: (f/.(i-'1))`2 >= p`2 by PSCOMP_1:47;
(f/.(i-'1))`2 <> p`2 by A4,A6,A39,A42,A56,GOBOARD7:29,TOPREAL3:6;
then
A59: (f/.(i-'1))`2 > p`2 by A58,XXREAL_0:1;
(f/.(i-'1))`2 <= (E-max L~f)`2 by A57,PSCOMP_1:47;
hence thesis by A59,XXREAL_0:2;
end;
suppose
LSeg(f,i) is vertical;
then
A60: p`1 = (f/.(i+1))`1 by A49,A45,SPPOL_1:def 3;
then
A61: f/.(i+1) in E-most L~f by A2,A7,A46,Th13,GOBOARD1:1;
then
A62: (f/.(i+1))`2 >= p`2 by PSCOMP_1:47;
(f/.(i+1))`2 <> p`2 by A4,A6,A46,A60,GOBOARD7:29,TOPREAL3:6;
then
A63: (f/.(i+1))`2 > p`2 by A62,XXREAL_0:1;
(f/.(i+1))`2 <= (E-max L~f)`2 by A61,PSCOMP_1:47;
hence thesis by A63,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
theorem
E-min L~f <> E-max L~f
proof
(E-min L~f)`2 < (E-max L~f)`2 by Th53;
hence thesis;
end;
theorem Th55:
(S-min L~f)`1 < (S-max L~f)`1
proof
set p = S-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:34;
A2: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
A3: p in rng f by Th41;
then
A4: i in dom f by FINSEQ_4:20;
then
A5: 1 <= i & i <= len f by FINSEQ_3:25;
A6: p = f.i by A3,FINSEQ_4:19
.= f/.i by A4,PARTFUN1:def 6;
A7: p`2 = S-bound L~f by EUCLID:52;
per cases by A5,XXREAL_0:1;
suppose
A8: i = 1 or i = len f;
then p = f/.1 by A6,FINSEQ_6:def 1;
then
A9: p in LSeg(f,1) by A2,TOPREAL1:21;
A10: 1+1 in dom f by A2,FINSEQ_3:25;
then
A11: f/.(1+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A12: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:21;
A13: len f -' 1+1 = len f by A1,XREAL_1:235,XXREAL_0:2;
then len f -' 1 > 3 by A1,XREAL_1:6;
then
A14: len f -' 1 > 1 by XXREAL_0:2;
then
A15: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,TOPREAL1:21;
len f -' 1 <= len f by A13,NAT_1:11;
then
A16: len f -' 1 in dom f by A14,FINSEQ_3:25;
then
A17: f/.(len f -' 1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A18: f/.1 = f/.len f by FINSEQ_6:def 1;
then
A19: p in LSeg(f,len f -' 1) by A6,A8,A13,A14,TOPREAL1:21;
A20: 1 in dom f by FINSEQ_5:6;
then
A21: p <> f/.(1+1) by A6,A8,A18,A10,GOBOARD7:29;
A22: len f in dom f by FINSEQ_5:6;
then
A23: p <> f/.(len f -' 1) by A6,A8,A18,A13,A16,GOBOARD7:29;
A24: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical)
proof
assume LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical;
then
A25: p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1 by A19,A9,A15,A12,
SPPOL_1:def 3;
A26: (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or (f/.(1+1))`2 >= (f/.(len f
-' 1))`2;
A27: p`2 <= (f/.(1+1))`2 & p`2 <= (f/.(len f -' 1))`2 by A7,A17,A11,
PSCOMP_1:24;
LSeg(f,1) = LSeg(f/.1,f/.(1+1)) & LSeg(f,len f -' 1) = LSeg(f/.1,f
/.(len f -' 1)) by A2,A18,A13,A14,TOPREAL1:def 3;
then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A6
,A8,A18,A25,A27,A26,GOBOARD7:7;
then f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in
LSeg(f,len f -' 1) /\ LSeg(f,1) by A15,A12,XBOOLE_0:def 4;
then
A28: LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A6,A8,A18,A23,A21,
TARSKI:def 1;
f.1 = f/.1 by A20,PARTFUN1:def 6;
hence contradiction by A28,JORDAN4:42;
end;
now
per cases by A24,SPPOL_1:19;
suppose
LSeg(f,len f -' 1) is horizontal;
then
A29: p`2 = (f/.(len f -' 1))`2 by A19,A15,SPPOL_1:def 2;
then
A30: f/.(len f -' 1) in S-most L~f by A2,A7,A16,Th11,GOBOARD1:1;
then
A31: (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:55;
(f/.(len f -' 1))`1 <> p`1 by A6,A8,A22,A18,A13,A16,A29,GOBOARD7:29
,TOPREAL3:6;
then
A32: (f/.(len f -' 1))`1 > p`1 by A31,XXREAL_0:1;
(f/.(len f -' 1))`1 <= (S-max L~f)`1 by A30,PSCOMP_1:55;
hence thesis by A32,XXREAL_0:2;
end;
suppose
LSeg(f,1) is horizontal;
then
A33: p`2 = (f/.(1+1))`2 by A9,A12,SPPOL_1:def 2;
then
A34: f/.(1+1) in S-most L~f by A2,A7,A10,Th11,GOBOARD1:1;
then
A35: (f/.(1+1))`1 >= p`1 by PSCOMP_1:55;
(f/.(1+1))`1 <> p`1 by A6,A8,A20,A18,A10,A33,GOBOARD7:29,TOPREAL3:6;
then
A36: (f/.(1+1))`1 > p`1 by A35,XXREAL_0:1;
(f/.(1+1))`1 <= (S-max L~f)`1 by A34,PSCOMP_1:55;
hence thesis by A36,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose that
A37: 1 < i and
A38: i < len f;
A39: i-'1+1 = i by A37,XREAL_1:235;
then
A40: i-'1 >= 1 by A37,NAT_1:13;
then
A41: f/.(i-'1) in LSeg(f,i-'1) by A38,A39,TOPREAL1:21;
i-'1 <= i by A39,NAT_1:11;
then i-'1 <= len f by A38,XXREAL_0:2;
then
A42: i-'1 in dom f by A40,FINSEQ_3:25;
then
A43: f/.(i-'1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A44: i+1 <= len f by A38,NAT_1:13;
then
A45: f/.(i+1) in LSeg(f,i) by A37,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A46: i+1 in dom f by A44,FINSEQ_3:25;
then
A47: f/.(i+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A48: p <> f/.(i+1) by A3,A6,A46,FINSEQ_4:20,GOBOARD7:29;
A49: p in LSeg(f,i) by A6,A37,A44,TOPREAL1:21;
A50: p in LSeg(f,i-'1) by A6,A38,A39,A40,TOPREAL1:21;
A51: p <> f/.(i-'1) by A4,A6,A39,A42,GOBOARD7:29;
A52: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical)
proof
assume LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical;
then
A53: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A50,A49,A41,A45,SPPOL_1:def 3
;
A54: (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2;
A55: p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2 by A7,A43,A47,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A37,A38,A39,A40,A44,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A6,A53,A55,A54
,GOBOARD7:7;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
/\ LSeg(f,i) by A41,A45,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A6
,A51,A48,TARSKI:def 1;
hence contradiction by A39,A40,A44,TOPREAL1:def 6;
end;
now
per cases by A52,SPPOL_1:19;
suppose
LSeg(f,i-'1) is horizontal;
then
A56: p`2 = (f/.(i-'1))`2 by A50,A41,SPPOL_1:def 2;
then
A57: f/.(i-'1) in S-most L~f by A2,A7,A42,Th11,GOBOARD1:1;
then
A58: (f/.(i-'1))`1 >= p`1 by PSCOMP_1:55;
(f/.(i-'1))`1 <> p`1 by A4,A6,A39,A42,A56,GOBOARD7:29,TOPREAL3:6;
then
A59: (f/.(i-'1))`1 > p`1 by A58,XXREAL_0:1;
(f/.(i-'1))`1 <= (S-max L~f)`1 by A57,PSCOMP_1:55;
hence thesis by A59,XXREAL_0:2;
end;
suppose
LSeg(f,i) is horizontal;
then
A60: p`2 = (f/.(i+1))`2 by A49,A45,SPPOL_1:def 2;
then
A61: f/.(i+1) in S-most L~f by A2,A7,A46,Th11,GOBOARD1:1;
then
A62: (f/.(i+1))`1 >= p`1 by PSCOMP_1:55;
(f/.(i+1))`1 <> p`1 by A4,A6,A46,A60,GOBOARD7:29,TOPREAL3:6;
then
A63: (f/.(i+1))`1 > p`1 by A62,XXREAL_0:1;
(f/.(i+1))`1 <= (S-max L~f)`1 by A61,PSCOMP_1:55;
hence thesis by A63,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
theorem Th56:
S-min L~f <> S-max L~f
proof
(S-min L~f)`1 < (S-max L~f)`1 by Th55;
hence thesis;
end;
theorem Th57:
(W-min L~f)`2 < (W-max L~f)`2
proof
set p = W-min L~f, i = p..f;
A1: len f > 3+1 by GOBOARD7:34;
A2: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
A3: p in rng f by Th43;
then
A4: i in dom f by FINSEQ_4:20;
then
A5: 1 <= i & i <= len f by FINSEQ_3:25;
A6: p = f.i by A3,FINSEQ_4:19
.= f/.i by A4,PARTFUN1:def 6;
A7: p`1 = W-bound L~f by EUCLID:52;
per cases by A5,XXREAL_0:1;
suppose
A8: i = 1 or i = len f;
then p = f/.1 by A6,FINSEQ_6:def 1;
then
A9: p in LSeg(f,1) by A2,TOPREAL1:21;
A10: 1+1 in dom f by A2,FINSEQ_3:25;
then
A11: f/.(1+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A12: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:21;
A13: len f -' 1+1 = len f by A1,XREAL_1:235,XXREAL_0:2;
then len f -' 1 > 3 by A1,XREAL_1:6;
then
A14: len f -' 1 > 1 by XXREAL_0:2;
then
A15: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,TOPREAL1:21;
len f -' 1 <= len f by A13,NAT_1:11;
then
A16: len f -' 1 in dom f by A14,FINSEQ_3:25;
then
A17: f/.(len f -' 1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A18: f/.1 = f/.len f by FINSEQ_6:def 1;
then
A19: p in LSeg(f,len f -' 1) by A6,A8,A13,A14,TOPREAL1:21;
A20: 1 in dom f by FINSEQ_5:6;
then
A21: p <> f/.(1+1) by A6,A8,A18,A10,GOBOARD7:29;
A22: len f in dom f by FINSEQ_5:6;
then
A23: p <> f/.(len f -' 1) by A6,A8,A18,A13,A16,GOBOARD7:29;
A24: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal)
proof
assume LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal;
then
A25: p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2 by A19,A9,A15,A12,
SPPOL_1:def 2;
A26: (f/.(1+1))`1 <= (f/.(len f -' 1))`1 or (f/.(1+1))`1 >= (f/.(len f
-' 1))`1;
A27: p`1 <= (f/.(1+1))`1 & p`1 <= (f/.(len f -' 1))`1 by A7,A17,A11,
PSCOMP_1:24;
LSeg(f,1) = LSeg(f/.1,f/.(1+1)) & LSeg(f,len f -' 1) = LSeg(f/.1,f
/.(len f -' 1)) by A2,A18,A13,A14,TOPREAL1:def 3;
then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A6
,A8,A18,A25,A27,A26,GOBOARD7:8;
then f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in
LSeg(f,len f -' 1) /\ LSeg(f,1) by A15,A12,XBOOLE_0:def 4;
then
A28: LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A6,A8,A18,A23,A21,
TARSKI:def 1;
f.1 = f/.1 by A20,PARTFUN1:def 6;
hence contradiction by A28,JORDAN4:42;
end;
now
per cases by A24,SPPOL_1:19;
suppose
LSeg(f,len f -' 1) is vertical;
then
A29: p`1 = (f/.(len f -' 1))`1 by A19,A15,SPPOL_1:def 3;
then
A30: f/.(len f -' 1) in W-most L~f by A2,A7,A16,Th12,GOBOARD1:1;
then
A31: (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:31;
(f/.(len f -' 1))`2 <> p`2 by A6,A8,A22,A18,A13,A16,A29,GOBOARD7:29
,TOPREAL3:6;
then
A32: (f/.(len f -' 1))`2 > p`2 by A31,XXREAL_0:1;
(f/.(len f -' 1))`2 <= (W-max L~f)`2 by A30,PSCOMP_1:31;
hence thesis by A32,XXREAL_0:2;
end;
suppose
LSeg(f,1) is vertical;
then
A33: p`1 = (f/.(1+1))`1 by A9,A12,SPPOL_1:def 3;
then
A34: f/.(1+1) in W-most L~f by A2,A7,A10,Th12,GOBOARD1:1;
then
A35: (f/.(1+1))`2 >= p`2 by PSCOMP_1:31;
(f/.(1+1))`2 <> p`2 by A6,A8,A20,A18,A10,A33,GOBOARD7:29,TOPREAL3:6;
then
A36: (f/.(1+1))`2 > p`2 by A35,XXREAL_0:1;
(f/.(1+1))`2 <= (W-max L~f)`2 by A34,PSCOMP_1:31;
hence thesis by A36,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose that
A37: 1 < i and
A38: i < len f;
A39: i-'1+1 = i by A37,XREAL_1:235;
then
A40: i-'1 >= 1 by A37,NAT_1:13;
then
A41: f/.(i-'1) in LSeg(f,i-'1) by A38,A39,TOPREAL1:21;
i-'1 <= i by A39,NAT_1:11;
then i-'1 <= len f by A38,XXREAL_0:2;
then
A42: i-'1 in dom f by A40,FINSEQ_3:25;
then
A43: f/.(i-'1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A44: i+1 <= len f by A38,NAT_1:13;
then
A45: f/.(i+1) in LSeg(f,i) by A37,TOPREAL1:21;
i+1 >= 1 by NAT_1:11;
then
A46: i+1 in dom f by A44,FINSEQ_3:25;
then
A47: f/.(i+1) in L~f by A1,GOBOARD1:1,XXREAL_0:2;
A48: p <> f/.(i+1) by A3,A6,A46,FINSEQ_4:20,GOBOARD7:29;
A49: p in LSeg(f,i) by A6,A37,A44,TOPREAL1:21;
A50: p in LSeg(f,i-'1) by A6,A38,A39,A40,TOPREAL1:21;
A51: p <> f/.(i-'1) by A4,A6,A39,A42,GOBOARD7:29;
A52: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal)
proof
assume LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal;
then
A53: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A50,A49,A41,A45,SPPOL_1:def 2
;
A54: (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1;
A55: p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1 by A7,A43,A47,PSCOMP_1:24;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) & LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1
)) by A37,A38,A39,A40,A44,TOPREAL1:def 3;
then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A6,A53,A55,A54
,GOBOARD7:8;
then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1)
/\ LSeg(f,i) by A41,A45,XBOOLE_0:def 4;
then i-'1+1+1 = i-'1+(1+1) & LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A6
,A51,A48,TARSKI:def 1;
hence contradiction by A39,A40,A44,TOPREAL1:def 6;
end;
now
per cases by A52,SPPOL_1:19;
suppose
LSeg(f,i-'1) is vertical;
then
A56: p`1 = (f/.(i-'1))`1 by A50,A41,SPPOL_1:def 3;
then
A57: f/.(i-'1) in W-most L~f by A2,A7,A42,Th12,GOBOARD1:1;
then
A58: (f/.(i-'1))`2 >= p`2 by PSCOMP_1:31;
(f/.(i-'1))`2 <> p`2 by A4,A6,A39,A42,A56,GOBOARD7:29,TOPREAL3:6;
then
A59: (f/.(i-'1))`2 > p`2 by A58,XXREAL_0:1;
(f/.(i-'1))`2 <= (W-max L~f)`2 by A57,PSCOMP_1:31;
hence thesis by A59,XXREAL_0:2;
end;
suppose
LSeg(f,i) is vertical;
then
A60: p`1 = (f/.(i+1))`1 by A49,A45,SPPOL_1:def 3;
then
A61: f/.(i+1) in W-most L~f by A2,A7,A46,Th12,GOBOARD1:1;
then
A62: (f/.(i+1))`2 >= p`2 by PSCOMP_1:31;
(f/.(i+1))`2 <> p`2 by A4,A6,A46,A60,GOBOARD7:29,TOPREAL3:6;
then
A63: (f/.(i+1))`2 > p`2 by A62,XXREAL_0:1;
(f/.(i+1))`2 <= (W-max L~f)`2 by A61,PSCOMP_1:31;
hence thesis by A63,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
theorem Th58:
W-min L~f <> W-max L~f
proof
(W-min L~f)`2 < (W-max L~f)`2 by Th57;
hence thesis;
end;
theorem Th59:
LSeg(NW-corner L~f,N-min L~f) misses LSeg(N-max L~f,NE-corner L~ f)
proof
A1: (N-min L~f)`2 = (N-max L~f)`2 by PSCOMP_1:37;
assume LSeg(NW-corner L~f,N-min L~f) meets LSeg(N-max L~f,NE-corner L~f);
then consider p being object such that
A2: p in LSeg(NW-corner L~f,N-min L~f) and
A3: p in LSeg(N-max L~f,NE-corner L~f) by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A2;
(N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:38;
then
A4: (N-max L~f)`1 <= p`1 by A3,TOPREAL1:3;
(NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:38;
then p`1 <= (N-min L~f)`1 by A2,TOPREAL1:3;
then
A5: (N-min L~f)`1 >= (N-max L~f)`1 by A4,XXREAL_0:2;
(N-min L~f)`1 <= (N-max L~f)`1 by PSCOMP_1:38;
then (N-min L~f)`1 = (N-max L~f)`1 by A5,XXREAL_0:1;
hence contradiction by A1,Th52,TOPREAL3:6;
end;
theorem Th60:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p <> f/.1 & (p`1 = (f/.1)`1 or p`2 = (f/.1)`2) & LSeg(p
,f/.1) /\ L~f = {f/.1} holds <*p*>^f is S-Sequence_in_R2
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: p <> f/.1 and
A3: p`1 = (f/.1)`1 or p`2 = (f/.1)`2 and
A4: LSeg(p,f/.1) /\ L~f = {f/.1};
reconsider f as S-Sequence_in_R2 by A1;
A5: len f >= 1+1 by TOPREAL1:def 8;
then
A6: f/.1 in LSeg(f,1) by TOPREAL1:21;
set g = <*p*>^f;
len g = len<*p*> + len f by FINSEQ_1:22;
then len g >= len f by NAT_1:11;
then
A7: len g >= 2 by A5,XXREAL_0:2;
now
assume
A8: p in rng f;
rng f c= L~f & p in LSeg(p,f/.1) by A5,RLTOPSP1:68,SPPOL_2:18;
then p in {f/.1} by A4,A8,XBOOLE_0:def 4;
hence contradiction by A2,TARSKI:def 1;
end;
then {p} misses rng f by ZFMISC_1:50;
then <*p*> is one-to-one & rng<*p*> misses rng f by FINSEQ_1:39,FINSEQ_3:93;
then
A9: g is one-to-one by FINSEQ_3:91;
L~<*p*> = {} by SPPOL_2:12;
then L~<*p*> /\ L~f = {};
then
A10: L~<*p*> misses L~f;
A11: 1 in dom f by FINSEQ_5:6;
A12: now
let i such that
A13: 1+1<=i and
A14: i+1 <= len f;
A15: 2 in dom f by A5,FINSEQ_3:25;
now
assume f/.1 in LSeg(f,i);
then
A16: f/.1 in LSeg(f,1) /\ LSeg(f,i) by A6,XBOOLE_0:def 4;
then
A17: LSeg(f,1) meets LSeg(f,i);
now
per cases by A13,XXREAL_0:1;
case
A18: i = 1+1;
then LSeg(f,1) /\ LSeg(f,1+1) = {f/.2} by A14,TOPREAL1:def 6;
hence f/.1 = f/.2 by A16,A18,TARSKI:def 1;
end;
case
i > 1+1;
hence contradiction by A17,TOPREAL1:def 7;
end;
end;
then f.1 = f/.2 by A11,PARTFUN1:def 6
.= f.2 by A15,PARTFUN1:def 6;
hence contradiction by A11,A15,FUNCT_1:def 4;
end;
then not f/.1 in LSeg(f,i) /\ LSeg(p,f/.1) by XBOOLE_0:def 4;
then
A19: LSeg(f,i) /\ LSeg(p,f/.1) <> {f/.1} by TARSKI:def 1;
LSeg(f,i) /\ LSeg(p,f/.1) c= {f/.1} by A4,TOPREAL3:19,XBOOLE_1:26;
then LSeg(f,i) /\ LSeg(p,f/.1) = {} by A19,ZFMISC_1:33;
hence LSeg(f,i) misses LSeg(p,f/.1);
end;
A20: len<*p*> = 1 by FINSEQ_1:39;
then
A21: <*p*> is s.n.c. & <*p*>/.len <*p*> = p by FINSEQ_4:16,SPPOL_2:33;
A22: now
let i such that
1<=i;
A23: 2 <= i+2 by NAT_1:11;
assume i+2 <= len <*p*>;
hence LSeg(<*p*>,i) misses LSeg(p,f/.1) by A20,A23,XXREAL_0:2;
end;
LSeg(p,f/.1) /\ LSeg(f,1) = {f/.1} by A4,A6,TOPREAL3:19,ZFMISC_1:124;
then g is unfolded s.n.c. special by A3,A21,A10,A22,A12,GOBOARD2:8,SPPOL_2:29
,36;
hence thesis by A9,A7,TOPREAL1:def 8;
end;
theorem Th61:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p <> f/.len f & (p`1 = (f/.len f)`1 or p`2 = (f/.len f)
`2) & LSeg(p,f/.len f) /\ L~f = {f/.len f} holds f^<*p*> is S-Sequence_in_R2
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: p <> f/.len f &( p`1 = (f/.len f)`1 or p`2 = (f/.len f)`2) and
A3: LSeg(p,f/.len f) /\ L~f = {f/.len f};
set g = <*f/.len f,p*>;
A4: g is being_S-Seq by A2,SPPOL_2:43;
AB: len g = 1+1 by FINSEQ_1:44; then
AA: 2 in dom g by FINSEQ_3:25;
then
A5: mid(g,2,len g) = <*g.2*> by FINSEQ_6:193,AB
.= <*g/.2*> by AA,PARTFUN1:def 6
.= <*p*> by FINSEQ_4:17;
reconsider f9 = f as S-Sequence_in_R2 by A1;
A6: len f9 in dom f9 by FINSEQ_5:6;
A7: g.1 = f/.len f
.= f.len f by A6,PARTFUN1:def 6;
L~f /\ L~g ={ f/.len f } by A3,SPPOL_2:21
.={f.len f} by A6,PARTFUN1:def 6;
hence thesis by A1,A7,A4,A5,JORDAN3:38;
end;
begin :: Appending corners
theorem Th62:
for i,j st i in dom f & j in dom f & mid(f,i,j) is
S-Sequence_in_R2 & f/.j = N-max L~f & N-max L~f <> NE-corner L~f holds mid(f,i,
j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof
set p = NE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = N-max L~f and
A5: N-max L~f <> NE-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.len mid(f,i,j) = N-max L~f by A1,A2,A4,Th9;
then
A8: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:37;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} & N-max L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:43;
then
LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.
len mid(f,i,j)} by A7,A6,A9,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th61;
end;
theorem
for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 &
f/.j = E-max L~f & E-max L~f <> NE-corner L~f holds mid(f,i,j)^<*NE-corner L~f
*> is S-Sequence_in_R2
proof
set p = NE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = E-max L~f and
A5: E-max L~f <> NE-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th9;
then
A8: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:45;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} & E-max L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:51;
then
LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.
len mid(f,i,j)} by A7,A6,A9,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th61;
end;
theorem Th64:
for i,j st i in dom f & j in dom f & mid(f,i,j) is
S-Sequence_in_R2 & f/.j = S-max L~f & S-max L~f <> SE-corner L~f holds mid(f,i,
j)^<*SE-corner L~f*> is S-Sequence_in_R2
proof
set p = SE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = S-max L~f and
A5: S-max L~f <> SE-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.len mid(f,i,j) = S-max L~f by A1,A2,A4,Th9;
then
A8: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:53;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} & S-max L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:59;
then
LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.
len mid(f,i,j)} by A7,A6,A9,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th61;
end;
theorem Th65:
for i,j st i in dom f & j in dom f & mid(f,i,j) is
S-Sequence_in_R2 & f/.j = E-max L~f & E-max L~f <> NE-corner L~f holds mid(f,i,
j)^<*NE-corner L~f*> is S-Sequence_in_R2
proof
set p = NE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.j = E-max L~f and
A5: E-max L~f <> NE-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th9;
then
A8: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:45;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} & E-max L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:51;
then
LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.
len mid(f,i,j)} by A7,A6,A9,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th61;
end;
theorem Th66:
for i,j st i in dom f & j in dom f & mid(f,i,j) is
S-Sequence_in_R2 & f/.i = N-min L~f & N-min L~f <> NW-corner L~f holds <*
NW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2
proof
set p = NW-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.1 = N-min L~f by A1,A2,A4,Th8;
then
A8: p`2 = ((mid(f,i,j))/.1)`2 by PSCOMP_1:37;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(NW-corner L~f, N-min L~f)/\L~f = {N-min L~f} & N-min L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:43;
then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1} by A7,A6,A9
,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th60;
end;
theorem Th67:
for i,j st i in dom f & j in dom f & mid(f,i,j) is
S-Sequence_in_R2 & f/.i = W-min L~f & W-min L~f <> SW-corner L~f holds <*
SW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2
proof
set p = SW-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = W-min L~f and
A5: W-min L~f <> SW-corner L~f;
A6: 1<=i & i<=len f by A1,FINSEQ_3:25;
A7: (mid(f,i,j))/.1 = W-min L~f by A1,A2,A4,Th8;
then
A8: p`1 = ((mid(f,i,j))/.1)`1 by PSCOMP_1:29;
A9: 1<=j & j<=len f by A2,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
LSeg(SW-corner L~f, W-min L~f)/\L~f = {W-min L~f} & W-min L~f in L~mid(f
,i,j ) by A7,JORDAN3:1,PSCOMP_1:35;
then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1} by A7,A6,A9
,JORDAN4:35,ZFMISC_1:124;
hence thesis by A3,A5,A7,A8,Th60;
end;
Lm1: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.
i = N-min L~f & N-min L~f <> NW-corner L~f & f/.j = N-max L~f & N-max L~f <>
NE-corner L~f holds <*NW-corner L~f*>^mid(f,i,j)^<*NE-corner L~f*> is
S-Sequence_in_R2
proof
set p = NW-corner L~f, q = NE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f and
A6: f/.j = N-max L~f and
A7: N-max L~f <> NE-corner L~f;
set g = <*NW-corner L~f*>^mid(f,i,j);
A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th66;
len g = len<*NW-corner L~f*> + len mid(f,i,j) & len mid(f,i,j) in dom
mid(f, i,j) by A3,FINSEQ_1:22,FINSEQ_5:6;
then
A9: g/.len g = (mid(f,i,j))/.len mid(f,i,j) by FINSEQ_4:69;
then
A10: g/.len g = N-max L~f by A1,A2,A6,Th9;
then
A11: q`2 = (g/.len g)`2 by PSCOMP_1:37;
(mid(f,i,j))/.1 = f/.i by A1,A2,Th8;
then
A12: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20;
A13: 1<=j & j<=len f by A2,FINSEQ_3:25;
A14: 1<=i & i<=len f by A1,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
A15: LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} & N-max L~f in L~mid(
f,i,j ) by A9,A10,JORDAN3:1,PSCOMP_1:43;
LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A10,Th59;
then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {};
then LSeg(q, g/.len g) /\ L~g = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by
A12,XBOOLE_1:23
.= {g/.len g} by A10,A15,A14,A13,JORDAN4:35,ZFMISC_1:124;
hence thesis by A7,A8,A10,A11,Th61;
end;
registration
let f be non constant standard special_circular_sequence;
cluster L~f -> being_simple_closed_curve;
coherence by JORDAN4:51;
end;
Lm2: LSeg(S-max L~f,SE-corner L~f) misses LSeg(NW-corner L~f,N-min L~f)
proof
A1: (NW-corner L~f)`2 = N-bound L~f & (N-min L~f)`2 = N-bound L~f by EUCLID:52;
assume LSeg(S-max L~f,SE-corner L~f) meets LSeg(NW-corner L~f,N-min L~f);
then
LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f) <> {};
then consider x being object such that
A2: x in LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f)
by XBOOLE_0:def 1;
reconsider p = x as Point of TOP-REAL 2 by A2;
p in LSeg(NW-corner L~f,N-min L~f) by A2,XBOOLE_0:def 4;
then N-bound L~f <= p`2 & p`2 <= N-bound L~f by A1,TOPREAL1:4;
then
A3: p`2 = N-bound L~f by XXREAL_0:1;
A4: (SE-corner L~f)`2 = S-bound L~f & (S-max L~f)`2 = S-bound L~f by EUCLID:52;
x in LSeg(S-max L~f,SE-corner L~f) by A2,XBOOLE_0:def 4;
then p`2 <= S-bound L~f by A4,TOPREAL1:4;
hence contradiction by A3,TOPREAL5:16;
end;
Lm3: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.
i = N-min L~f & N-min L~f <> NW-corner L~f & f/.j = S-max L~f & S-max L~f <>
SE-corner L~f holds <*NW-corner L~f*>^mid(f,i,j)^<*SE-corner L~f*> is
S-Sequence_in_R2
proof
set p = NW-corner L~f, q = SE-corner L~f;
let i,j such that
A1: i in dom f and
A2: j in dom f and
A3: mid(f,i,j) is S-Sequence_in_R2 and
A4: f/.i = N-min L~f and
A5: N-min L~f <> NW-corner L~f and
A6: f/.j = S-max L~f and
A7: S-max L~f <> SE-corner L~f;
set g = <*NW-corner L~f*>^mid(f,i,j);
A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th66;
len g = len<*NW-corner L~f*> + len mid(f,i,j) & len mid(f,i,j) in dom
mid(f, i,j) by A3,FINSEQ_1:22,FINSEQ_5:6;
then
A9: g/.len g = (mid(f,i,j))/.len mid(f,i,j) by FINSEQ_4:69;
then
A10: g/.len g = S-max L~f by A1,A2,A6,Th9;
then
A11: q`2 = (g/.len g)`2 by PSCOMP_1:53;
(mid(f,i,j))/.1 = f/.i by A1,A2,Th8;
then
A12: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20;
A13: 1<=j & j<=len f by A2,FINSEQ_3:25;
A14: 1<=i & i<=len f by A1,FINSEQ_3:25;
len mid(f,i,j) >= 2 by A3,TOPREAL1:def 8;
then
A15: LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} & S-max L~f in L~mid(
f,i,j ) by A9,A10,JORDAN3:1,PSCOMP_1:59;
LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A10,Lm2;
then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {};
then LSeg(q, g/.len g) /\ L~g = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by
A12,XBOOLE_1:23
.= {g/.len g} by A10,A15,A14,A13,JORDAN4:35,ZFMISC_1:124;
hence thesis by A7,A8,A10,A11,Th61;
end;
begin :: The order
theorem Th68:
f/.1 = N-min L~f implies (N-min L~f)..f < (N-max L~f)..f
proof
assume f/.1 = N-min L~f;
then
A1: (N-min L~f)..f = 1 by FINSEQ_6:43;
A2: N-max L~f in rng f by Th40;
then (N-max L~f)..f in dom f by FINSEQ_4:20;
then
A3: (N-max L~f)..f >= 1 by FINSEQ_3:25;
N-min L~f in rng f by Th39;
then (N-min L~f)..f <> (N-max L~f)..f by A2,Th52,FINSEQ_5:9;
hence thesis by A3,A1,XXREAL_0:1;
end;
theorem
f/.1 = N-min L~f implies (N-max L~f)..f > 1
proof
assume
A1: f/.1 = N-min L~f;
then (N-min L~f)..f = 1 by FINSEQ_6:43;
hence thesis by A1,Th68;
end;
Lm4: f/.1 = N-min L~f implies (N-min L~f)..f < (E-max L~f)..f
proof
A1: N-min L~f in rng f by Th39;
assume f/.1 = N-min L~f;
then
A2: (N-min L~f)..f = 1 by FINSEQ_6:43;
(N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:38;
then (N-max L~f)`1 <= E-bound L~f by EUCLID:52;
then (N-min L~f)`1 < E-bound L~f by Th51,XXREAL_0:2;
then
A3: (N-min L~f)`1 < (E-max L~f)`1 by EUCLID:52;
A4: E-max L~f in rng f by Th46;
then (E-max L~f)..f >= 1 by FINSEQ_4:21;
hence thesis by A4,A1,A3,A2,FINSEQ_5:9,XXREAL_0:1;
end;
reserve z for clockwise_oriented non constant standard
special_circular_sequence;
Lm5: z/.1 = N-min L~z implies (N-max L~z)..z < (S-max L~z)..z
proof
set i1 = (N-max L~z)..z, i2 = (S-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: N-min L~z <> N-max L~z by Th52;
A4: S-max L~z in rng z by Th42;
then
A5: i2 in dom z by FINSEQ_4:20;
then
A6: i2 <= len z by FINSEQ_3:25;
A7: z/.i2 = z.i2 by A5,PARTFUN1:def 6
.= S-max L~z by A4,FINSEQ_4:19;
then
A8: (z/.i2)`2 = S-bound L~z by EUCLID:52;
A9: 1 <= i2 by A5,FINSEQ_3:25;
A10: i2 <> 0 by A5,FINSEQ_3:25;
(z/.1)`2 = N-bound L~z by A1,EUCLID:52;
then
A11: i2 <> 1 by A8,TOPREAL5:16;
z/.2 in N-most L~z by A1,Th30;
then
A12: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:39
.= N-bound L~z by EUCLID:52;
then i2 <> 2 by A8,TOPREAL5:16;
then i2 <> 0 & ... & i2 <> 2 by A10,A11;
then
A13: i2 > 2;
then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A6,Th37;
A14: 2 <= len z by NAT_D:60;
then
A15: 2 in dom z by FINSEQ_3:25;
then
A16: (h/.len h)`2 = N-bound L~z by A5,A12,Th9;
h/.1 = S-max L~z by A5,A7,A15,Th8;
then
A17: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z by A5,A15,Th21,Th22;
then
A18: h is_a_v.c._for z by A17,A16;
A19: N-max L~z in rng z by Th40;
then
A20: i1 in dom z by FINSEQ_4:20;
then
A21: z/.i1 = z.i1 by PARTFUN1:def 6
.= N-max L~z by A19,FINSEQ_4:19;
A22: i1 <= len z by A20,FINSEQ_3:25;
z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
then
A23: i1 < len z by A22,A21,A3,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A24: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
(N-max L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by EUCLID:52;
then z/.i1 <> z/.i2 by A7,A21,TOPREAL5:16;
then
A25: i1 > i2 by A2,XXREAL_0:1;
then i1 > 1 by A9,XXREAL_0:2;
then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A23,Th37;
A26: 1 in dom M by FINSEQ_5:6;
A27: len z in dom z by FINSEQ_5:6;
then
A28: M/.len M = z/.i1 by A20,Th9
.= N-max L~z by A19,FINSEQ_5:38;
A29: L~M misses L~h by A22,A25,A13,Th49;
A30: 2 <= len h by TOPREAL1:def 8;
1 <= i1 by A20,FINSEQ_3:25;
then
A31: len M = len z -' i1 + 1 by A22,FINSEQ_6:187;
then
A32: M/.len M in L~M by A24,JORDAN3:1;
A33: z/.1 = z/.len z by FINSEQ_6:def 1;
then
A34: M/.1 = z/.1 by A20,A27,Th8;
per cases;
suppose that
A35: NW-corner L~z = N-min L~z and
A36: NE-corner L~z = N-max L~z;
A37: (M/.len M)`1 = E-bound L~z by A28,A36,EUCLID:52;
M/.1 = z/.len z by A20,A27,Th8;
then
A38: (M/.1)`1 = W-bound L~z by A1,A33,A35,EUCLID:52;
M is_in_the_area_of z by A20,A27,Th21,Th22;
then M is_a_h.c._for z by A38,A37;
hence contradiction by A18,A29,A31,A24,A30,Th29;
end;
suppose that
A39: NW-corner L~z = N-min L~z and
A40: NE-corner L~z <> N-max L~z;
reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2 by A20,A21,A27,A40
,Th62;
A41: len g >= 2 & L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
len g = len M + len<*NE-corner L~z*> by FINSEQ_1:22
.= len M + 1 by FINSEQ_1:39;
then g/.len g = NE-corner L~z by FINSEQ_4:67;
then
A42: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*NE-corner L~z*> is_in_the_area_of z by A20,A27
,Th21,Th22,Th25;
then
A43: g is_in_the_area_of z by Th24;
LSeg(M/.len M,NE-corner L~z) /\ L~h c= LSeg(M/.len M,NE-corner L~z)
/\ L~z by A9,A6,A14,JORDAN4:35,XBOOLE_1:26;
then
A44: LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A28,PSCOMP_1:43;
g/.1 = M/.1 by A26,FINSEQ_4:68
.= z/.1 by A20,A27,A33,Th8;
then (g/.1)`1 = W-bound L~z by A1,A39,EUCLID:52;
then g is_a_h.c._for z by A43,A42;
hence contradiction by A18,A29,A32,A30,A41,A44,Th29,ZFMISC_1:125;
end;
suppose that
A45: NW-corner L~z <> N-min L~z and
A46: NE-corner L~z = N-max L~z;
reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A20,A27,A33
,A45,Th66;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i1 by A20,A27,Th9
.= N-max L~z by A19,FINSEQ_5:38;
then
A47: (g/.len g)`1 = E-bound L~z by A46,EUCLID:52;
A48: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A49: (g/.1)`1 = W-bound L~z by EUCLID:52;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A9,A6
,A14,JORDAN4:35,XBOOLE_1:26;
then
A50: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:43;
A51: M/.1 in L~M by A31,A24,JORDAN3:1;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A20,A27
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A49,A47;
hence contradiction by A18,A29,A30,A48,A50,A51,Th29,ZFMISC_1:125;
end;
suppose that
A52: NW-corner L~z <> N-min L~z & NE-corner L~z <> N-max L~z;
set K = <*NW-corner L~z*>^M;
reconsider g = K^<*NE-corner L~z*> as S-Sequence_in_R2 by A1,A20,A21,A27
,A33,A52,Lm1;
1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
then g/.1 = (<*NW-corner L~z*>^M)/.1 by FINSEQ_4:68
.= NW-corner L~z by FINSEQ_5:15;
then
A53: (g/.1)`1 = W-bound L~z by EUCLID:52;
len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*> by FINSEQ_1:22
.= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:39;
then g/.len g = NE-corner L~z by FINSEQ_4:67;
then
A54: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A20,A27
,Th21,Th22,Th26;
then
A55: <*NW-corner L~z*>^M is_in_the_area_of z by Th24;
<*NE-corner L~z*> is_in_the_area_of z by Th25;
then g is_in_the_area_of z by A55,Th24;
then
A56: g is_a_h.c._for z by A53,A54;
len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22;
then len K >= len M by NAT_1:11;
then len K >= 2 by A31,A24,XXREAL_0:2;
then
A57: K/.len K in L~K by JORDAN3:1;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A9,A6
,A14,JORDAN4:35,XBOOLE_1:26;
then
A58: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:43;
L~K = L~M \/ LSeg(NW-corner L~z,M/.1) & M/.1 in L~M by A31,A24,JORDAN3:1
,SPPOL_2:20;
then
A59: L~K misses L~h by A29,A58,ZFMISC_1:125;
len M in dom M & len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then
A60: K/.len K = M/.len M by FINSEQ_4:69
.= z/.i1 by A20,A27,Th9
.= N-max L~z by A19,FINSEQ_5:38;
LSeg(K/.len K,NE-corner L~z) /\ L~h c= LSeg(K/.len K,NE-corner L~z)
/\ L~z by A9,A6,A14,JORDAN4:35,XBOOLE_1:26;
then
A61: LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K} by A60,PSCOMP_1:43;
len g >= 2 & L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
hence contradiction by A18,A30,A56,A59,A57,A61,Th29,ZFMISC_1:125;
end;
end;
Lm6: z/.1 = N-min L~z implies (N-max L~z)..z < (S-min L~z)..z
proof
set i1 = (N-max L~z)..z, i2 = (S-min L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: N-min L~z <> N-max L~z by Th52;
z/.2 in N-most L~z by A1,Th30;
then
A4: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:39
.= N-bound L~z by EUCLID:52;
A5: S-bound L~z < N-bound L~z by TOPREAL5:16;
A6: S-min L~z in rng z by Th41;
then
A7: i2 in dom z by FINSEQ_4:20;
then
A8: i2 <= len z by FINSEQ_3:25;
A9: z/.i2 = z.i2 by A7,PARTFUN1:def 6
.= S-min L~z by A6,FINSEQ_4:19;
then
A10: (z/.i2)`2 = S-bound L~z by EUCLID:52;
A11: 1 <= i2 by A7,FINSEQ_3:25;
A12: i2 <> 0 by A7,FINSEQ_3:25;
(z/.1)`2 = N-bound L~z by A1,EUCLID:52;
then i2 <> 0 & ... & i2 <> 2 by A4,A12,A10,A5;
then
A13: i2 > 2;
then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th37;
A14: 2 <= len z by NAT_D:60;
then
A15: 2 in dom z by FINSEQ_3:25;
then h/.1 = S-min L~z by A7,A9,Th8;
then
A16: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z & h/.len h = z/.2 by A7,A15,Th9,Th21,Th22;
then
A17: len h >= 2 & h is_a_v.c._for z by A4,A16,TOPREAL1:def 8;
A18: N-max L~z in rng z by Th40;
then
A19: i1 in dom z by FINSEQ_4:20;
then
A20: z/.i1 = z.i1 by PARTFUN1:def 6
.= N-max L~z by A18,FINSEQ_4:19;
A21: i1 <= len z by A19,FINSEQ_3:25;
z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
then
A22: i1 < len z by A21,A20,A3,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A23: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
(N-max L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by EUCLID:52;
then z/.i1 <> z/.i2 by A9,A20,TOPREAL5:16;
then
A24: i1 > i2 by A2,XXREAL_0:1;
then i1 > 1 by A11,XXREAL_0:2;
then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A22,Th37;
A25: 1 in dom M by FINSEQ_5:6;
A26: len z in dom z by FINSEQ_5:6;
then
A27: M/.len M = z/.i1 by A19,Th9
.= N-max L~z by A18,FINSEQ_5:38;
A28: L~M misses L~h by A21,A24,A13,Th49;
1 <= i1 by A19,FINSEQ_3:25;
then
A29: len M = len z -' i1 + 1 by A21,FINSEQ_6:187;
then
A30: M/.len M in L~M by A23,JORDAN3:1;
A31: z/.1 = z/.len z by FINSEQ_6:def 1;
then
A32: M/.1 = z/.1 by A19,A26,Th8;
per cases;
suppose that
A33: NW-corner L~z = N-min L~z and
A34: NE-corner L~z = N-max L~z;
A35: (M/.len M)`1 = E-bound L~z by A27,A34,EUCLID:52;
M/.1 = z/.len z by A19,A26,Th8;
then
A36: (M/.1)`1 = W-bound L~z by A1,A31,A33,EUCLID:52;
M is_in_the_area_of z by A19,A26,Th21,Th22;
then M is_a_h.c._for z by A36,A35;
hence contradiction by A17,A28,A29,A23,Th29;
end;
suppose that
A37: NW-corner L~z = N-min L~z and
A38: NE-corner L~z <> N-max L~z;
reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2 by A19,A20,A26,A38
,Th62;
A39: len g >= 2 & L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
len g = len M + len<*NE-corner L~z*> by FINSEQ_1:22
.= len M + 1 by FINSEQ_1:39;
then g/.len g = NE-corner L~z by FINSEQ_4:67;
then
A40: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*NE-corner L~z*> is_in_the_area_of z by A19,A26
,Th21,Th22,Th25;
then
A41: g is_in_the_area_of z by Th24;
LSeg(M/.len M,NE-corner L~z) /\ L~h c= LSeg(M/.len M,NE-corner L~z)
/\ L~z by A11,A8,A14,JORDAN4:35,XBOOLE_1:26;
then
A42: LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A27,PSCOMP_1:43;
g/.1 = M/.1 by A25,FINSEQ_4:68
.= z/.1 by A19,A26,A31,Th8;
then (g/.1)`1 = W-bound L~z by A1,A37,EUCLID:52;
then g is_a_h.c._for z by A41,A40;
hence contradiction by A17,A28,A30,A39,A42,Th29,ZFMISC_1:125;
end;
suppose that
A43: NW-corner L~z <> N-min L~z and
A44: NE-corner L~z = N-max L~z;
reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A19,A26,A31
,A43,Th66;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i1 by A19,A26,Th9
.= N-max L~z by A18,FINSEQ_5:38;
then
A45: (g/.len g)`1 = E-bound L~z by A44,EUCLID:52;
A46: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A47: (g/.1)`1 = W-bound L~z by EUCLID:52;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A11
,A8,A14,JORDAN4:35,XBOOLE_1:26;
then
A48: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A32,PSCOMP_1:43;
A49: M/.1 in L~M by A29,A23,JORDAN3:1;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A19,A26
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A47,A45;
hence contradiction by A17,A28,A46,A48,A49,Th29,ZFMISC_1:125;
end;
suppose that
A50: NW-corner L~z <> N-min L~z & NE-corner L~z <> N-max L~z;
set K = <*NW-corner L~z*>^M;
reconsider g = K^<*NE-corner L~z*> as S-Sequence_in_R2 by A1,A19,A20,A26
,A31,A50,Lm1;
1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
then g/.1 = (<*NW-corner L~z*>^M)/.1 by FINSEQ_4:68
.= NW-corner L~z by FINSEQ_5:15;
then
A51: (g/.1)`1 = W-bound L~z by EUCLID:52;
len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*> by FINSEQ_1:22
.= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:39;
then g/.len g = NE-corner L~z by FINSEQ_4:67;
then
A52: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A19,A26
,Th21,Th22,Th26;
then
A53: <*NW-corner L~z*>^M is_in_the_area_of z by Th24;
<*NE-corner L~z*> is_in_the_area_of z by Th25;
then g is_in_the_area_of z by A53,Th24;
then
A54: g is_a_h.c._for z by A51,A52;
len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22;
then len K >= len M by NAT_1:11;
then len K >= 2 by A29,A23,XXREAL_0:2;
then
A55: K/.len K in L~K by JORDAN3:1;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A11
,A8,A14,JORDAN4:35,XBOOLE_1:26;
then
A56: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A32,PSCOMP_1:43;
L~K = L~M \/ LSeg(NW-corner L~z,M/.1) & M/.1 in L~M by A29,A23,JORDAN3:1
,SPPOL_2:20;
then
A57: L~K misses L~h by A28,A56,ZFMISC_1:125;
len M in dom M & len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then
A58: K/.len K = M/.len M by FINSEQ_4:69
.= z/.i1 by A19,A26,Th9
.= N-max L~z by A18,FINSEQ_5:38;
LSeg(K/.len K,NE-corner L~z) /\ L~h c= LSeg(K/.len K,NE-corner L~z)
/\ L~z by A11,A8,A14,JORDAN4:35,XBOOLE_1:26;
then
A59: LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K} by A58,PSCOMP_1:43;
len g >= 2 & L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
hence contradiction by A17,A54,A57,A55,A59,Th29,ZFMISC_1:125;
end;
end;
theorem
z/.1 = N-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (
E-max L~z)..z
proof
set i1 = (N-max L~z)..z, i2 = (E-max L~z)..z, j = (S-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: N-max L~z <> E-max L~z & i1 >= i2;
(N-min L~z)..z = 1 by A1,FINSEQ_6:43;
then
A3: 1 < i2 by A1,Lm4;
(N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by EUCLID:52;
then
A4: N-min L~z <> S-max L~z by TOPREAL5:16;
A5: S-max L~z in rng z by Th42;
then
A6: j in dom z by FINSEQ_4:20;
then
A7: z/.j = z.j by PARTFUN1:def 6
.= S-max L~z by A5,FINSEQ_4:19;
A8: j <= len z by A6,FINSEQ_3:25;
z/.len z = z/.1 by FINSEQ_6:def 1;
then
A9: j < len z by A1,A8,A7,A4,XXREAL_0:1;
A10: N-max L~z in rng z by Th40;
then
A11: i1 in dom z by FINSEQ_4:20;
then
A12: 1 <= i1 by FINSEQ_3:25;
A13: z/.i1 = z.i1 by A11,PARTFUN1:def 6
.= N-max L~z by A10,FINSEQ_4:19;
A14: j > i1 by A1,Lm5;
then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A12,A9,Th37;
h/.1 = S-max L~z by A11,A6,A7,Th8;
then
A15: (h/.1)`2 = S-bound L~z by EUCLID:52;
h/.len h = z/.i1 by A11,A6,Th9;
then
A16: (h/.len h)`2 = N-bound L~z by A13,EUCLID:52;
h is_in_the_area_of z by A11,A6,Th21,Th22;
then
A17: h is_a_v.c._for z by A15,A16;
A18: 1 <= j by A6,FINSEQ_3:25;
A19: i1 <= len z by A11,FINSEQ_3:25;
A20: E-max L~z in rng z by Th46;
then
A21: i2 in dom z by FINSEQ_4:20;
then
A22: 1 <= i2 & i2 <= len z by FINSEQ_3:25;
z/.i2 = z.i2 by A21,PARTFUN1:def 6
.= E-max L~z by A20,FINSEQ_4:19;
then
A23: i1 > i2 by A2,A13,XXREAL_0:1;
then i2 < len z by A19,XXREAL_0:2;
then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A3,Th38;
A24: len M >= 2 by TOPREAL1:def 8;
A25: 1 in dom z by FINSEQ_5:6;
then
A26: M/.len M = z/.i2 by A21,Th9
.= E-max L~z by A20,FINSEQ_5:38;
A27: len h >= 2 & L~M misses L~h by A14,A9,A3,A23,Th48,TOPREAL1:def 8;
per cases;
suppose
A28: NW-corner L~z = N-min L~z;
M/.1 = z/.1 by A25,A21,Th8;
then
A29: (M/.1)`1 = W-bound L~z by A1,A28,EUCLID:52;
M is_in_the_area_of z & (M/.len M)`1 = E-bound L~z by A25,A21,A26,Th21,Th22
,EUCLID:52;
then M is_a_h.c._for z by A29;
hence contradiction by A17,A24,A27,Th29;
end;
suppose
NW-corner L~z <> N-min L~z;
then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A25,A21
,Th66;
A30: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A31: (g/.1)`1 = W-bound L~z by EUCLID:52;
len M = i2 -' 1 + 1 by A22,FINSEQ_6:186
.= i2 by A3,XREAL_1:235;
then len M >= 1+1 by A3,NAT_1:13;
then
A32: M/.1 in L~M by JORDAN3:1;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i2 by A25,A21,Th9
.= E-max L~z by A20,FINSEQ_5:38;
then
A33: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M/.1 = z/.1 & LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner
L~z) /\ L~z by A25,A12,A19,A18,A8,A21,Th8,JORDAN4:35,XBOOLE_1:26;
then
A34: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,PSCOMP_1:43;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A25,A21
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A31,A33;
hence contradiction by A17,A27,A30,A34,A32,Th29,ZFMISC_1:125;
end;
end;
Lm7: z/.1 = N-min L~z implies (E-max L~z)..z < (S-max L~z)..z
proof
set i1 = (E-max L~z)..z, i2 = (S-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: (N-min L~z)`1 < (N-max L~z)`1 by Th51;
z/.2 in N-most L~z by A1,Th30;
then
A4: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:39
.= N-bound L~z by EUCLID:52;
E-min L~z in L~z by SPRECT_1:14;
then
A5: S-bound L~z <= (E-min L~z)`2 by PSCOMP_1:24;
A6: S-bound L~z < N-bound L~z by TOPREAL5:16;
A7: S-max L~z in rng z by Th42;
then
A8: i2 in dom z by FINSEQ_4:20;
then
A9: i2 <= len z by FINSEQ_3:25;
A10: i2 <> 0 by A8,FINSEQ_3:25;
A11: z/.i2 = z.i2 by A8,PARTFUN1:def 6
.= S-max L~z by A7,FINSEQ_4:19;
then
A12: (z/.i2)`2 = S-bound L~z by EUCLID:52;
A13: 1 <= i2 by A8,FINSEQ_3:25;
(z/.1)`2 = N-bound L~z by A1,EUCLID:52;
then i2 <> 0 & ... & i2 <> 2 by A4,A10,A12,A6;
then
A14: i2 > 2;
then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A9,Th37;
A15: 2 <= len z by NAT_D:60;
then
A16: 2 in dom z by FINSEQ_3:25;
then h/.1 = S-max L~z by A8,A11,Th8;
then
A17: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z & h/.len h = z/.2 by A8,A16,Th9,Th21,Th22;
then
A18: len h >= 2 & h is_a_v.c._for z by A4,A17,TOPREAL1:def 8;
N-max L~z in L~z by SPRECT_1:11;
then
A19: (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
A20: E-max L~z in rng z by Th46;
then
A21: i1 in dom z by FINSEQ_4:20;
then
A22: z/.i1 = z.i1 by PARTFUN1:def 6
.= E-max L~z by A20,FINSEQ_4:19;
A23: i1 <= len z by A21,FINSEQ_3:25;
z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
then i1 <> len z by A22,A3,A19,EUCLID:52;
then
A24: i1 < len z by A23,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A25: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
(E-min L~z)`2 < (E-max L~z)`2 by Th53;
then E-max L~z <> S-max L~z by A5,EUCLID:52;
then
A26: i1 > i2 by A2,A11,A22,XXREAL_0:1;
then i1 > 1 by A13,XXREAL_0:2;
then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A24,Th37;
A27: len M >= 2 by TOPREAL1:def 8;
1 <= i1 by A21,FINSEQ_3:25;
then
A28: len M = len z -' i1 + 1 by A23,FINSEQ_6:187;
A29: len z in dom z by FINSEQ_5:6;
then
A30: M/.len M = z/.i1 by A21,Th9
.= E-max L~z by A20,FINSEQ_5:38;
A31: L~M misses L~h by A23,A26,A14,Th49;
A32: z/.1 = z/.len z by FINSEQ_6:def 1;
then
A33: M/.1 = z/.1 by A21,A29,Th8;
per cases;
suppose that
A34: NW-corner L~z = N-min L~z;
M/.1 = z/.len z by A21,A29,Th8;
then
A35: (M/.1)`1 = W-bound L~z by A1,A32,A34,EUCLID:52;
M is_in_the_area_of z & (M/.len M)`1 = E-bound L~z by A21,A29,A30,Th21,Th22
,EUCLID:52;
then M is_a_h.c._for z by A35;
hence contradiction by A18,A27,A31,Th29;
end;
suppose
NW-corner L~z <> N-min L~z;
then reconsider
g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A21,A29,A32,Th66;
A36: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A37: (g/.1)`1 = W-bound L~z by EUCLID:52;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A13
,A9,A15,JORDAN4:35,XBOOLE_1:26;
then
A38: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A33,PSCOMP_1:43;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i1 by A21,A29,Th9
.= E-max L~z by A20,FINSEQ_5:38;
then
A39: (g/.len g)`1 = E-bound L~z by EUCLID:52;
A40: M/.1 in L~M by A28,A25,JORDAN3:1;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A21,A29
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A37,A39;
hence contradiction by A18,A31,A36,A38,A40,Th29,ZFMISC_1:125;
end;
end;
Lm8: LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) = {}
proof
A1: (NE-corner L~f)`1 = E-bound L~f & (E-max L~f)`1 = E-bound L~f by EUCLID:52;
assume LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) <> {};
then consider x being object such that
A2: x in LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f)
by XBOOLE_0:def 1;
reconsider p = x as Point of TOP-REAL 2 by A2;
p in LSeg(NE-corner L~f,E-max L~f) by A2,XBOOLE_0:def 4;
then E-bound L~f <= p`1 & p`1 <= E-bound L~f by A1,TOPREAL1:3;
then
A3: p`1 = E-bound L~f by XXREAL_0:1;
A4: (NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:38;
(N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:38;
then
A5: (N-min L~f)`1 < (NE-corner L~f)`1 by Th51,XXREAL_0:2;
x in LSeg(N-min L~f,NW-corner L~f) by A2,XBOOLE_0:def 4;
then p`1 <= (N-min L~f)`1 by A4,TOPREAL1:3;
hence contradiction by A3,A5,EUCLID:52;
end;
theorem
z/.1 = N-min L~z implies (E-max L~z)..z < (E-min L~z)..z
proof
set i1 = (E-max L~z)..z, i2 = (E-min L~z)..z, j = (S-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: i1 < j by A1,Lm7;
A4: E-min L~z in rng z by Th45;
then
A5: i2 in dom z by FINSEQ_4:20;
then
A6: 1 <= i2 by FINSEQ_3:25;
A7: z/.i2 = z.i2 by A5,PARTFUN1:def 6
.= E-min L~z by A4,FINSEQ_4:19;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
then
A8: i2 > 1 by A1,A6,A7,XXREAL_0:1;
A9: i2 <= len z by A5,FINSEQ_3:25;
then
A10: 1 <= len z by A6,XXREAL_0:2;
A11: (S-max L~z)`2 = S-bound L~z by EUCLID:52;
A12: S-bound L~z < N-bound L~z & (N-min L~z)`2 = N-bound L~z by EUCLID:52
,TOPREAL5:16;
A13: S-max L~z in rng z by Th42;
then
A14: j in dom z by FINSEQ_4:20;
then
A15: j <= len z by FINSEQ_3:25;
A16: 1 <= j by A14,FINSEQ_3:25;
A17: E-max L~z in rng z by Th46;
then
A18: i1 in dom z by FINSEQ_4:20;
then
A19: z/.i1 = z.i1 by PARTFUN1:def 6
.= E-max L~z by A17,FINSEQ_4:19;
A20: 1 <= i1 by A18,FINSEQ_3:25;
A21: i1 <= len z by A18,FINSEQ_3:25;
(E-min L~z)`2 < (E-max L~z)`2 by Th53;
then
A22: i1 > i2 by A2,A7,A19,XXREAL_0:1;
then i2 < len z by A21,XXREAL_0:2;
then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A8,Th38;
A23: 1 in dom z by FINSEQ_5:6;
then
A24: M/.1 = z/.1 by A5,Th8;
i1 > 1 by A6,A22,XXREAL_0:2;
then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A15,A3,Th37;
A25: h/.len h = z/.i1 by A18,A14,Th9;
A26: z/.j = z.j by A14,PARTFUN1:def 6
.= S-max L~z by A13,FINSEQ_4:19;
then h/.1 = S-max L~z by A18,A14,Th8;
then
A27: (h/.1)`2 = S-bound L~z by EUCLID:52;
M/.len M = z/.i2 by A23,A5,Th9
.= E-min L~z by A4,FINSEQ_5:38;
then
A28: (M/.len M)`1 = E-bound L~z by EUCLID:52;
A29: M is_in_the_area_of z by A23,A5,Th21,Th22;
len h >= 1 by A18,A14,Th5;
then len h > 1 by A18,A14,A3,Th6,XXREAL_0:1;
then
A30: len h >= 1+1 by NAT_1:13;
len M = i2 -' 1 + 1 by A6,A9,FINSEQ_6:186
.= i2 by A6,XREAL_1:235;
then
A31: len M >= 1+1 by A8,NAT_1:13;
A32: h is_in_the_area_of z by A18,A14,Th21,Th22;
z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
then j < len z by A15,A26,A12,A11,XXREAL_0:1;
then
A33: L~M misses L~h by A6,A22,A3,Th48;
per cases;
suppose that
A34: NW-corner L~z = N-min L~z and
A35: NE-corner L~z = E-max L~z;
(M/.1)`1 = W-bound L~z by A1,A24,A34,EUCLID:52;
then
A36: M is_a_h.c._for z by A29,A28;
(h/.len h)`2 = N-bound L~z by A19,A25,A35,EUCLID:52;
then h is_a_v.c._for z by A32,A27;
hence contradiction by A33,A31,A30,A36,Th29;
end;
suppose that
A37: NW-corner L~z <> N-min L~z and
A38: NE-corner L~z = E-max L~z;
reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A23,A5,A37
,Th66;
A39: 2 <= len g & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
(h/.len h)`2 = N-bound L~z by A19,A25,A38,EUCLID:52;
then
A40: h is_a_v.c._for z by A32,A27;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A41: (g/.1)`1 = W-bound L~z by EUCLID:52;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i2 by A23,A5,Th9
.= E-min L~z by A4,FINSEQ_5:38;
then
A42: (g/.len g)`1 = E-bound L~z by EUCLID:52;
<*NW-corner L~z*> is_in_the_area_of z by Th26;
then g is_in_the_area_of z by A29,Th24;
then
A43: g is_a_h.c._for z by A41,A42;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A20
,A21,A16,A15,JORDAN4:35,XBOOLE_1:26;
then
A44: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A24,PSCOMP_1:43;
M/.1 in L~M by A31,JORDAN3:1;
hence contradiction by A33,A30,A40,A43,A39,A44,Th29,ZFMISC_1:125;
end;
suppose that
A45: NW-corner L~z = N-min L~z and
A46: NE-corner L~z<> E-max L~z;
reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2 by A18,A19,A14,A46
,Th65;
A47: len M >= 2 & len N >= 2 by TOPREAL1:def 8;
LSeg(h/.len h,NE-corner L~z) /\ L~M c= LSeg(h/.len h,NE-corner L~z)
/\ L~z by A6,A9,A10,JORDAN4:35,XBOOLE_1:26;
then
A48: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A19,A25,PSCOMP_1:51;
L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) & h/.len h in L~h by A30,
JORDAN3:1,SPPOL_2:19;
then
A49: L~M misses L~N by A33,A48,ZFMISC_1:125;
len N = len h + len<*NE-corner L~z*> by FINSEQ_1:22
.= len h + 1 by FINSEQ_1:39;
then N/.len N = NE-corner L~z by FINSEQ_4:67;
then
A50: (N/.len N)`2 = N-bound L~z by EUCLID:52;
M/.1 = z/.1 by A23,A5,Th8;
then (M/.1)`1 = W-bound L~z by A1,A45,EUCLID:52;
then
A51: M is_a_h.c._for z by A29,A28;
1 in dom h by FINSEQ_5:6;
then
A52: (N/.1)`2 = S-bound L~z by A27,FINSEQ_4:68;
<*NE-corner L~z*> is_in_the_area_of z by Th25;
then N is_in_the_area_of z by A32,Th24;
then N is_a_v.c._for z by A52,A50;
hence contradiction by A51,A47,A49,Th29;
end;
suppose that
A53: NW-corner L~z <> N-min L~z and
A54: NE-corner L~z <> E-max L~z;
reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2 by A18,A19,A14,A54
,Th65;
reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A23,A5,A53
,Th66;
A55: len g >= 2 & len N >= 2 by TOPREAL1:def 8;
A56: L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) by SPPOL_2:19;
LSeg(M/.1,NW-corner L~z) /\ LSeg(NE-corner L~z,h/.len h) = {} by A1,A19,A25
,A24,Lm8;
then LSeg(M/.1,NW-corner L~z) /\ L~N = LSeg(M/.1,NW-corner L~z) /\ L~h \/
{} by A56,XBOOLE_1:23
.= LSeg(M/.1,NW-corner L~z) /\ L~h;
then LSeg(M/.1,NW-corner L~z) /\ L~N c= LSeg(M/.1,NW-corner L~z) /\ L~z
by A20,A21,A16,A15,JORDAN4:35,XBOOLE_1:26;
then
A57: LSeg(M/.1,NW-corner L~z) /\ L~N c= {M/.1} by A1,A24,PSCOMP_1:43;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A58: (g/.1)`1 = W-bound L~z by EUCLID:52;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i2 by A23,A5,Th9
.= E-min L~z by A4,FINSEQ_5:38;
then
A59: (g/.len g)`1 = E-bound L~z by EUCLID:52;
len N = len h + len<*NE-corner L~z*> by FINSEQ_1:22
.= len h + 1 by FINSEQ_1:39;
then N/.len N = NE-corner L~z by FINSEQ_4:67;
then
A60: (N/.len N)`2 = N-bound L~z by EUCLID:52;
LSeg(h/.len h,NE-corner L~z) /\ L~M c= LSeg(h/.len h,NE-corner L~z)
/\ L~z by A6,A9,A10,JORDAN4:35,XBOOLE_1:26;
then
A61: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A19,A25,PSCOMP_1:51;
h/.len h in L~h by A30,JORDAN3:1;
then
A62: L~M misses L~N by A33,A56,A61,ZFMISC_1:125;
1 in dom h by FINSEQ_5:6;
then
A63: (N/.1)`2 = S-bound L~z by A27,FINSEQ_4:68;
<*NE-corner L~z*> is_in_the_area_of z by Th25;
then N is_in_the_area_of z by A32,Th24;
then
A64: N is_a_v.c._for z by A63,A60;
<*NW-corner L~z*> is_in_the_area_of z by Th26;
then g is_in_the_area_of z by A29,Th24;
then
A65: g is_a_h.c._for z by A58,A59;
L~g = L~M \/ LSeg(NW-corner L~z,M/.1) & M/.1 in L~M by A31,JORDAN3:1
,SPPOL_2:20;
hence contradiction by A65,A55,A64,A62,A57,Th29,ZFMISC_1:125;
end;
end;
theorem Th72:
z/.1 = N-min L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z
< (S-max L~z)..z
proof
set i1 = (E-min L~z)..z, i2 = (S-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: E-min L~z <> S-max L~z & i1 >= i2;
A3: S-bound L~z < N-bound L~z by TOPREAL5:16;
z/.2 in N-most L~z by A1,Th30;
then
A4: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:39
.= N-bound L~z by EUCLID:52;
A5: S-max L~z in rng z by Th42;
then
A6: i2 in dom z by FINSEQ_4:20;
then
A7: i2 <= len z by FINSEQ_3:25;
A8: z/.i2 = z.i2 by A6,PARTFUN1:def 6
.= S-max L~z by A5,FINSEQ_4:19;
then
A9: (z/.i2)`2 = S-bound L~z by EUCLID:52;
A10: 1 <= i2 by A6,FINSEQ_3:25;
A11: i2 <> 0 by A6,FINSEQ_3:25;
(z/.1)`2 = N-bound L~z by A1,EUCLID:52;
then i2 <> 0 & ... & i2 <> 2 by A4,A11,A9,A3;
then
A12: i2 > 2;
then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A7,Th37;
A13: 2 <= len z by NAT_D:60;
then
A14: 2 in dom z by FINSEQ_3:25;
then h/.1 = S-max L~z by A6,A8,Th8;
then
A15: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z & h/.len h = z/.2 by A6,A14,Th9,Th21,Th22;
then
A16: len h >= 2 & h is_a_v.c._for z by A4,A15,TOPREAL1:def 8;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then
A17: (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
A18: E-min L~z in rng z by Th45;
then
A19: i1 in dom z by FINSEQ_4:20;
then
A20: z/.i1 = z.i1 by PARTFUN1:def 6
.= E-min L~z by A18,FINSEQ_4:19;
A21: i1 <= len z by A19,FINSEQ_3:25;
z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
then
A22: i1 < len z by A21,A20,A17,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A23: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
A24: i1 > i2 by A2,A8,A20,XXREAL_0:1;
then i1 > 1 by A10,XXREAL_0:2;
then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A22,Th37;
A25: len z in dom z by FINSEQ_5:6;
then
A26: M/.len M = z/.i1 by A19,Th9
.= E-min L~z by A18,FINSEQ_5:38;
1 <= i1 by A19,FINSEQ_3:25;
then
A27: len M = len z -' i1 + 1 by A21,FINSEQ_6:187;
A28: L~M misses L~h by A21,A24,A12,Th49;
A29: z/.1 = z/.len z by FINSEQ_6:def 1;
then
A30: M/.1 = z/.1 by A19,A25,Th8;
per cases;
suppose that
A31: NW-corner L~z = N-min L~z;
M/.1 = z/.len z by A19,A25,Th8;
then
A32: (M/.1)`1 = W-bound L~z by A1,A29,A31,EUCLID:52;
M is_in_the_area_of z & (M/.len M)`1 = E-bound L~z by A19,A25,A26,Th21,Th22
,EUCLID:52;
then M is_a_h.c._for z by A32;
hence contradiction by A16,A28,A27,A23,Th29;
end;
suppose
NW-corner L~z <> N-min L~z;
then reconsider
g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A19,A25,A29,Th66;
A33: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A34: (g/.1)`1 = W-bound L~z by EUCLID:52;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A10
,A7,A13,JORDAN4:35,XBOOLE_1:26;
then
A35: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A30,PSCOMP_1:43;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= z/.i1 by A19,A25,Th9
.= E-min L~z by A18,FINSEQ_5:38;
then
A36: (g/.len g)`1 = E-bound L~z by EUCLID:52;
A37: M/.1 in L~M by A27,A23,JORDAN3:1;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A19,A25
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A34,A36;
hence contradiction by A16,A28,A33,A35,A37,Th29,ZFMISC_1:125;
end;
end;
theorem Th73:
z/.1 = N-min L~z implies (S-max L~z)..z < (S-min L~z)..z
proof
set i1 = (S-max L~z)..z, i2 = (S-min L~z)..z, j = (N-max L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: z/.1 = z/.len z by FINSEQ_6:def 1;
A4: S-min L~z in rng z by Th41;
then
A5: i2 in dom z by FINSEQ_4:20;
then
A6: i2 <= len z by FINSEQ_3:25;
A7: 1 <= i2 by A5,FINSEQ_3:25;
A8: S-max L~z in rng z by Th42;
then
A9: i1 in dom z by FINSEQ_4:20;
then
A10: z/.i1 = z.i1 by PARTFUN1:def 6
.= S-max L~z by A8,FINSEQ_4:19;
A11: i1 <= len z by A9,FINSEQ_3:25;
(N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by EUCLID:52;
then N-min L~z <> S-max L~z by TOPREAL5:16;
then
A12: i1 < len z by A1,A11,A10,A3,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A13: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
A14: N-max L~z in rng z by Th40;
then
A15: j in dom z by FINSEQ_4:20;
then
A16: 1 <= j by FINSEQ_3:25;
then i1 > 1 by A1,Lm5,XXREAL_0:2;
then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A12,Th37;
A17: z/.j = z.j by A15,PARTFUN1:def 6
.= N-max L~z by A14,FINSEQ_4:19;
then
A18: (z/.j)`2 = N-bound L~z by EUCLID:52;
N-min L~z <> N-max L~z by Th52;
then
A19: 1 < j by A1,A16,A17,XXREAL_0:1;
A20: len z in dom z by FINSEQ_5:6;
then
A21: M/.1 = z/.len z by A9,Th8;
1 <= i1 by A9,FINSEQ_3:25;
then
A22: len M = len z -' i1 + 1 by A11,FINSEQ_6:187;
then
A23: M/.len M in L~M by A13,JORDAN3:1;
A24: 1 in dom M by FINSEQ_5:6;
A25: j <= len z by A15,FINSEQ_3:25;
A26: i2 > j by A1,Lm6;
then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A6,A19,Th37;
A27: z/.i2 = z.i2 by A5,PARTFUN1:def 6
.= S-min L~z by A4,FINSEQ_4:19;
then h/.1 = S-min L~z by A5,A15,Th8;
then
A28: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z & h/.len h = z/.j by A5,A15,Th9,Th21,Th22;
then
A29: len h >= 2 & h is_a_v.c._for z by A18,A28,TOPREAL1:def 8;
S-min L~z <> S-max L~z by Th56;
then i1 > i2 by A2,A27,A10,XXREAL_0:1;
then
A30: L~h misses L~M by A11,A26,A19,Th49;
A31: M/.len M = S-max L~z by A9,A10,A20,Th9;
per cases;
suppose that
A32: NW-corner L~z = N-min L~z & SE-corner L~z = S-max L~z;
A33: M is_in_the_area_of z by A9,A20,Th21,Th22;
(M/.1)`1 = W-bound L~z & (M/.len M)`1 = E-bound L~z by A1,A3,A31,A21,A32,
EUCLID:52;
then M is_a_h.c._for z by A33;
hence contradiction by A29,A30,A22,A13,Th29;
end;
suppose that
A34: NW-corner L~z = N-min L~z and
A35: SE-corner L~z <> S-max L~z;
reconsider g = M^<*SE-corner L~z*> as S-Sequence_in_R2 by A9,A10,A20,A35
,Th64;
A36: len g >= 2 & L~g = L~M \/ LSeg(M/.len M,SE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
len g = len M + len<*SE-corner L~z*> by FINSEQ_1:22
.= len M + 1 by FINSEQ_1:39;
then g/.len g = SE-corner L~z by FINSEQ_4:67;
then
A37: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*SE-corner L~z*> is_in_the_area_of z by A9,A20
,Th21,Th22,Th27;
then
A38: g is_in_the_area_of z by Th24;
LSeg(M/.len M,SE-corner L~z) /\ L~h c= LSeg(M/.len M,SE-corner L~z)
/\ L~z by A7,A6,A16,A25,JORDAN4:35,XBOOLE_1:26;
then
A39: LSeg(M/.len M,SE-corner L~z) /\ L~h c= {M/.len M} by A31,PSCOMP_1:59;
g/.1 = M/.1 by A24,FINSEQ_4:68
.= z/.1 by A9,A3,A20,Th8;
then (g/.1)`1 = W-bound L~z by A1,A34,EUCLID:52;
then g is_a_h.c._for z by A38,A37;
hence contradiction by A29,A30,A23,A36,A39,Th29,ZFMISC_1:125;
end;
suppose that
A40: NW-corner L~z <> N-min L~z and
A41: SE-corner L~z = S-max L~z;
reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A9,A3,A20,A40
,Th66;
len M in dom M & len g = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69
.= S-max L~z by A9,A10,A20,Th9;
then
A42: (g/.len g)`1 = E-bound L~z by A41,EUCLID:52;
A43: len g >= 2 & L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20
,TOPREAL1:def 8;
g/.1 = NW-corner L~z by FINSEQ_5:15;
then
A44: (g/.1)`1 = W-bound L~z by EUCLID:52;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A7,A6
,A16,A25,JORDAN4:35,XBOOLE_1:26;
then
A45: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A3,A21,PSCOMP_1:43;
A46: M/.1 in L~M by A22,A13,JORDAN3:1;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A9,A20
,Th21,Th22,Th26;
then g is_in_the_area_of z by Th24;
then g is_a_h.c._for z by A44,A42;
hence contradiction by A29,A30,A43,A45,A46,Th29,ZFMISC_1:125;
end;
suppose that
A47: NW-corner L~z <> N-min L~z & SE-corner L~z <> S-max L~z;
set K = <*NW-corner L~z*>^M;
reconsider g = K^<*SE-corner L~z*> as S-Sequence_in_R2 by A1,A9,A10,A3,A20
,A47,Lm3;
1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6;
then g/.1 = (<*NW-corner L~z*>^M)/.1 by FINSEQ_4:68
.= NW-corner L~z by FINSEQ_5:15;
then
A48: (g/.1)`1 = W-bound L~z by EUCLID:52;
len g = len(<*NW-corner L~z*>^M) + len<*SE-corner L~z*> by FINSEQ_1:22
.= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:39;
then g/.len g = SE-corner L~z by FINSEQ_4:67;
then
A49: (g/.len g)`1 = E-bound L~z by EUCLID:52;
M is_in_the_area_of z & <*NW-corner L~z*> is_in_the_area_of z by A9,A20
,Th21,Th22,Th26;
then
A50: <*NW-corner L~z*>^M is_in_the_area_of z by Th24;
<*SE-corner L~z*> is_in_the_area_of z by Th27;
then g is_in_the_area_of z by A50,Th24;
then
A51: g is_a_h.c._for z by A48,A49;
len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22;
then len K >= len M by NAT_1:11;
then len K >= 2 by A22,A13,XXREAL_0:2;
then
A52: K/.len K in L~K by JORDAN3:1;
LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A7,A6
,A16,A25,JORDAN4:35,XBOOLE_1:26;
then
A53: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A3,A21,PSCOMP_1:43;
L~K = L~M \/ LSeg(NW-corner L~z,M/.1) & M/.1 in L~M by A22,A13,JORDAN3:1
,SPPOL_2:20;
then
A54: L~K misses L~h by A30,A53,ZFMISC_1:125;
len M in dom M & len K = len M + len<*NW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then
A55: K/.len K = M/.len M by FINSEQ_4:69
.= z/.i1 by A9,A20,Th9
.= S-max L~z by A8,FINSEQ_5:38;
LSeg(K/.len K,SE-corner L~z) /\ L~h c= LSeg(K/.len K,SE-corner L~z)
/\ L~z by A7,A6,A16,A25,JORDAN4:35,XBOOLE_1:26;
then
A56: LSeg(K/.len K,SE-corner L~z) /\ L~h c= {K/.len K} by A55,PSCOMP_1:59;
len g >= 2 & L~g = L~K \/ LSeg(K/.len K,SE-corner L~z) by SPPOL_2:19
,TOPREAL1:def 8;
hence contradiction by A29,A51,A54,A52,A56,Th29,ZFMISC_1:125;
end;
end;
Lm9: z/.1 = N-min L~z implies (E-min L~z)..z < (S-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then (E-min L~z)..z <= (S-max L~z)..z by Th72;
hence thesis by A1,Th73,XXREAL_0:2;
end;
Lm10: z/.1 = N-min L~z & N-min L~z <> W-max L~z implies (E-min L~z)..z < (
W-max L~z)..z
proof
set i1 = (E-min L~z)..z, i2 = (W-max L~z)..z, j = (S-min L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: N-min L~z <> W-max L~z and
A3: i1 >= i2;
A4: z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then
A5: (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
(N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by EUCLID:52;
then
A6: N-min L~z <> S-min L~z by TOPREAL5:16;
A7: S-min L~z in rng z by Th41;
then
A8: j in dom z by FINSEQ_4:20;
then
A9: j <= len z by FINSEQ_3:25;
A10: E-min L~z in rng z by Th45;
then
A11: i1 in dom z by FINSEQ_4:20;
then
A12: z/.i1 = z.i1 by PARTFUN1:def 6
.= E-min L~z by A10,FINSEQ_4:19;
A13: W-max L~z in rng z by Th44;
then
A14: i2 in dom z by FINSEQ_4:20;
then
A15: z/.i2 = z.i2 by PARTFUN1:def 6
.= W-max L~z by A13,FINSEQ_4:19;
A16: 1 <= i2 by A14,FINSEQ_3:25;
(W-max L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z by EUCLID:52;
then (W-max L~z)`1 < (E-min L~z)`1 by TOPREAL5:17;
then
A17: i1 > i2 by A3,A15,A12,XXREAL_0:1;
then i1 > 1 by A16,XXREAL_0:2;
then
A18: j > 1 by A1,Lm9,XXREAL_0:2;
z/.j = z.j by A8,PARTFUN1:def 6
.= S-min L~z by A7,FINSEQ_4:19;
then j < len z by A4,A9,A6,XXREAL_0:1;
then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A18,Th38;
A19: i1 < j by A1,Lm9;
A20: len z in dom z by FINSEQ_5:6;
then h/.len h = z/.len z by A8,Th9;
then
A21: (h/.len h)`2 = N-bound L~z by A4,EUCLID:52;
i1 <= len z by A11,FINSEQ_3:25;
then i1 < len z by A4,A12,A5,XXREAL_0:1;
then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A16,A17,Th38;
M/.len M = z/.i1 by A11,A14,Th9
.= E-min L~z by A10,FINSEQ_5:38;
then
A22: (M/.len M)`1 = E-bound L~z by EUCLID:52;
M/.1 = W-max L~z by A11,A14,A15,Th8;
then
A23: (M/.1)`1 = W-bound L~z by EUCLID:52;
M is_in_the_area_of z by A11,A14,Th21,Th22;
then
A24: M is_a_h.c._for z by A23,A22;
z/.j = z.j by A8,PARTFUN1:def 6
.= S-min L~z by A7,FINSEQ_4:19;
then h/.1 = S-min L~z by A20,A8,Th8;
then
A25: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z by A20,A8,Th21,Th22;
then
A26: h is_a_v.c._for z by A25,A21;
i2 > 1 by A1,A2,A16,A15,XXREAL_0:1;
then
A27: L~M misses L~h by A3,A9,A19,Th47;
len h >= 2 & len M >= 2 by TOPREAL1:def 8;
hence contradiction by A26,A24,A27,Th29;
end;
Lm11: z/.1 = N-min L~z implies (E-min L~z)..z < (W-min L~z)..z
proof
set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: i1 >= i2;
A3: z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then
A4: (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
(N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by EUCLID:52;
then
A5: N-min L~z <> S-min L~z by TOPREAL5:16;
A6: S-min L~z in rng z by Th41;
then
A7: j in dom z by FINSEQ_4:20;
then
A8: j <= len z by FINSEQ_3:25;
A9: E-min L~z in rng z by Th45;
then
A10: i1 in dom z by FINSEQ_4:20;
then
A11: z/.i1 = z.i1 by PARTFUN1:def 6
.= E-min L~z by A9,FINSEQ_4:19;
A12: W-min L~z in rng z by Th43;
then
A13: i2 in dom z by FINSEQ_4:20;
then
A14: z/.i2 = z.i2 by PARTFUN1:def 6
.= W-min L~z by A12,FINSEQ_4:19;
A15: 1 <= i2 by A13,FINSEQ_3:25;
(W-min L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z by EUCLID:52;
then z/.i1 <> z/.i2 by A14,A11,TOPREAL5:17;
then
A16: i1 > i2 by A2,XXREAL_0:1;
then i1 > 1 by A15,XXREAL_0:2;
then
A17: j > 1 by A1,Lm9,XXREAL_0:2;
z/.j = z.j by A7,PARTFUN1:def 6
.= S-min L~z by A6,FINSEQ_4:19;
then j < len z by A3,A8,A5,XXREAL_0:1;
then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A17,Th38;
A18: i1 < j by A1,Lm9;
A19: len z in dom z by FINSEQ_5:6;
then h/.len h = z/.len z by A7,Th9;
then
A20: (h/.len h)`2 = N-bound L~z by A3,EUCLID:52;
i1 <= len z by A10,FINSEQ_3:25;
then i1 < len z by A3,A11,A4,XXREAL_0:1;
then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A15,A16,Th38;
M/.len M = z/.i1 by A10,A13,Th9
.= E-min L~z by A9,FINSEQ_5:38;
then
A21: (M/.len M)`1 = E-bound L~z by EUCLID:52;
z/.j = z.j by A7,PARTFUN1:def 6
.= S-min L~z by A6,FINSEQ_4:19;
then h/.1 = S-min L~z by A19,A7,Th8;
then
A22: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z by A19,A7,Th21,Th22;
then
A23: h is_a_v.c._for z by A22,A20;
W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by EUCLID:52,SPRECT_1:13;
then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:24;
then N-min L~z <> W-min L~z by Th57;
then i2 > 1 by A1,A15,A14,XXREAL_0:1;
then
A24: L~M misses L~h by A2,A8,A18,Th47;
M/.1 = W-min L~z by A10,A13,A14,Th8;
then
A25: (M/.1)`1 = W-bound L~z by EUCLID:52;
M is_in_the_area_of z by A10,A13,Th21,Th22;
then
A26: M is_a_h.c._for z by A25,A21;
len h >= 2 & len M >= 2 by TOPREAL1:def 8;
hence contradiction by A23,A26,A24,Th29;
end;
theorem
z/.1 = N-min L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (
W-min L~z)..z
proof
set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: S-min L~z <> W-min L~z & j >= i2;
A3: z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then
A4: (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
A5: E-min L~z in rng z by Th45;
then
A6: i1 in dom z by FINSEQ_4:20;
then
A7: 1 <= i1 by FINSEQ_3:25;
then
A8: j > 1 by A1,Lm9,XXREAL_0:2;
z/.i1 = z.i1 by A6,PARTFUN1:def 6
.= E-min L~z by A5,FINSEQ_4:19;
then
A9: i1 > 1 by A1,A7,A4,XXREAL_0:1;
(N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by EUCLID:52;
then
A10: N-min L~z <> S-min L~z by TOPREAL5:16;
A11: S-min L~z in rng z by Th41;
then
A12: j in dom z by FINSEQ_4:20;
then
A13: j <= len z by FINSEQ_3:25;
z/.j = z.j by A12,PARTFUN1:def 6
.= S-min L~z by A11,FINSEQ_4:19;
then j < len z by A3,A13,A10,XXREAL_0:1;
then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A8,Th38;
A14: len z in dom z by FINSEQ_5:6;
then h/.len h = z/.len z by A12,Th9;
then
A15: (h/.len h)`2 = N-bound L~z by A3,EUCLID:52;
A16: z/.j = z.j by A12,PARTFUN1:def 6
.= S-min L~z by A11,FINSEQ_4:19;
then h/.1 = S-min L~z by A12,A14,Th8;
then
A17: (h/.1)`2 = S-bound L~z by EUCLID:52;
h is_in_the_area_of z by A12,A14,Th21,Th22;
then
A18: h is_a_v.c._for z by A17,A15;
A19: i1 < i2 by A1,Lm11;
A20: W-min L~z in rng z by Th43;
then
A21: i2 in dom z by FINSEQ_4:20;
then i2 <= len z by FINSEQ_3:25;
then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A19,A9,Th37;
M/.len M = z/.i1 by A6,A21,Th9
.= E-min L~z by A5,FINSEQ_5:38;
then
A22: (M/.len M)`1 = E-bound L~z by EUCLID:52;
A23: z/.i2 = z.i2 by A21,PARTFUN1:def 6
.= W-min L~z by A20,FINSEQ_4:19;
then M/.1 = W-min L~z by A6,A21,Th8;
then
A24: (M/.1)`1 = W-bound L~z by EUCLID:52;
M is_in_the_area_of z by A6,A21,Th21,Th22;
then
A25: M is_a_h.c._for z by A24,A22;
A26: len h >= 2 & len M >= 2 by TOPREAL1:def 8;
j > i2 by A2,A23,A16,XXREAL_0:1;
then L~M misses L~h by A19,A9,A13,Th50;
hence contradiction by A18,A26,A25,Th29;
end;
theorem Th75:
z/.1 = N-min L~z & N-min L~z <> W-max L~z implies (W-min L~z)..z
< (W-max L~z)..z
proof
set i1 = (W-min L~z)..z, i2 = (W-max L~z)..z, j = (E-min L~z)..z;
assume that
A1: z/.1 = N-min L~z and
A2: N-min L~z <> W-max L~z and
A3: i1 >= i2;
A4: i2 > j by A1,A2,Lm10;
A5: E-min L~z in rng z by Th45;
then
A6: j in dom z by FINSEQ_4:20;
then
A7: z/.j = z.j by PARTFUN1:def 6
.= E-min L~z by A5,FINSEQ_4:19;
then
A8: (z/.j)`1 = E-bound L~z by EUCLID:52;
A9: j <= len z by A6,FINSEQ_3:25;
A10: z/.len z = N-min L~z by A1,FINSEQ_6:def 1;
A11: W-max L~z in rng z by Th44;
then
A12: i2 in dom z by FINSEQ_4:20;
then
A13: 1 <= i2 by FINSEQ_3:25;
A14: W-min L~z in rng z by Th43;
then
A15: i1 in dom z by FINSEQ_4:20;
then
A16: z/.i1 = z.i1 by PARTFUN1:def 6
.= W-min L~z by A14,FINSEQ_4:19;
A17: i1 <= len z by A15,FINSEQ_3:25;
W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by EUCLID:52,SPRECT_1:13;
then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:24;
then z/.1 = z/.len z & N-min L~z <> W-min L~z by Th57,FINSEQ_6:def 1;
then
A18: i1 < len z by A1,A17,A16,XXREAL_0:1;
then i1 + 1 <= len z by NAT_1:13;
then len z - i1 >= 1 by XREAL_1:19;
then len z -' i1 >= 1 by NAT_D:39;
then
A19: len z -' i1 + 1 >= 1+1 by XREAL_1:6;
A20: 1 <= j by A6,FINSEQ_3:25;
then i1 > 1 by A1,Lm11,XXREAL_0:2;
then reconsider M = mid(z,i1,len z) as S-Sequence_in_R2 by A18,Th38;
A21: len z in dom z by FINSEQ_5:6;
then
A22: M/.1 = z/.i1 by A15,Th8;
1 <= i1 by A15,FINSEQ_3:25;
then
A23: len M = len z -' i1 + 1 by A17,FINSEQ_6:186;
A24: M is_in_the_area_of z by A15,A21,Th21,Th22;
A25: M/.len M = z/.len z by A15,A21,Th9;
N-max L~z in L~z by SPRECT_1:11;
then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:24;
then (N-min L~z)`1 < E-bound L~z by Th51,XXREAL_0:2;
then (N-min L~z)`1 < (E-min L~z)`1 by EUCLID:52;
then
A26: 1 < j by A1,A20,A7,XXREAL_0:1;
A27: i2 <= len z by A12,FINSEQ_3:25;
then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A4,A26,Th37;
A28: z/.i2 = z.i2 by A12,PARTFUN1:def 6
.= W-max L~z by A11,FINSEQ_4:19;
then h/.1 = W-max L~z by A12,A6,Th8;
then
A29: (h/.1)`1 = W-bound L~z by EUCLID:52;
h is_in_the_area_of z & h/.len h = z/.j by A12,A6,Th9,Th21,Th22;
then
A30: len h >= 2 & h is_a_h.c._for z by A8,A29,TOPREAL1:def 8;
W-max L~z <> W-min L~z by Th58;
then i1 > i2 by A3,A28,A16,XXREAL_0:1;
then
A31: L~M misses L~h by A17,A4,A26,Th50;
per cases;
suppose
A32: SW-corner L~z = W-min L~z;
A33: (M/.len M)`2 = N-bound L~z by A10,A25,EUCLID:52;
(M/.1)`2 = S-bound L~z by A16,A22,A32,EUCLID:52;
then M is_a_v.c._for z by A24,A33;
hence contradiction by A30,A31,A23,A19,Th29;
end;
suppose
SW-corner L~z <> W-min L~z;
then reconsider g = <*SW-corner L~z*>^M as S-Sequence_in_R2 by A15,A16,A21
,Th67;
g/.1 = SW-corner L~z by FINSEQ_5:15;
then
A34: (g/.1)`2 = S-bound L~z by EUCLID:52;
len M in dom M & len g = len M + len<*SW-corner L~z*> by FINSEQ_1:22
,FINSEQ_5:6;
then g/.len g = M/.len M by FINSEQ_4:69;
then
A35: (g/.len g)`2 = N-bound L~z by A10,A25,EUCLID:52;
LSeg(M/.1,SW-corner L~z) /\ L~h c= LSeg(M/.1,SW-corner L~z) /\ L~z by A13
,A27,A20,A9,JORDAN4:35,XBOOLE_1:26;
then
A36: LSeg(M/.1,SW-corner L~z) /\ L~h c= {M/.1} by A16,A22,PSCOMP_1:35;
L~g = L~M \/ LSeg(SW-corner L~z,M/.1) & M/.1 in L~M by A23,A19,JORDAN3:1
,SPPOL_2:20;
then
A37: L~g misses L~h by A31,A36,ZFMISC_1:125;
<*SW-corner L~z*> is_in_the_area_of z by Th28;
then g is_in_the_area_of z by A24,Th24;
then len g >= 2 & g is_a_v.c._for z by A34,A35,TOPREAL1:def 8;
hence contradiction by A30,A37,Th29;
end;
end;
theorem
z/.1 = N-min L~z implies (W-min L~z)..z < len z
proof
assume
A1: z/.1 = N-min L~z;
A2: W-max L~z in rng z by Th44;
A3: W-min L~z in rng z by Th43;
per cases;
suppose
N-min L~z = W-max L~z;
then
A4: z/.len z = W-max L~z by A1,FINSEQ_6:def 1;
A5: (W-min L~z)..z in dom z by A3,FINSEQ_4:20;
then
A6: (W-min L~z)..z <= len z by FINSEQ_3:25;
z/.((W-min L~z)..z) = z.((W-min L~z)..z) by A5,PARTFUN1:def 6
.= W-min L~z by A3,FINSEQ_4:19;
then (W-min L~z)..z <> len z by A4,Th58;
hence thesis by A6,XXREAL_0:1;
end;
suppose
A7: N-min L~z <> W-max L~z;
(W-max L~z)..z in dom z by A2,FINSEQ_4:20;
then (W-max L~z)..z <= len z by FINSEQ_3:25;
hence thesis by A1,A7,Th75,XXREAL_0:2;
end;
end;
theorem
f/.1 = N-min L~f implies (W-max L~f)..f < len f
proof
assume
A1: f/.1 = N-min L~f;
then
A2: f/.len f = N-min L~f by FINSEQ_6:def 1;
A3: W-max L~f in rng f by Th44;
then (W-max L~f)..f in dom f by FINSEQ_4:20;
then
A4: f/.((W-max L~f)..f) = f.((W-max L~f)..f) by PARTFUN1:def 6
.= W-max L~f by A3,FINSEQ_4:19;
per cases;
suppose
N-min L~f = W-max L~f;
then (W-max L~f)..f = 1 by A1,FINSEQ_6:43;
hence thesis by GOBOARD7:34,XXREAL_0:2;
end;
suppose
A5: N-min L~f <> W-max L~f;
(W-max L~f)..f <= len f by A3,FINSEQ_4:21;
hence thesis by A2,A4,A5,XXREAL_0:1;
end;
end;