Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### A Decomposition of Simple Closed Curves and the Order of Their Points

**by****Yatsuka Nakamura, and****Andrzej Trybulec**- Received December 19, 1997
- MML identifier: JORDAN6

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, PRE_TOPC, EUCLID, TOPMETR, PCOMPS_1, BORSUK_1, RCOMP_1, ARYTM_3, ARYTM_1, RELAT_1, BOOLE, SUBSET_1, ORDINAL2, FUNCT_1, MCART_1, FINSEQ_1, TOPREAL1, RELAT_2, TOPS_2, COMPTS_1, JORDAN5C, JORDAN3, TREAL_1, SEQ_1, PSCOMP_1, TOPREAL2, SEQ_2, METRIC_1, SEQ_4, ABSVALUE, SQUARE_1, FUNCT_5, JORDAN6; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RCOMP_1, SETWOP_2, STRUCT_0, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, TOPREAL1, TOPREAL2, CONNSP_1, JORDAN2B, SQUARE_1, TSEP_1, TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, METRIC_1, PCOMPS_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1; constructors RCOMP_1, ABSVALUE, TOPREAL2, CONNSP_1, JORDAN2B, TSEP_1, TOPS_2, REAL_1, TOPREAL1, SQUARE_1, SETWOP_2, JORDAN5C, TREAL_1, PSCOMP_1, TSP_1, COMPTS_1, YELLOW_8, PARTFUN1, MEMBERED; clusters SUBSET_1, STRUCT_0, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, METRIC_1, PSCOMP_1, BORSUK_2, TSEP_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Middle Points of Arcs reserve x,y for set; reserve s,r for real number; reserve r1,r2 for Real; reserve n for Nat; reserve p,p3,q,q1,q2,q3 for Point of TOP-REAL 2; canceled; theorem :: JORDAN6:2 r<=s implies r <= (r+s)/2 & (r+s)/2 <= s; theorem :: JORDAN6:3 for TX being non empty TopSpace, P being Subset of TX, A being Subset of TX|P, B being Subset of TX st B is closed & A=B/\P holds A is closed; theorem :: JORDAN6:4 for TX,TY being non empty TopSpace, P being non empty Subset of TY,f being map of TX,TY|P holds f is map of TX,TY & for f2 being map of TX,TY st f2=f & f is continuous holds f2 is continuous; theorem :: JORDAN6:5 for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1>=r} holds P is closed; theorem :: JORDAN6:6 for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1<=r} holds P is closed; theorem :: JORDAN6:7 for r being real number,P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1=r} holds P is closed; theorem :: JORDAN6:8 for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2>=r} holds P is closed; theorem :: JORDAN6:9 for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2<=r} holds P is closed; theorem :: JORDAN6:10 for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2=r} holds P is closed; theorem :: JORDAN6:11 for 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 connected; theorem :: JORDAN6:12 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 P is closed; theorem :: JORDAN6:13 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 ex q being Point of TOP-REAL 2 st q in P & q `1 = (p1 `1+p2 `1)/2; theorem :: JORDAN6:14 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 & Q={q:q`1=(p1`1+p2`1)/2} holds P meets Q & P /\ Q is closed; theorem :: JORDAN6:15 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 & Q={q:q`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed; definition let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; func x_Middle(P,p1,p2) -> Point of TOP-REAL 2 means :: JORDAN6:def 1 for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2} holds it=First_Point(P,p1,p2,Q); end; definition let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; func y_Middle(P,p1,p2) -> Point of TOP-REAL 2 means :: JORDAN6:def 2 for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2} holds it=First_Point(P,p1,p2,Q); end; theorem :: JORDAN6:16 for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P; theorem :: JORDAN6:17 for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds p1=x_Middle(P,p1,p2) iff p1`1=p2`1; theorem :: JORDAN6:18 for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds p1=y_Middle(P,p1,p2) iff p1`2=p2`2; begin ::Segments of Arcs theorem :: JORDAN6:19 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 holds LE q2,q1,P,p2,p1; definition let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; func L_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals :: JORDAN6:def 3 {q : LE q,q1,P,p1,p2}; end; definition let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; func R_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals :: JORDAN6:def 4 {q: LE q1,q,P,p1,p2}; end; theorem :: JORDAN6:20 for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 holds L_Segment(P,p1,p2,q1) c= P; theorem :: JORDAN6:21 for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 holds R_Segment(P,p1,p2,q1) c= P; theorem :: JORDAN6:22 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 L_Segment(P,p1,p2,p1)={p1}; canceled 2; theorem :: JORDAN6:25 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 L_Segment(P,p1,p2,p2)=P; theorem :: JORDAN6:26 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 R_Segment(P,p1,p2,p2)={p2}; theorem :: JORDAN6:27 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 R_Segment(P,p1,p2,p1)=P; theorem :: JORDAN6:28 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 R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1); definition let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; func Segment(P,p1,p2,q1,q2) -> Subset of TOP-REAL 2 equals :: JORDAN6:def 5 R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2); end; theorem :: JORDAN6:29 for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 holds Segment(P,p1,p2,q1,q2)={q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}; theorem :: JORDAN6:30 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 holds LE q1,q2,P,p1,p2 iff LE q2,q1,P,p2,p1; theorem :: JORDAN6:31 for P being Subset of TOP-REAL 2, p1,p2,q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q in P holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q); theorem :: JORDAN6:32 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 holds Segment(P,p1,p2,q1,q2)=Segment(P,p2,p1,q2,q1); begin ::Decomposition of a Simple Closed Curve into Two Arcs definition let s be real number; func Vertical_Line(s) -> Subset of TOP-REAL 2 equals :: JORDAN6:def 6 {p where p is Point of TOP-REAL 2: p`1=s}; func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals :: JORDAN6:def 7 {p: p`2=s}; end; theorem :: JORDAN6:33 for r being real number holds Vertical_Line(r) is closed & Horizontal_Line(r) is closed; theorem :: JORDAN6:34 for r being real number,p being Point of TOP-REAL 2 holds p in Vertical_Line(r) iff p`1=r; theorem :: JORDAN6:35 for r being real number,p being Point of TOP-REAL 2 holds p in Horizontal_Line(r) iff p`2=r; canceled 4; theorem :: JORDAN6:40 for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve ex P1,P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; begin ::Uniqueness of Decomposition of a Simple Closed Curve theorem :: JORDAN6:41 for P being Subset of I[01] st P=(the carrier of I[01]) \{0,1} holds P is open; canceled 2; theorem :: JORDAN6:44 for r,s being real number holds ].r,s.[ misses {r,s}; theorem :: JORDAN6:45 for a,b,c being real number holds c in ].a,b.[ iff a < c & c < b; theorem :: JORDAN6:46 for P being Subset of R^1, r,s being real number st P=].r,s.[ holds P is open; theorem :: JORDAN6:47 for S being non empty TopSpace, P1,P2 being Subset of S, P1' being Subset of S|P2 st P1=P1' & P1 c= P2 holds S|P1=(S|P2)|P1'; theorem :: JORDAN6:48 for P7 being Subset of I[01] st P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected; theorem :: JORDAN6:49 for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds p1<>p2; theorem :: JORDAN6:50 for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is open; ::A proof of the following is almost same as JORDAN5A:1. canceled; theorem :: JORDAN6:52 for P being Subset of TOP-REAL n, P1,P2 being non empty Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2} holds Q is open; theorem :: JORDAN6:53 for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is connected; theorem :: JORDAN6:54 for GX being non empty TopSpace, P1, P being Subset of GX, Q' being Subset of GX|P1, Q being Subset of GX|P st P1 c=P & Q=Q' & Q' is connected holds Q is connected; theorem :: JORDAN6:55 for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 ex p3 being Point of TOP-REAL n st p3 in P & p3<>p1 & p3<>p2; theorem :: JORDAN6:56 for 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\{p1,p2}<>{}; theorem :: JORDAN6:57 for P1 being Subset of TOP-REAL n, P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2} holds Q is connected; theorem :: JORDAN6:58 for T,S,V being non empty TopSpace, P1 being non empty Subset of S, P2 being Subset of S, f being map of T,S|P1, g being map of S|P2,V st P1 c= P2 & f is continuous & g is continuous ex h being map of T,V st h=g*f & h is continuous; theorem :: JORDAN6:59 for P1,P2 being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1=P2; theorem :: JORDAN6:60 for P being non empty Subset of TOP-REAL 2, Q being Subset of (TOP-REAL 2)|P, p1,p2 being Point of TOP-REAL 2 st P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2} holds not Q is connected; theorem :: JORDAN6:61 for P being non empty Subset of TOP-REAL 2, P1,P2,P1',P2' being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2=P & P1' is_an_arc_of p1,p2 & P2' is_an_arc_of p1,p2 & P1' \/ P2'=P holds P1=P1' & P2=P2' or P1=P2' & P2=P1'; begin ::Lower Arcs and Upper Arcs definition cluster -> real Element of R^1; end; canceled 2; theorem :: JORDAN6:64 for P1 being Subset of TOP-REAL 2, r being Real,p1,p2 being Point of TOP-REAL 2 st p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2 holds P1 meets Vertical_Line(r) & P1 /\ Vertical_Line(r) is closed; definition let P be compact non empty Subset of TOP-REAL 2 such that P is_simple_closed_curve; func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means :: JORDAN6:def 8 it is_an_arc_of W-min(P),E-max(P) & ex P2 being non empty Subset of TOP-REAL 2 st P2 is_an_arc_of E-max(P),W-min(P) & it /\ P2={W-min(P),E-max(P)} & it \/ P2=P & First_Point(it,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; end; definition let P be compact non empty Subset of TOP-REAL 2; assume P is_simple_closed_curve; func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means :: JORDAN6:def 9 it is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ it={W-min(P),E-max(P)} & Upper_Arc(P) \/ it=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(it,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; end; theorem :: JORDAN6:65 for P being compact non empty Subset of (TOP-REAL 2) st P is_simple_closed_curve holds Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Upper_Arc(P) is_an_arc_of E-max(P),W-min(P) & Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) & Lower_Arc(P) is_an_arc_of W-min(P),E-max(P) & Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(Lower_Arc(P),E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; theorem :: JORDAN6:66 for P being compact non empty Subset of (TOP-REAL 2) st P is_simple_closed_curve holds Lower_Arc(P)=(P\Upper_Arc(P)) \/ {W-min(P),E-max(P)} & Upper_Arc(P)=(P\Lower_Arc(P)) \/ {W-min(P),E-max(P)}; theorem :: JORDAN6:67 for P being compact non empty Subset of (TOP-REAL 2), P1 being Subset of (TOP-REAL 2)|P st P is_simple_closed_curve & Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P holds P1=Lower_Arc(P); theorem :: JORDAN6:68 for P being compact non empty Subset of (TOP-REAL 2), P1 being Subset of (TOP-REAL 2)|P st P is_simple_closed_curve & P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P holds P1=Upper_Arc(P); begin ::An Order of Points in a Simple Closed Curve theorem :: JORDAN6:69 for P being Subset of TOP-REAL 2, p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds q=p1; theorem :: JORDAN6:70 for P being Subset of TOP-REAL 2, p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds q=p2; definition let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; pred LE q1,q2,P means :: JORDAN6:def 10 q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) or q1 in Upper_Arc(P) & q2 in Upper_Arc(P) & LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) or q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) & LE q1,q2,Lower_Arc(P),E-max(P),W-min(P); end; theorem :: JORDAN6:71 for P being compact non empty Subset of (TOP-REAL 2), q being Point of TOP-REAL 2 st P is_simple_closed_curve & q in P holds LE q,q,P; theorem :: JORDAN6:72 for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1=q2; theorem :: JORDAN6:73 for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds LE q1,q3,P;

Back to top