:: A Decomposition of Simple Closed Curves and an Order of Their Points :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received December 19, 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, REAL_1, SUBSET_1, PRE_TOPC, EUCLID, XXREAL_0, ARYTM_3, XBOOLE_0, RELAT_1, RCOMP_1, FUNCT_1, ORDINAL2, STRUCT_0, MCART_1, FINSEQ_1, TARSKI, PARTFUN1, TOPREAL1, RELAT_2, BORSUK_1, TOPS_2, CARD_1, TOPMETR, XXREAL_1, JORDAN5C, JORDAN3, ARYTM_1, TREAL_1, VALUED_1, TOPREAL2, PSCOMP_1, XXREAL_2, SEQ_4, METRIC_1, COMPLEX1, RLTOPSP1, JORDAN6, FUNCT_2, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RCOMP_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, STRUCT_0, TOPREAL1, TOPREAL2, CONNSP_1, TSEP_1, TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, RLTOPSP1, METRIC_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1; constructors REAL_1, COMPLEX1, RCOMP_1, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1, TOPREAL1, TOPREAL2, TREAL_1, PSCOMP_1, JORDAN5C, SEQ_4, MONOID_0, BINOP_2, PCOMPS_1, BINOP_1, NUMBERS; registrations RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, BORSUK_2, MONOID_0, JORDAN2B, MEASURE6, BINOP_2, VALUED_0, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Middle Points of Arcs reserve x,y for set; reserve s,r for Real; reserve r1,r2 for Real; reserve n for Nat; reserve p,q,q1,q2 for Point of TOP-REAL 2; theorem :: JORDAN6:1 r<=s implies r <= (r+s)/2 & (r+s)/2 <= s; theorem :: JORDAN6:2 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:3 for TX,TY being non empty TopSpace, P being non empty Subset of TY,f being Function of TX,TY|P holds f is Function of TX,TY & for f2 being Function of TX,TY st f2=f & f is continuous holds f2 is continuous; theorem :: JORDAN6:4 for r being Real, 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:5 for r being Real, 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,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, 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:8 for r being Real, 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, 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 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: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 P is closed; 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 ex q being Point of TOP-REAL 2 st q in P & q`1 = (p1`1+p2`1)/2; theorem :: JORDAN6:13 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: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`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed; definition let P be 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 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:15 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 x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P; theorem :: JORDAN6:16 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 p1=x_Middle(P,p1,p2) iff p1`1=p2`1; theorem :: JORDAN6:17 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 p1=y_Middle(P,p1,p2) iff p1`2=p2`2; begin ::Segments of Arcs theorem :: JORDAN6:18 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:19 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:20 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:21 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}; 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,p2)=P; theorem :: JORDAN6:23 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:24 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:25 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 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:26 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:27 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 q2,q1,P,p2,p1 holds LE q1,q2,P,p1,p2; theorem :: JORDAN6:28 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 holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q); theorem :: JORDAN6:29 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 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; 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:30 for r being Real holds Vertical_Line(r) is closed & Horizontal_Line(r) is closed; theorem :: JORDAN6:31 for r being Real,p being Point of TOP-REAL 2 holds p in Vertical_Line(r) iff p`1=r; theorem :: JORDAN6:32 for r being Real,p being Point of TOP-REAL 2 holds p in Horizontal_Line(r) iff p`2=r; theorem :: JORDAN6:33 for P being Subset of TOP-REAL 2 st P is being_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:34 for P being Subset of I[01] st P=(the carrier of I[01]) \{0,1} holds P is open; theorem :: JORDAN6:35 for P being Subset of R^1, r,s being Real st P=].r,s.[ holds P is open; theorem :: JORDAN6:36 for P7 being Subset of I[01] st P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected; theorem :: JORDAN6:37 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:38 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. theorem :: JORDAN6:39 for P,P1,P2 being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2} holds Q is open; theorem :: JORDAN6:40 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:41 for GX being TopSpace, P1, P being Subset of GX, Q9 being Subset of GX|P1, Q being Subset of GX|P st P1 c=P & Q=Q9 & Q9 is connected holds Q is connected; theorem :: JORDAN6:42 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:43 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:44 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:45 for T,S,V being non empty TopSpace, P1 being non empty Subset of S, P2 being Subset of S, f being Function of T,S|P1, g being Function of S|P2,V st P1 c= P2 & f is continuous & g is continuous ex h being Function of T,V st h=g*f & h is continuous; theorem :: JORDAN6:46 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:47 for P being Subset of TOP-REAL 2, Q being Subset of (TOP-REAL 2)|P, p1,p2 being Point of TOP-REAL 2 st P is being_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2} holds not Q is connected; theorem :: JORDAN6:48 for P,P1,P2,P19,P29 being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2=P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29=P holds P1=P19 & P2=P29 or P1=P29 & P2=P19; begin theorem :: JORDAN6:49 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 Subset of TOP-REAL 2 such that P is being_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 Subset of TOP-REAL 2; assume P is being_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:50 for P being Subset of TOP-REAL 2 st P is being_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:51 for P being Subset of TOP-REAL 2 st P is being_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:52 for P being Subset of TOP-REAL 2, P1 being Subset of (TOP-REAL 2)|P st P is being_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:53 for P being Subset of TOP-REAL 2, P1 being Subset of (TOP-REAL 2)|P st P is being_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:54 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:55 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 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:56 for P being Subset of TOP-REAL 2, q being Point of TOP-REAL 2 st P is being_simple_closed_curve & q in P holds LE q,q,P; theorem :: JORDAN6:57 for P being Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1=q2; theorem :: JORDAN6:58 for P being 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 holds LE q1,q3,P; theorem :: JORDAN6:59 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 <> p2 holds not p2 in L_Segment(P,p1,p2,q); theorem :: JORDAN6:60 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 <> p1 holds not p1 in R_Segment(P,p1,p2,q); registration let S be non empty being_simple_closed_curve Subset of TOP-REAL 2; cluster Lower_Arc S -> non empty compact; cluster Upper_Arc S -> non empty compact; end; theorem :: JORDAN6:61 for S being being_simple_closed_curve non empty Subset of TOP-REAL 2 holds Lower_Arc S c= S & Upper_Arc S c= S; reserve C for Simple_closed_curve; definition let C be Simple_closed_curve; func Lower_Middle_Point C -> Point of TOP-REAL 2 equals :: JORDAN6:def 11 First_Point(Lower_Arc C,W-min C,E-max C, Vertical_Line((W-bound C+E-bound C)/2)); func Upper_Middle_Point C -> Point of TOP-REAL 2 equals :: JORDAN6:def 12 First_Point(Upper_Arc C,W-min C,E-max C, Vertical_Line((W-bound C+E-bound C)/2)); end; theorem :: JORDAN6:62 Lower_Arc C meets Vertical_Line((W-bound C+E-bound C)/2); theorem :: JORDAN6:63 Upper_Arc C meets Vertical_Line((W-bound C+E-bound C)/2); theorem :: JORDAN6:64 (Lower_Middle_Point C)`1 = (W-bound C+E-bound C)/2; theorem :: JORDAN6:65 (Upper_Middle_Point C)`1 = (W-bound C+E-bound C)/2; theorem :: JORDAN6:66 Lower_Middle_Point C in Lower_Arc C; theorem :: JORDAN6:67 Upper_Middle_Point C in Upper_Arc C; theorem :: JORDAN6:68 Upper_Middle_Point C in C; theorem :: JORDAN6:69 :: JORDAN1B:26: AK, 20.02.2006 for C be Simple_closed_curve for r be Real st W-bound C <= r & r <= E-bound C holds LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C; theorem :: JORDAN6:70 :: JORDAN1B:27: AK, 20.02.2006 for C be Simple_closed_curve for r be Real st W-bound C <= r & r <= E-bound C holds LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C;