:: The Ordering of Points on a Curve, Part { II } :: 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, SUBSET_1, EUCLID, PRE_TOPC, FUNCT_1, BORSUK_1, RELAT_1, REAL_1, TOPS_2, CARD_1, XXREAL_0, ARYTM_3, XBOOLE_0, ORDINAL2, STRUCT_0, RCOMP_1, TOPREAL1, TARSKI, JORDAN3, XXREAL_1, FINSEQ_1, PARTFUN1, RLTOPSP1, ARYTM_1, TREAL_1, VALUED_1, TOPMETR, NAT_1, SUPINF_2, JORDAN5C, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, REAL_1, XCMPLX_0, XREAL_0, NAT_1, RCOMP_1, RELAT_1, FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, TOPMETR, JORDAN3, STRUCT_0, TOPREAL1, PRE_TOPC, TOPS_2, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TREAL_1, XXREAL_0; constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1, TREAL_1, JORDAN3; registrations FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPREAL1, SPPOL_1, XREAL_0, NAT_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: First and last point of a curve theorem :: JORDAN5C:1 for P, Q being Subset of TOP-REAL 2, p1, p2, q1 being Point of TOP-REAL 2, f being Function of I[01], (TOP-REAL 2)|P, s1 be Real st q1 in P & f.s1 = q1 & f is being_homeomorphism & f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 & (for t being Real st 0 <= t & t < s1 holds not f.t in Q) for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = q1 & 0 <= s2 & s2 <= 1 for t being Real st 0 <= t & t < s2 holds not g.t in Q; definition let P, Q be Subset of TOP-REAL 2, p1, p2 be Point of TOP-REAL 2; assume that P meets Q & P /\ Q is closed and P is_an_arc_of p1,p2; func First_Point(P,p1,p2,Q) -> Point of TOP-REAL 2 means :: JORDAN5C:def 1 it in P /\ Q & for g being Function of I[01], (TOP-REAL 2)|P, s2 being Real st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = it & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g.t in Q; end; theorem :: JORDAN5C:2 for P, Q being Subset of TOP-REAL 2, p, p1, p2 being Point of TOP-REAL 2 st p in P & P is_an_arc_of p1, p2 & Q = {p} holds First_Point (P,p1,p2,Q) = p ; theorem :: JORDAN5C:3 for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st p1 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds First_Point (P, p1, p2, Q) = p1; theorem :: JORDAN5C:4 for P, Q being Subset of TOP-REAL 2, p1, p2, q1 being Point of TOP-REAL 2, f being Function of I[01], (TOP-REAL 2)|P, s1 be Real st q1 in P & f.s1 = q1 & f is being_homeomorphism & f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 & (for t being Real st 1 >= t & t > s1 holds not f.t in Q) for g being Function of I[01], (TOP-REAL 2)|P, s2 being Real st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = q1 & 0 <= s2 & s2 <= 1 for t being Real st 1 >= t & t > s2 holds not g.t in Q; definition let P, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume that P meets Q & P /\ Q is closed and P is_an_arc_of p1,p2; func Last_Point (P,p1,p2,Q) -> Point of TOP-REAL 2 means :: JORDAN5C:def 2 it in P /\ Q & for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = it & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g.t in Q; end; theorem :: JORDAN5C:5 for P, Q being Subset of TOP-REAL 2, p, p1,p2 being Point of TOP-REAL 2 st p in P & P is_an_arc_of p1, p2 & Q = {p} holds Last_Point (P, p1, p2, Q) = p; theorem :: JORDAN5C:6 for P,Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st p2 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds Last_Point (P, p1, p2, Q) = p2; theorem :: JORDAN5C:7 for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st P c= Q & P is closed & P is_an_arc_of p1, p2 holds First_Point (P , p1, p2, Q) = p1 & Last_Point (P, p1, p2, Q) = p2; begin :: The ordering of points on a curve definition let P be Subset of TOP-REAL 2, p1, p2, q1, q2 be Point of TOP-REAL 2; pred LE q1, q2, P, p1, p2 means :: JORDAN5C:def 3 q1 in P & q2 in P & for g being Function of I[01], (TOP-REAL 2)|P, s1, s2 being Real st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g. s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2; end; theorem :: JORDAN5C:8 for P being Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2, g being Function of I[01], (TOP-REAL 2)|P, s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P ,p1,p2; theorem :: JORDAN5C:9 for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 st q1 in P holds LE q1,q1,P,p1,p2; theorem :: JORDAN5C:10 for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P holds LE p1,q1,P,p1,p2 & LE q1,p2, P,p1,p2; theorem :: JORDAN5C:11 for P being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds LE p1,p2,P,p1,p2; theorem :: JORDAN5C:12 for P being Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds q1=q2; theorem :: JORDAN5C:13 for P being Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of TOP-REAL 2 st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds LE q1,q3,P,p1,p2; theorem :: JORDAN5C:14 for P being Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2 st P is_an_arc_of p1, p2 & q1 in P & q2 in P & q1 <> q2 holds LE q1, q2,P,p1,p2 & not LE q2,q1,P,p1,p2 or LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2; begin :: Some properties of the ordering of points on a curve theorem :: JORDAN5C:15 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, q being Point of TOP-REAL 2 st f is being_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds LE First_Point(L~f,f/.1,f/.len f,Q), q, L~f, f /.1, f/.len f; theorem :: JORDAN5C:16 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, q being Point of TOP-REAL 2 st f is being_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds LE q, Last_Point(L~f,f/.1,f/.len f,Q), L~f, f /.1, f/.len f; theorem :: JORDAN5C:17 for q1, q2, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds LE q1, q2, LSeg(p1, p2), p1, p2 implies LE q1, q2, p1, p2; theorem :: JORDAN5C:18 for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds First_Point(P,p1, p2,Q) = Last_Point(P,p2,p1,Q) & Last_Point(P,p1,p2,Q) = First_Point(P,p2,p1,Q); theorem :: JORDAN5C:19 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, i being Nat st L~f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i+1 <= len f & First_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds First_Point (L~f, f/.1, f/.len f, Q) = First_Point (LSeg (f, i), f/.i, f/.(i+1), Q); theorem :: JORDAN5C:20 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, i being Nat st L~f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i+1 <= len f & Last_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds Last_Point (L~f, f/.1, f/.len f, Q) = Last_Point (LSeg (f, i) , f/.i, f/.(i+1), Q); theorem :: JORDAN5C:21 for f being FinSequence of TOP-REAL 2, i be Nat st 1 <= i & i+1 <= len f & f is being_S-Seq & First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i) holds First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.i; theorem :: JORDAN5C:22 for f being FinSequence of TOP-REAL 2, i be Nat st 1 <= i & i+1 <= len f & f is being_S-Seq & Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i) holds Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.(i+1) ; theorem :: JORDAN5C:23 for f be FinSequence of TOP-REAL 2, i be Nat st f is being_S-Seq & 1 <= i & i+1 <= len f holds LE f/.i, f/.(i+1), L~f, f/.1, f/.len f; theorem :: JORDAN5C:24 for f be FinSequence of TOP-REAL 2, i, j be Nat st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds LE f/.i, f/.j, L~f, f/.1, f/.len f; theorem :: JORDAN5C:25 for f being FinSequence of TOP-REAL 2, q being Point of TOP-REAL 2, i being Nat st f is being_S-Seq & 1 <= i & i+1 <= len f & q in LSeg(f,i) holds LE f/.i, q, L~f, f/.1, f/.len f; theorem :: JORDAN5C:26 for f being FinSequence of TOP-REAL 2, q being Point of TOP-REAL 2, i being Nat st f is being_S-Seq & 1<=i & i+1<=len f & q in LSeg(f ,i) holds LE q, f/.(i+1), L~f, f/.1, f/.len f; theorem :: JORDAN5C:27 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, q being Point of TOP-REAL 2, i, j being Nat st L~f meets Q & f is being_S-Seq & Q is closed & First_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1 <=i & i+1<=len f & q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point (L~f,f/.1,f/.len f,Q) <> q holds i <= j & (i=j implies LE First_Point(L~f,f/.1,f/.len f,Q), q, f/.i, f/.(i+1)); theorem :: JORDAN5C:28 for f being FinSequence of TOP-REAL 2, Q being Subset of TOP-REAL 2, q being Point of TOP-REAL 2, i, j being Nat st L~f meets Q & f is being_S-Seq & Q is closed & Last_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<= i & i+1<=len f & q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point (L~f,f/.1,f/.len f,Q) <> q holds i >= j & (i=j implies LE q, Last_Point(L~f,f/. 1,f/.len f,Q), f/.i, f/.(i+1)); theorem :: JORDAN5C:29 for f being FinSequence of TOP-REAL 2, q1, q2 being Point of TOP-REAL 2, i being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f holds LE q1, q2, L~f, f/.1, f/.len f implies LE q1, q2, LSeg (f,i), f/.i, f/.(i+1); theorem :: JORDAN5C:30 for f being FinSequence of TOP-REAL 2, q1, q2 being Point of TOP-REAL 2 st q1 in L~f & q2 in L~f & f is being_S-Seq & q1 <> q2 holds LE q1, q2, L~f, f/.1, f/.len f iff for i, j being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,j) & 1 <= i & i+1 <= len f & 1 <= j & j+1 <= len f holds i <= j & (i = j implies LE q1,q2,f/.i,f/.(i+1));