:: On a Dividing Function of the Simple Closed Curve into Segments :: by Yatsuka Nakamura :: :: Received June 16, 1998 :: Copyright (c) 1998-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, PRE_TOPC, EUCLID, ARYTM_1, SUBSET_1, XXREAL_0, ARYTM_3, RCOMP_1, XBOOLE_0, TOPREAL2, PSCOMP_1, JORDAN6, TOPREAL1, JORDAN3, TARSKI, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, STRUCT_0, FINSEQ_1, CARD_1, XXREAL_1, REAL_1, PARTFUN1, MEASURE5, GOBRD10, ORDINAL4, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RCOMP_1, NAT_D, FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1, VALUED_0, TOPREAL1, TOPREAL2, TBSP_1, GOBRD10, PRE_TOPC, TOPS_2, FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, PSCOMP_1, JORDAN5C, JORDAN6, TOPMETR, XXREAL_0; constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, TOPREAL1, PSCOMP_1, GOBRD10, JORDAN5C, JORDAN6, XXREAL_2, FINSEQ_6; registrations RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, FINSEQ_1, FUNCT_1, ORDINAL1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; begin :: Definition of the Segment and its property reserve p,p1,p2,p3,q for Point of TOP-REAL 2; theorem :: JORDAN7:1 for P being compact non empty 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); theorem :: JORDAN7:2 for P being compact non empty Subset of TOP-REAL 2,q st P is being_simple_closed_curve & LE q,W-min(P),P holds q=W-min(P); theorem :: JORDAN7:3 for P being compact non empty Subset of TOP-REAL 2,q st P is being_simple_closed_curve & q in P holds LE W-min(P),q,P; definition let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; func Segment(q1,q2,P) -> Subset of TOP-REAL 2 equals :: JORDAN7:def 1 {p: LE q1,p,P & LE p,q2,P} if q2<>W-min(P) otherwise {p1: LE q1,p1,P or q1 in P & p1=W-min(P)}; end; theorem :: JORDAN7:4 for P being compact non empty 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); theorem :: JORDAN7:5 for P being compact non empty Subset of TOP-REAL 2, 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; theorem :: JORDAN7:6 for P being compact non empty Subset of TOP-REAL 2, 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); theorem :: JORDAN7:7 for P being compact non empty Subset of TOP-REAL 2, 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); theorem :: JORDAN7:8 for P being compact non empty Subset of TOP-REAL 2, 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}; theorem :: JORDAN7:9 for P being compact non empty Subset of TOP-REAL 2, 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); theorem :: JORDAN7:10 for P being compact non empty Subset of TOP-REAL 2, 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 & q1=W-min(P)) & not(q2=q3 & q2=W-min(P)) holds Segment(q1, q2,P)/\ Segment(q2,q3,P)={q2}; theorem :: JORDAN7:11 for P being compact non empty Subset of TOP-REAL 2, 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}; theorem :: JORDAN7:12 for P being compact non empty Subset of TOP-REAL 2, 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)} ; theorem :: JORDAN7:13 for P being compact non empty Subset of TOP-REAL 2, 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); theorem :: JORDAN7:14 for P being compact non empty Subset of TOP-REAL 2, 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); begin :: A function to divide the simple closed curve reserve n for Nat; theorem :: JORDAN7:15 for P being non empty Subset of TOP-REAL n, f being Function of I[01], (TOP-REAL n)|P st f is being_homeomorphism ex g being Function of I[01], TOP-REAL n st f=g & g is continuous & g is one-to-one; theorem :: JORDAN7:16 for P being non empty Subset of TOP-REAL n, g being Function of I[01], (TOP-REAL n) st g is continuous one-to-one & rng g = P ex f being Function of I[01],(TOP-REAL n)|P st f=g & f is being_homeomorphism; theorem :: JORDAN7:17 for A being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st A is_an_arc_of p1,p2 ex g being Function of I[01], TOP-REAL 2 st g is continuous one-to-one & rng g = A & g.0 = p1 & g.1 = p2; theorem :: JORDAN7:18 for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2, g being Function of I[01], TOP-REAL 2, s1, s2 being Real st P is_an_arc_of p1,p2 & g is continuous 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; theorem :: JORDAN7:19 for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2, g being Function of I[01], TOP-REAL 2, s1, s2 being Real st g is continuous 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; theorem :: JORDAN7:20 :: Dividing simple closed curve into segments. for P being compact non empty Subset of TOP-REAL 2, e being Real st P is being_simple_closed_curve & e > 0 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 Nat st 1<=i & i