:: Behaviour of an Arc Crossing a Line :: by Yatsuka Nakamura :: :: Received January 26, 2004 :: Copyright (c) 2004-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, SUBSET_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN6, JORDAN3, TARSKI, REAL_1, RLTOPSP1, MCART_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, CARD_1, SUPINF_2, SPPOL_2, FINSEQ_1, PARTFUN1, XBOOLE_0, FUNCT_1, TOPMETR, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, SEQ_4, STRUCT_0, XXREAL_2, METRIC_1, COMPLEX1, RCOMP_1, PCOMPS_1, RELAT_2, BORSUK_2, GRAPH_1, TOPREAL4, NAT_1, JORDAN20, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, NAT_D, PARTFUN1, FUNCT_2, SEQ_4, FINSEQ_1, STRUCT_0, CONNSP_1, RCOMP_1, METRIC_1, PCOMPS_1, JORDAN5C, JORDAN6, RLVECT_1, RLTOPSP1, EUCLID, TOPMETR, PRE_TOPC, TOPS_2, NUMBERS, PSCOMP_1, BORSUK_2, TOPREAL4, TOPREAL1, SPPOL_2, FINSEQ_6; constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPREAL1, TOPREAL4, PSCOMP_1, BORSUK_2, JORDAN5C, JORDAN6, BINOP_2, NAT_D, SEQ_4, CONVEX1, FINSEQ_6, PCOMPS_1; registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, XXREAL_2, RLTOPSP1, RELAT_1, ORDINAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin theorem :: JORDAN20:1 for P being Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & p in P holds Segment(P,p1,p2,p,p)={p}; theorem :: JORDAN20:2 for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg( p1,p2) & p1`1<=a & p2`1<=a holds p`1<=a; theorem :: JORDAN20:3 for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg( p1,p2) & p1`1>=a & p2`1>=a holds p`1>=a; theorem :: JORDAN20:4 for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg(p1,p2) & p1`1a & p2`1>a holds p`1>a; reserve j for Nat; theorem :: JORDAN20:6 for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st 1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(f,j) & (f/.j)`2=(f/.(j+1))`2 & (f /.j)`1>(f/.(j+1))`1 & LE p,q,L~f,f/.1,f/.(len f) holds p`1>=q`1; theorem :: JORDAN20:7 for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st 1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(f,j) & (f/.j)`2=(f/.(j+1))`2 & (f /.j)`1<(f/.(j+1))`1 & LE p,q,L~f,f/.1,f/.(len f) holds p`1<=q`1; definition let P be Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2, e be Real; pred p is_Lin P,p1,p2,e means :: JORDAN20:def 1 P is_an_arc_of p1,p2 & p in P & p`1=e & ex p4 being Point of TOP-REAL 2 st p4`1e & LE p4,p,P,p1,p2 & for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds p5`1>=e; pred p is_Lout P,p1,p2,e means :: JORDAN20:def 3 P is_an_arc_of p1,p2 & p in P & p`1=e & ex p4 being Point of TOP-REAL 2 st p4`1e & LE p,p4,P,p1,p2 & for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds p5`1>=e; pred p is_OSin P,p1,p2,e means :: JORDAN20:def 5 P is_an_arc_of p1,p2 & p in P & p`1=e & ex p7 being Point of TOP-REAL 2 st LE p7,p,P,p1,p2 & (for p8 being Point of TOP-REAL 2 st LE p7,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds p8`1=e) & for p4 being Point of TOP-REAL 2 st LE p4,p7,P,p1,p2 & p4<>p7 holds (ex p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p7,P,p1,p2 & p5`1>e) & ex p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p7,P,p1,p2 & p6`1p7 holds (ex p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p7,p5,P,p1,p2 & p5`1>e)& ex p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p7,p6,P,p1,p2 & p6`1=e holds ex p3 being Point of TOP-REAL 2 st p3 in P & p3`1=e; theorem :: JORDAN20:9 for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_an_arc_of p1,p2 & p1`1e & p in P & p`1=e holds p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e or p is_OSout P,p1,p2,e; theorem :: JORDAN20:11 for P being Subset of I[01],s being Real st P=[.0,s.[ holds P is open; theorem :: JORDAN20:12 for P being Subset of I[01],s being Real st P=].s,1.] holds P is open; theorem :: JORDAN20:13 for P being non empty Subset of TOP-REAL 2, P1 being Subset of ( TOP-REAL 2)|P,Q being Subset of I[01], f being Function of I[01],(TOP-REAL 2)|P ,s being Real st s<=1 & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st 0<=ss & ss=0 & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s=0 & f is being_homeomorphism & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st sp1 & q<>p2 & Q=P\{q} holds not Q is connected & not ex R being Function of I[01],((TOP-REAL 2)|P)|Q st R is continuous & R.0=p1 & R.1=p2; theorem :: JORDAN20:19 for P being non empty 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 LE q1,q2, P,p1,p2 or LE q2,q1,P,p1,p2; theorem :: JORDAN20:20 :: Another version of TOPMETR3:18 for n being Nat,p1,p2 being Point of TOP-REAL n, P,P1 being non empty Subset of TOP-REAL n st P is_an_arc_of p1,p2 & P1 is_an_arc_of p1,p2 & P1 c= P holds P1=P; theorem :: JORDAN20:21 for P being non empty 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 & p2<>q1 holds Segment(P,p1,p2, q1,p2) is_an_arc_of q1,p2; theorem :: JORDAN20:22 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1, p2 holds Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3) =Segment(P,p1,p2,q1, q3); theorem :: JORDAN20:23 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) = {q2}; theorem :: JORDAN20:24 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 Segment(P,p1,p2,p1,p2)=P; theorem :: JORDAN20:25 for P,Q1 being non empty Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2, P,p1,p2 & Q1 c= P holds Q1= Segment(P,p1,p2,q1,q2); theorem :: JORDAN20:26 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Lin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Lin P,p1,p2,e; theorem :: JORDAN20:27 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Rin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Rin P,p1,p2,e; theorem :: JORDAN20:28 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Lout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Lout P,p1,p2,e; theorem :: JORDAN20:29 for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Rout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Rout P,p1,p2,e; theorem :: JORDAN20:30 for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_S-P_arc_joining p1,p2 & p1`1e & p in P & p`1=e holds p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e;