:: On the Order on a Special Polygon :: by Andrzej Trybulec and Yatsuka Nakamura :: :: Received November 30, 1997 :: Copyright (c) 1997-2021 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; begin :: Finite sequences reserve i,j,k,l,m,n for Nat, D for non empty set, f for FinSequence of D; theorem :: SPRECT_2:1 i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies k+ i-'1 in dom f; theorem :: SPRECT_2:2 i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies i -' k + 1 in dom f; theorem :: SPRECT_2:3 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); theorem :: SPRECT_2:4 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); theorem :: SPRECT_2:5 i in dom f & j in dom f implies len mid(f,i,j) >= 1; theorem :: SPRECT_2:6 i in dom f & j in dom f & len mid(f,i,j) = 1 implies i = j; theorem :: SPRECT_2:7 i in dom f & j in dom f implies mid(f,i,j) is non empty; theorem :: SPRECT_2:8 i in dom f & j in dom f implies (mid(f,i,j))/.1 = f/.i; theorem :: SPRECT_2:9 i in dom f & j in dom f implies (mid(f,i,j))/.len mid(f,i,j) = f /.j; begin :: Compact sets on the plane reserve X for compact Subset of TOP-REAL 2; theorem :: SPRECT_2:10 for p being Point of TOP-REAL 2 st p in X & p`2 = N-bound X holds p in N-most X; theorem :: SPRECT_2:11 for p being Point of TOP-REAL 2 st p in X & p`2 = S-bound X holds p in S-most X; theorem :: SPRECT_2:12 for p being Point of TOP-REAL 2 st p in X & p`1 = W-bound X holds p in W-most X; theorem :: SPRECT_2:13 for p being Point of TOP-REAL 2 st p in X & p`1 = E-bound X holds p in E-most X; begin :: Finite sequences on the plane theorem :: SPRECT_2:14 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}; theorem :: SPRECT_2:15 for f being FinSequence of TOP-REAL 2 holds dom X_axis f = dom f; theorem :: SPRECT_2:16 for f being FinSequence of TOP-REAL 2 holds dom Y_axis f = dom f; reserve r for Real; theorem :: SPRECT_2:17 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; theorem :: SPRECT_2:18 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; theorem :: SPRECT_2:19 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; theorem :: SPRECT_2:20 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; 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 :: SPRECT_2:def 1 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 :: SPRECT_2:21 for f being non trivial FinSequence of TOP-REAL 2 holds f is_in_the_area_of f ; theorem :: SPRECT_2:22 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; theorem :: SPRECT_2:23 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; theorem :: SPRECT_2:24 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; theorem :: SPRECT_2:25 for f being non trivial FinSequence of TOP-REAL 2 holds <* NE-corner L~f*> is_in_the_area_of f; theorem :: SPRECT_2:26 for f being non trivial FinSequence of TOP-REAL 2 holds <* NW-corner L~f*> is_in_the_area_of f; theorem :: SPRECT_2:27 for f being non trivial FinSequence of TOP-REAL 2 holds <* SE-corner L~f*> is_in_the_area_of f; theorem :: SPRECT_2:28 for f being non trivial FinSequence of TOP-REAL 2 holds <* SW-corner L~f*> is_in_the_area_of f; begin :: Horizontal and vertical connections definition let f, g be FinSequence of TOP-REAL 2; pred g is_a_h.c._for f means :: SPRECT_2:def 2 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 :: SPRECT_2:def 3 g is_in_the_area_of f & (g/.1)`2 = S-bound L~f & (g/.len g)`2 = N-bound L~f; end; theorem :: SPRECT_2:29 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; begin :: Orientation definition let f be FinSequence of TOP-REAL 2; attr f is clockwise_oriented means :: SPRECT_2:def 4 (Rotate(f,N-min L~f))/.2 in N-most L~f; end; theorem :: SPRECT_2:30 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; registration cluster R^2-unit_square -> compact; end; theorem :: SPRECT_2:31 N-bound R^2-unit_square = 1; theorem :: SPRECT_2:32 W-bound R^2-unit_square = 0; theorem :: SPRECT_2:33 E-bound R^2-unit_square = 1; theorem :: SPRECT_2:34 S-bound R^2-unit_square = 0; theorem :: SPRECT_2:35 N-most R^2-unit_square = LSeg(|[0,1]|,|[1,1]|); theorem :: SPRECT_2:36 N-min R^2-unit_square = |[0,1]|; registration let X be non vertical non horizontal non empty compact Subset of TOP-REAL 2; cluster SpStSeq X -> clockwise_oriented; end; registration cluster clockwise_oriented for non constant standard special_circular_sequence; end; theorem :: SPRECT_2:37 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; theorem :: SPRECT_2:38 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; reserve f for non trivial FinSequence of TOP-REAL 2; theorem :: SPRECT_2:39 N-min L~f in rng f; theorem :: SPRECT_2:40 N-max L~f in rng f; theorem :: SPRECT_2:41 S-min L~f in rng f; theorem :: SPRECT_2:42 S-max L~f in rng f; theorem :: SPRECT_2:43 W-min L~f in rng f; theorem :: SPRECT_2:44 W-max L~f in rng f; theorem :: SPRECT_2:45 E-min L~f in rng f; theorem :: SPRECT_2:46 E-max L~f in rng f; reserve f for non constant standard special_circular_sequence; theorem :: SPRECT_2:47 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); theorem :: SPRECT_2:48 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); theorem :: SPRECT_2:49 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); theorem :: SPRECT_2:50 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); theorem :: SPRECT_2:51 (N-min L~f)`1 < (N-max L~f)`1; theorem :: SPRECT_2:52 N-min L~f <> N-max L~f; theorem :: SPRECT_2:53 (E-min L~f)`2 < (E-max L~f)`2; theorem :: SPRECT_2:54 E-min L~f <> E-max L~f; theorem :: SPRECT_2:55 (S-min L~f)`1 < (S-max L~f)`1; theorem :: SPRECT_2:56 S-min L~f <> S-max L~f; theorem :: SPRECT_2:57 (W-min L~f)`2 < (W-max L~f)`2; theorem :: SPRECT_2:58 W-min L~f <> W-max L~f; theorem :: SPRECT_2:59 LSeg(NW-corner L~f,N-min L~f) misses LSeg(N-max L~f,NE-corner L~ f); theorem :: SPRECT_2:60 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; theorem :: SPRECT_2:61 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; begin :: Appending corners theorem :: SPRECT_2:62 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; theorem :: SPRECT_2:63 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; theorem :: SPRECT_2:64 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; theorem :: SPRECT_2:65 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; theorem :: SPRECT_2:66 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; theorem :: SPRECT_2:67 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; registration let f be non constant standard special_circular_sequence; cluster L~f -> being_simple_closed_curve; end; begin :: The order theorem :: SPRECT_2:68 f/.1 = N-min L~f implies (N-min L~f)..f < (N-max L~f)..f; theorem :: SPRECT_2:69 f/.1 = N-min L~f implies (N-max L~f)..f > 1; reserve z for clockwise_oriented non constant standard special_circular_sequence; theorem :: SPRECT_2:70 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; theorem :: SPRECT_2:71 z/.1 = N-min L~z implies (E-max L~z)..z < (E-min L~z)..z; theorem :: SPRECT_2:72 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; theorem :: SPRECT_2:73 z/.1 = N-min L~z implies (S-max L~z)..z < (S-min L~z)..z; theorem :: SPRECT_2:74 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; theorem :: SPRECT_2:75 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; theorem :: SPRECT_2:76 z/.1 = N-min L~z implies (W-min L~z)..z < len z; theorem :: SPRECT_2:77 f/.1 = N-min L~f implies (W-max L~f)..f < len f;