:: Graph Theoretical Properties of Arcs in the Plane and Fashoda :: Meet Theorem :: by Yatsuka Nakamura :: :: Received August 21, 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, GRAPH_1, FINSEQ_1, STRUCT_0, TREES_2, SUBSET_1, REAL_1, GRAPH_4, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0, CARD_1, ZFMISC_1, MCART_1, ARYTM_1, NAT_1, RELAT_1, TARSKI, PARTFUN1, GLIB_000, FINSET_1, EUCLID, RLTOPSP1, TOPREAL1, GOBOARD5, PRE_TOPC, SUPINF_2, GOBOARD1, GOBOARD4, COMPLEX1, METRIC_1, SQUARE_1, RVSUM_1, CARD_3, PCOMPS_1, RCOMP_1, WEIERSTR, INT_1, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, MEASURE5, PSCOMP_1, XXREAL_2, JGRAPH_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, FINSET_1, NAT_1, NAT_D, SEQM_3, GRAPH_1, STRUCT_0, GRAPH_2, GRAPH_4, TOPREAL1, GOBOARD5, PRE_TOPC, GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, TOPS_2, METRIC_1, TBSP_1, RCOMP_1, SQUARE_1, PSCOMP_1, RVSUM_1, RLVECT_1, RLTOPSP1, EUCLID, FUNCT_3; constructors FUNCT_3, REAL_1, SQUARE_1, NAT_D, RCOMP_1, BINARITH, TOPS_2, COMPTS_1, TBSP_1, MONOID_0, GOBOARD1, GOBOARD4, GOBOARD5, PSCOMP_1, GRAPH_2, WEIERSTR, GRAPH_4, XXREAL_2, FUNCSDOM, FINSEQ_6; registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, GRAPH_2, GRAPH_4, FINSET_1, VALUED_0, FUNCT_2, CARD_1, XXREAL_2, TOPREAL1, RELSET_1, SQUARE_1, ORDINAL1, FINSEQ_6; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: GRAPHS BY CARTESIAN PRODUCT reserve x,y for set; reserve G for Graph; reserve vs,vs9 for FinSequence of the carrier of G; reserve IT for oriented Chain of G; reserve N for Nat; reserve n,m,k,i,j for Nat; reserve r,r1,r2 for Real; theorem :: JGRAPH_1:1 for vs st IT is Simple & vs is_oriented_vertex_seq_of IT holds for n,m st 1<=n & n MultiGraphStruct equals :: JGRAPH_1:def 1 MultiGraphStruct(#X,[:X,X:],pr1(X, X),pr2(X,X)#); end; theorem :: JGRAPH_1:2 for X being set holds the carrier of PGraph(X)=X; definition let f be FinSequence; func PairF(f) -> FinSequence means :: JGRAPH_1:def 2 len it=len f-'1 & for i being Nat st 1<=i & i non empty; end; theorem :: JGRAPH_1:3 for f being FinSequence of X holds f is FinSequence of the carrier of PGraph(X); theorem :: JGRAPH_1:4 for f being FinSequence of X holds PairF(f) is FinSequence of the carrier' of PGraph(X); definition let X be non empty set,f be FinSequence of X; redefine func PairF(f) -> FinSequence of the carrier' of PGraph(X); end; theorem :: JGRAPH_1:5 for n being Nat,f being FinSequence of X st 1 <= n & n <= len PairF(f) holds (PairF(f)).n in the carrier' of PGraph(X); theorem :: JGRAPH_1:6 for f being FinSequence of X holds PairF(f) is oriented Chain of PGraph(X); definition let X be non empty set,f be FinSequence of X; redefine func PairF(f) -> oriented Chain of PGraph(X); end; theorem :: JGRAPH_1:7 for f being FinSequence of X, f1 being FinSequence of the carrier of PGraph(X) st len f>=1 & f=f1 holds f1 is_oriented_vertex_seq_of PairF(f); begin :: SHORTCUTS OF FINITE SEQUENCES IN PLANE definition let X be non empty set,f,g be FinSequence of X; pred g is_Shortcut_of f means :: JGRAPH_1:def 3 f.1=g.1 & f.len f=g.len g & ex fc being Subset of PairF(f),fvs being Subset of f, sc being oriented simple Chain of PGraph(X), g1 being FinSequence of the carrier of PGraph(X) st Seq fc = sc & Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc; end; theorem :: JGRAPH_1:8 for f,g being FinSequence of X st g is_Shortcut_of f holds 1<= len g & len g <= len f; theorem :: JGRAPH_1:9 for f being FinSequence of X st len f>=1 holds ex g being FinSequence of X st g is_Shortcut_of f; theorem :: JGRAPH_1:10 for f,g being FinSequence of X st g is_Shortcut_of f holds rng PairF(g) c= rng PairF(f); theorem :: JGRAPH_1:11 for f,g being FinSequence of X st f.1<>f.len f & g is_Shortcut_of f holds g is one-to-one; definition let n; let IT be FinSequence of TOP-REAL n; attr IT is nodic means :: JGRAPH_1:def 4 for i,j st LSeg(IT,i) meets LSeg(IT,j) holds LSeg(IT,i) /\ LSeg(IT,j)={IT.i} &(IT.i=IT.j or IT.i=IT.(j+1)) or LSeg(IT,i) /\ LSeg(IT,j)={IT.(i+1)} &(IT.(i+1)=IT.j or IT.(i+1)=IT.(j+1)) or LSeg(IT,i)=LSeg( IT,j); end; theorem :: JGRAPH_1:12 for f being FinSequence of TOP-REAL 2 st f is s.n.c. holds f is s.c.c.; theorem :: JGRAPH_1:13 for f being FinSequence of TOP-REAL 2 st f is s.c.c. & LSeg(f,1) misses LSeg(f,len f -'1) holds f is s.n.c.; theorem :: JGRAPH_1:14 for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f) is Simple holds f is s.c.c.; theorem :: JGRAPH_1:15 for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is s.n.c.; theorem :: JGRAPH_1:16 for p1,p2,p3 being Point of TOP-REAL n st (ex x being set st x<> p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3)) holds p1 in LSeg(p2,p3) or p3 in LSeg(p1, p2); theorem :: JGRAPH_1:17 for f being FinSequence of TOP-REAL 2 st f is s.n.c. & LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} & LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)} holds f is unfolded; theorem :: JGRAPH_1:18 for f being FinSequence of X holds PairF(f) is Simple & f.1<>f. len f implies f is one-to-one & len f<>1; theorem :: JGRAPH_1:19 for f being FinSequence of X holds f is one-to-one & len f>1 implies PairF(f) is Simple & f.1<>f.len f; theorem :: JGRAPH_1:20 for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is unfolded; theorem :: JGRAPH_1:21 for f,g being FinSequence of TOP-REAL 2,i st g is_Shortcut_of f & 1 <= i & i+1 <= len g holds ex k1 being Element of NAT st 1<=k1 & k1+1<=len f & f/.k1=g/.i & f/.(k1+1)=g/.(i+1) & f.k1=g.i & f.(k1+1)=g.(i+1); theorem :: JGRAPH_1:22 for f,g being FinSequence of TOP-REAL 2 st g is_Shortcut_of f holds rng g c= rng f; theorem :: JGRAPH_1:23 for f,g being FinSequence of TOP-REAL 2 st g is_Shortcut_of f holds L~g c= L~f; theorem :: JGRAPH_1:24 for f,g being FinSequence of TOP-REAL 2 st f is special & g is_Shortcut_of f holds g is special; theorem :: JGRAPH_1:25 for f being FinSequence of TOP-REAL 2 st f is special & 2<=len f & f.1 <> f.len f holds ex g being FinSequence of TOP-REAL 2 st 2<=len g & g is special & g is one-to-one & L~g c= L~f & f.1=g.1 & f.len f=g.len g & rng g c= rng f; :: Goboard Theorem for general special sequences theorem :: JGRAPH_1:26 for f1,f2 being FinSequence of TOP-REAL 2 st f1 is special & f2 is special & 2<=len f1 & 2<=len f2 & f1.1<>f1.len f1 & f2.1<>f2.len f2 & X_axis (f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1) lies_between ( Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds L~f1 meets L~f2; begin :: NORM OF POINTS IN TOPREAL n theorem :: JGRAPH_1:27 for a,b,r1,r2 being Real st a<=r1 & r1<=b & a<=r2 & r2<=b holds |.r1-r2.|<=b-a; reserve p,p1,p2 for Point of TOP-REAL N; theorem :: JGRAPH_1:28 for x1,x2 being Point of Euclid N st x1=p1 & x2=p2 holds |.p1 - p2.| = dist(x1,x2); theorem :: JGRAPH_1:29 for p being Point of TOP-REAL 2 holds |.p.|^2 = (p`1)^2+(p`2)^2; theorem :: JGRAPH_1:30 for p being Point of TOP-REAL 2 holds |.p.| = sqrt((p`1)^2+(p`2) ^2); theorem :: JGRAPH_1:31 for p being Point of TOP-REAL 2 holds |.p.|<=|.p`1.|+|.p`2.|; theorem :: JGRAPH_1:32 for p1,p2 being Point of TOP-REAL 2 holds |.p1-p2.|<=|.p1`1-p2`1.|+|.p1`2-p2`2.|; theorem :: JGRAPH_1:33 for p being Point of TOP-REAL 2 holds |.p`1.|<=|.p.| & |.p`2.| <=|.p.|; theorem :: JGRAPH_1:34 for p1,p2 being Point of TOP-REAL 2 holds |.p1`1-p2`1.|<=|.p1- p2.| & |.p1`2-p2`2.|<=|.p1-p2.|; ::$CT theorem :: JGRAPH_1:36 p in LSeg(p1,p2) implies |.p-p1.|<=|.p1-p2.| & |.p-p2.|<=|.p1-p2 .|; begin :: EXTENDED GOBOARD THEOREM AND FASHODA MEET THEOREM reserve M for non empty MetrSpace; theorem :: JGRAPH_1:37 for P,Q being Subset of TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds min_dist_min(P,Q)>=0; theorem :: JGRAPH_1:38 for P,Q being Subset of TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds P misses Q iff min_dist_min(P,Q)>0; :: Approximation of finite sequence by special finite sequence theorem :: JGRAPH_1:39 for f being FinSequence of TOP-REAL 2, a,c,d being Real st 1<=len f & X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) & Y_axis(f) lies_between c, d & a>0 & (for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .| =len f & X_axis(g) lies_between (X_axis(f)).1, (X_axis(f) ).(len f) & Y_axis(g) lies_between c, d & (for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .|0 & (for i st 1<=i & i+1<=len f holds |. (f/.i)-(f/.(i+1) ) .|=len f & Y_axis(g) lies_between (Y_axis(f)).1, (Y_axis( f)).(len f) & X_axis(g) lies_between c, d & (for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .| < a)& for j st 1<=j & j+1<=len g holds |. g/.j - g/.(j+1) .|