:: The Ordering of Points on a Curve, Part { I } :: by Adam Grabowski and Yatsuka Nakamura :: :: Received September 10, 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, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, STRUCT_0, BORSUK_1, PRE_TOPC, EUCLID, MCART_1, RLTOPSP1, REAL_1, RELAT_1, SUPINF_2, XXREAL_1, FINSEQ_1, XBOOLE_0, SUBSET_1, FUNCT_1, TOPREAL1, TOPS_2, PARTFUN1, TOPMETR, TREAL_1, VALUED_1, FUNCT_4, RCOMP_1, TARSKI, ORDINAL2, PCOMPS_1, METRIC_1, JORDAN3, RFINSEQ, FINSEQ_5, GROUP_2, ORDINAL4, GOBOARD5, GOBOARD2, TREES_1, TOPREAL4, GOBOARD1, MATRIX_1, FUNCT_2; notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RCOMP_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4, TOPMETR, FINSEQ_6, SEQ_4, JORDAN3, STRUCT_0, TOPREAL1, RFINSEQ, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, RLVECT_1, RLTOPSP1, EUCLID, TREAL_1, METRIC_1, GOBOARD1, GOBOARD2, MATRIX_0, TOPREAL4, GOBOARD5, FUNCT_4, FINSEQ_5, PCOMPS_1; constructors FUNCT_4, REAL_1, SEQ_4, RCOMP_1, FINSEQ_4, RFINSEQ, NAT_D, FINSEQ_5, TOPS_2, COMPTS_1, TREAL_1, TOPREAL4, GOBOARD2, GOBOARD5, JORDAN3, GOBOARD1, CONVEX1, BINOP_2, PCOMPS_1, MONOID_0; registrations FUNCT_1, RELSET_1, FUNCT_2, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, GOBOARD2, GOBOARD5, VALUED_0, XXREAL_2, RLTOPSP1, SEQ_4, SPPOL_2, NAT_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries theorem :: JORDAN5B:1 for i1 being Nat st 1 <= i1 holds i1-'1 q`2 & p1 in LSeg (p, q) holds ( p1`2 = p`2 implies p1 = p ); theorem :: JORDAN5B:6 for p, q, p1 being Point of TOP-REAL 2 st p`1 <> q`1 & p1 in LSeg (p, q) holds ( p1`1 = p`1 implies p1 = p ); theorem :: JORDAN5B:7 for f being FinSequence of TOP-REAL 2, P being non empty Subset of TOP-REAL 2, F being Function of I[01], (TOP-REAL 2) | P, i being Nat st 1 <= i & i+1 <= len f & f is being_S-Seq & P = L~f & F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.len f ex p1, p2 being Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f, i) = F.:[.p1, p2.] & F.p1 = f/.i & F.p2 = f/.(i+1); theorem :: JORDAN5B:8 for f being FinSequence of TOP-REAL 2, Q, R being non empty Subset of TOP-REAL 2, F being Function of I[01], (TOP-REAL 2)|Q, i being Nat, P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.len f & 1 <= i & i+1 <= len f & F.:P = LSeg (f,i) & Q = L~f & R = LSeg(f,i) ex G being Function of I[01]|P, (TOP-REAL 2)|R st G = F|P & G is being_homeomorphism; begin :: Some properties of real intervals theorem :: JORDAN5B:9 for p1, p2, p being Point of TOP-REAL 2 st p1 <> p2 & p in LSeg(p1,p2) holds LE p,p,p1,p2; theorem :: JORDAN5B:10 for p, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 & p in LSeg(p1,p2) holds LE p1,p,p1,p2; theorem :: JORDAN5B:11 for p, p1, p2 being Point of TOP-REAL 2 st p in LSeg(p1,p2) & p1 <> p2 holds LE p,p2,p1,p2; theorem :: JORDAN5B:12 for p1, p2, q1, q2, q3 being Point of TOP-REAL 2 st p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds LE q1,q3,p1,p2; theorem :: JORDAN5B:13 for p, q being Point of TOP-REAL 2 st p <> q holds LSeg (p, q) = { p1 where p1 is Point of TOP-REAL 2 : LE p, p1, p, q & LE p1, q, p, q }; theorem :: JORDAN5B:14 for n being Nat, P being Subset of TOP-REAL n, p1, p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1; theorem :: JORDAN5B:15 for i being Nat, f being FinSequence of TOP-REAL 2, P being Subset of TOP-REAL 2 st f is being_S-Seq & 1 <= i & i+1 <= len f & P = LSeg(f,i) holds P is_an_arc_of f/.i, f/.(i+1); begin :: Cutting off sequences theorem :: JORDAN5B:16 for g1 being FinSequence of TOP-REAL 2, i being Nat st 1 <= i & i <= len g1 & g1 is being_S-Seq holds g1/.1 in L~mid(g1, i, len g1) implies i = 1; theorem :: JORDAN5B:17 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 holds L_Cut (f,p) = <*p*>; theorem :: JORDAN5B:18 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f & p <> f.len f & f is being_S-Seq holds Index (p, L_Cut(f,p)) = 1; theorem :: JORDAN5B:19 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f & f is being_S-Seq & p <> f.len f holds p in L~L_Cut (f,p); theorem :: JORDAN5B:20 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f & f is being_S-Seq & p <> f.1 holds p in L~R_Cut (f,p); theorem :: JORDAN5B:21 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f & f is one-to-one holds B_Cut(f,p,p) = <*p*>; theorem :: JORDAN5B:22 for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st p in L~f & q in L~f & q <> f.len f & p = f.len f & f is being_S-Seq holds p in L~L_Cut(f,q); theorem :: JORDAN5B:23 for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st p <> f.len f & p in L~f & q in L~f & f is being_S-Seq holds p in L~L_Cut(f,q) or q in L~L_Cut(f,p); theorem :: JORDAN5B:24 for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st p in L~f & q in L~f & f is being_S-Seq holds L~B_Cut(f,p,q) c= L~f; theorem :: JORDAN5B:25 for f being non constant standard special_circular_sequence, i, j being Nat st 1 <= i & j <= len GoB f & i < j holds LSeg((GoB f)*(1,width GoB f), (GoB f)*(i,width GoB f)) /\ LSeg((GoB f)*(j,width GoB f), (GoB f)*(len GoB f,width GoB f)) = {}; theorem :: JORDAN5B:26 for f being non constant standard special_circular_sequence, i, j being Nat st 1 <= i & j <= width GoB f & i < j holds LSeg((GoB f)*(len GoB f,1), (GoB f)*(len GoB f,i)) /\ LSeg((GoB f)*(len GoB f,j), (GoB f)*(len GoB f,width GoB f)) = {}; theorem :: JORDAN5B:27 for f being FinSequence of TOP-REAL 2 st f is being_S-Seq holds L_Cut (f,f/.1) = f; theorem :: JORDAN5B:28 for f being FinSequence of TOP-REAL 2 st f is being_S-Seq holds R_Cut (f,f/.len f) = f; theorem :: JORDAN5B:29 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds p in LSeg ( f/.Index(p,f), f/.(Index(p,f)+1) ); theorem :: JORDAN5B:30 for f be FinSequence of TOP-REAL 2 for i be Nat st f is unfolded s.n.c. one-to-one & len f >= 2 & f/.1 in LSeg (f,i) holds i = 1; theorem :: JORDAN5B:31 for f be non constant standard special_circular_sequence, j be Nat, P be Subset of TOP-REAL 2 st 1 <= j & j <= width GoB f & P = LSeg ((GoB f)*(1,j), (GoB f)*(len (GoB f),j)) holds P is_S-P_arc_joining (GoB f)*(1,j), (GoB f)*(len (GoB f),j); theorem :: JORDAN5B:32 for f be non constant standard special_circular_sequence, j be Nat, P be Subset of TOP-REAL 2 st 1 <= j & j <= len GoB f & P = LSeg ((GoB f)*(j,1), (GoB f)*(j,width GoB f)) holds P is_S-P_arc_joining (GoB f)*(j,1), (GoB f)*(j,width GoB f); theorem :: JORDAN5B:33 for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f & ( Index(p,f) < Index(q,f) or Index(p,f) = Index(q,f) & LE p,q,f/.Index(p,f),f/.(Index(p,f)+1) ) & p <> q holds L~B_Cut(f,p,q) c= L~f;