:: On a Dividing Function of the Simple Closed Curve into Segments :: by Yatsuka Nakamura :: :: Received June 16, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin Lm1: 2 -' 1 = 2 - 1 by XREAL_1:233 .= 1 ; Lm2: for i, j, k being Element of NAT st i -' k <= j holds i <= j + k proofend; Lm3: for i, j, k being Element of NAT st j + k <= i holds k <= i -' j proofend; theorem Th1: :: JORDAN7:1 for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P ) proofend; theorem Th2: :: JORDAN7:2 for P being non empty compact Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q, W-min P,P holds q = W-min P proofend; theorem Th3: :: JORDAN7:3 for P being non empty compact Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds LE W-min P,q,P proofend; definition let P be non empty compact Subset of (TOP-REAL 2); let q1, q2 be Point of (TOP-REAL 2); func Segment (q1,q2,P) -> Subset of (TOP-REAL 2) equals :Def1: :: JORDAN7:def 1 { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } if q2 <> W-min P otherwise { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ; correctness coherence ( ( q2 <> W-min P implies { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } is Subset of (TOP-REAL 2) ) & ( not q2 <> W-min P implies { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } is Subset of (TOP-REAL 2) ) ); consistency for b1 being Subset of (TOP-REAL 2) holds verum; proofend; end; :: deftheorem Def1 defines Segment JORDAN7:def_1_:_ for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) holds ( ( q2 <> W-min P implies Segment (q1,q2,P) = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies Segment (q1,q2,P) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) ); theorem :: JORDAN7:4 for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ( Segment ((W-min P),(E-max P),P) = Upper_Arc P & Segment ((E-max P),(W-min P),P) = Lower_Arc P ) proofend; theorem Th5: :: JORDAN7:5 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P holds ( q1 in P & q2 in P ) proofend; theorem Th6: :: JORDAN7:6 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P holds ( q1 in Segment (q1,q2,P) & q2 in Segment (q1,q2,P) ) proofend; theorem Th7: :: JORDAN7:7 for P being non empty compact Subset of (TOP-REAL 2) for q1 being Point of (TOP-REAL 2) st q1 in P & P is being_simple_closed_curve holds q1 in Segment (q1,(W-min P),P) proofend; theorem :: JORDAN7:8 for P being non empty compact Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P & q <> W-min P holds Segment (q,q,P) = {q} proofend; theorem :: JORDAN7:9 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P holds not W-min P in Segment (q1,q2,P) proofend; theorem Th10: :: JORDAN7:10 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & ( not q2 = q3 or not q2 = W-min P ) holds (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2} proofend; theorem Th11: :: JORDAN7:11 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & q1 <> W-min P & q2 <> W-min P holds (Segment (q1,q2,P)) /\ (Segment (q2,(W-min P),P)) = {q2} proofend; theorem Th12: :: JORDAN7:12 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & q1 <> q2 & q1 <> W-min P holds (Segment (q2,(W-min P),P)) /\ (Segment ((W-min P),q1,P)) = {(W-min P)} proofend; theorem Th13: :: JORDAN7:13 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2, q3, q4 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P & q1 <> q2 & q2 <> q3 holds Segment (q1,q2,P) misses Segment (q3,q4,P) proofend; theorem Th14: :: JORDAN7:14 for P being non empty compact Subset of (TOP-REAL 2) for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1 <> W-min P & q2 <> q3 holds Segment (q1,q2,P) misses Segment (q3,(W-min P),P) proofend; begin theorem Th15: :: JORDAN7:15 for n being Element of NAT for P being non empty Subset of (TOP-REAL n) for f being Function of I[01],((TOP-REAL n) | P) st f is being_homeomorphism holds ex g being Function of I[01],(TOP-REAL n) st ( f = g & g is continuous & g is one-to-one ) proofend; theorem Th16: :: JORDAN7:16 for n being Element of NAT for P being non empty Subset of (TOP-REAL n) for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds ex f being Function of I[01],((TOP-REAL n) | P) st ( f = g & f is being_homeomorphism ) proofend; Lm4: now__::_thesis:_for_h2_being_Element_of_NAT_holds_(h2_-_1)_-_1_<_h2 let h2 be Element of NAT ; ::_thesis: (h2 - 1) - 1 < h2 h2 < h2 + 1 by NAT_1:13; then A1: h2 - 1 < (h2 + 1) - 1 by XREAL_1:9; then (h2 - 1) - 1 < h2 - 1 by XREAL_1:9; hence (h2 - 1) - 1 < h2 by A1, XXREAL_0:2; ::_thesis: verum end; Lm5: 0 in [.0,1.] by XXREAL_1:1; Lm6: 1 in [.0,1.] by XXREAL_1:1; theorem Th17: :: JORDAN7:17 for A being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 holds ex g being Function of I[01],(TOP-REAL 2) st ( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 ) proofend; theorem Th18: :: JORDAN7:18 for P being non empty 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) for s1, s2 being Real st P is_an_arc_of p1,p2 & g is continuous & g is one-to-one & rng g = P & 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 Th19: :: JORDAN7:19 for P being non empty 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) for s1, s2 being Real st g is continuous & g is one-to-one & rng g = P & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & LE q1,q2,P,p1,p2 holds s1 <= s2 proofend; theorem :: JORDAN7:20 for P being non empty compact Subset of (TOP-REAL 2) for e being Real st P is being_simple_closed_curve & e > 0 holds ex h being FinSequence of the carrier of (TOP-REAL 2) st ( h . 1 = W-min P & h is one-to-one & 8 <= len h & rng h c= P & ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),P ) & ( for i being Element of NAT for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),P) holds diameter W < e ) & ( for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),P) holds diameter W < e ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),P)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),P)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),P)) /\ (Segment ((h /. 1),(h /. 2),P)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),P)) /\ (Segment ((h /. (len h)),(h /. 1),P)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),P) misses Segment ((h /. 1),(h /. 2),P) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),P) misses Segment ((h /. j),(h /. (j + 1)),P) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),P) misses Segment ((h /. i),(h /. (i + 1)),P) ) ) proofend;