:: The Ordering of Points on a Curve, Part { II } :: by Adam Grabowski and Yatsuka Nakamura :: :: Received September 10, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin theorem Th1: :: JORDAN5C:1 for P, Q being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being 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 ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q proofend; definition let P, Q be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); assume that A1: ( P meets Q & P /\ Q is closed ) and A2: P is_an_arc_of p1,p2 ; func First_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1 ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for 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 ) ); existence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) proofend; uniqueness for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines First_Point JORDAN5C:def_1_:_ for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds for b5 being Point of (TOP-REAL 2) holds ( b5 = First_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ); theorem :: JORDAN5C:2 for P, Q being Subset of (TOP-REAL 2) for 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 proofend; theorem Th3: :: JORDAN5C:3 for P, Q being Subset of (TOP-REAL 2) for 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 proofend; theorem Th4: :: JORDAN5C:4 for P, Q being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being 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 ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q proofend; definition let P, Q be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); assume that A1: ( P meets Q & P /\ Q is closed ) and A2: P is_an_arc_of p1,p2 ; func Last_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2 ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for 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 1 >= t & t > s2 holds not g . t in Q ) ); existence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) proofend; uniqueness for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Last_Point JORDAN5C:def_2_:_ for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds for b5 being Point of (TOP-REAL 2) holds ( b5 = Last_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ); theorem :: JORDAN5C:5 for P, Q being Subset of (TOP-REAL 2) for 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 proofend; theorem Th6: :: JORDAN5C:6 for P, Q being Subset of (TOP-REAL 2) for 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 proofend; theorem Th7: :: JORDAN5C:7 for P, Q being Subset of (TOP-REAL 2) for 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 ) proofend; begin definition let P be Subset of (TOP-REAL 2); let p1, p2, q1, q2 be Point of (TOP-REAL 2); pred LE q1,q2,P,p1,p2 means :Def3: :: JORDAN5C:def 3 ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P) for 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; :: deftheorem Def3 defines LE JORDAN5C:def_3_:_ for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds ( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P) for 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 ) ) ); theorem Th8: :: JORDAN5C:8 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) for g being Function of I[01],((TOP-REAL 2) | P) for 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 proofend; theorem Th9: :: JORDAN5C:9 for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds LE q1,q1,P,p1,p2 proofend; theorem Th10: :: JORDAN5C:10 for P being Subset of (TOP-REAL 2) for 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 ) proofend; theorem :: JORDAN5C:11 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds LE p1,p2,P,p1,p2 proofend; theorem Th12: :: JORDAN5C:12 for P being Subset of (TOP-REAL 2) for 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 proofend; theorem Th13: :: JORDAN5C:13 for P being Subset of (TOP-REAL 2) for 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 proofend; theorem :: JORDAN5C:14 for P being Subset of (TOP-REAL 2) for 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 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) proofend; begin theorem Th15: :: JORDAN5C:15 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for 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) proofend; theorem Th16: :: JORDAN5C:16 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for 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) proofend; theorem Th17: :: JORDAN5C:17 for q1, q2, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 holds LE q1,q2,p1,p2 proofend; theorem :: JORDAN5C:18 for P, Q being Subset of (TOP-REAL 2) for 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) ) proofend; theorem Th19: :: JORDAN5C:19 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for i being Element of 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) proofend; theorem Th20: :: JORDAN5C:20 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for i being Element of 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) proofend; theorem :: JORDAN5C:21 for f being FinSequence of (TOP-REAL 2) for i being Element of 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 proofend; theorem :: JORDAN5C:22 for f being FinSequence of (TOP-REAL 2) for i being Element of 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) proofend; theorem Th23: :: JORDAN5C:23 for f being FinSequence of (TOP-REAL 2) for i being Element of 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) proofend; theorem Th24: :: JORDAN5C:24 for f being FinSequence of (TOP-REAL 2) for i, j being Element of 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) proofend; Lm1: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) proofend; Lm2: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of 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,i) & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) proofend; Lm3: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) proofend; Lm4: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of 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,i) & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) proofend; theorem Th25: :: JORDAN5C:25 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of 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) proofend; theorem Th26: :: JORDAN5C:26 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of 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) proofend; theorem :: JORDAN5C:27 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of 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) ) ) proofend; theorem :: JORDAN5C:28 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of 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) ) ) proofend; theorem Th29: :: JORDAN5C:29 for f being FinSequence of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) proofend; theorem :: JORDAN5C:30 for f being FinSequence of (TOP-REAL 2) for 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 Element of 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) ) ) ) proofend;