:: Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem :: by Yatsuka Nakamura :: :: Received August 21, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin theorem Th1: :: JGRAPH_1:1 for G being Graph for IT being oriented Chain of G for vs being FinSequence of the carrier of G st IT is Simple & vs is_oriented_vertex_seq_of IT holds for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) proofend; definition let X be set ; func PGraph X -> MultiGraphStruct equals :: JGRAPH_1:def 1 MultiGraphStruct(# X,[:X,X:],(pr1 (X,X)),(pr2 (X,X)) #); coherence MultiGraphStruct(# X,[:X,X:],(pr1 (X,X)),(pr2 (X,X)) #) is MultiGraphStruct ; end; :: deftheorem defines PGraph JGRAPH_1:def_1_:_ for X being set holds PGraph X = MultiGraphStruct(# X,[:X,X:],(pr1 (X,X)),(pr2 (X,X)) #); 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 :Def2: :: JGRAPH_1:def 2 ( len it = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds it . i = [(f . i),(f . (i + 1))] ) ); existence ex b1 being FinSequence st ( len b1 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds b1 . i = [(f . i),(f . (i + 1))] ) ) proofend; uniqueness for b1, b2 being FinSequence st len b1 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds b1 . i = [(f . i),(f . (i + 1))] ) & len b2 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds b2 . i = [(f . i),(f . (i + 1))] ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines PairF JGRAPH_1:def_2_:_ for f, b2 being FinSequence holds ( b2 = PairF f iff ( len b2 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds b2 . i = [(f . i),(f . (i + 1))] ) ) ); registration let X be non empty set ; cluster PGraph X -> non empty ; coherence not PGraph X is empty ; end; theorem :: JGRAPH_1:3 for X being non empty set for f being FinSequence of X holds f is FinSequence of the carrier of (PGraph X) ; theorem Th4: :: JGRAPH_1:4 for X being non empty set for f being FinSequence of X holds PairF f is FinSequence of the carrier' of (PGraph X) proofend; definition let X be non empty set ; let f be FinSequence of X; :: original:PairF redefine func PairF f -> FinSequence of the carrier' of (PGraph X); coherence PairF f is FinSequence of the carrier' of (PGraph X) by Th4; end; theorem Th5: :: JGRAPH_1:5 for X being non empty set for n being Element of NAT for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds (PairF f) . n in the carrier' of (PGraph X) proofend; theorem Th6: :: JGRAPH_1:6 for X being non empty set for f being FinSequence of X holds PairF f is oriented Chain of PGraph X proofend; definition let X be non empty set ; let f be FinSequence of X; :: original:PairF redefine func PairF f -> oriented Chain of PGraph X; coherence PairF f is oriented Chain of PGraph X by Th6; end; theorem Th7: :: JGRAPH_1:7 for X being non empty set for f being FinSequence of X for f1 being FinSequence of the carrier of (PGraph X) st len f >= 1 & f = f1 holds f1 is_oriented_vertex_seq_of PairF f proofend; begin definition let X be non empty set ; let f, g be FinSequence of X; predg is_Shortcut_of f means :Def3: :: JGRAPH_1:def 3 ( f . 1 = g . 1 & f . (len f) = g . (len g) & ex fc being Subset of (PairF f) ex fvs being Subset of f ex sc being oriented simple Chain of PGraph X ex 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; :: deftheorem Def3 defines is_Shortcut_of JGRAPH_1:def_3_:_ for X being non empty set for f, g being FinSequence of X holds ( g is_Shortcut_of f iff ( f . 1 = g . 1 & f . (len f) = g . (len g) & ex fc being Subset of (PairF f) ex fvs being Subset of f ex sc being oriented simple Chain of PGraph X ex 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 ) ) ); theorem Th8: :: JGRAPH_1:8 for X being non empty set for f, g being FinSequence of X st g is_Shortcut_of f holds ( 1 <= len g & len g <= len f ) proofend; theorem Th9: :: JGRAPH_1:9 for X being non empty set for f being FinSequence of X st len f >= 1 holds ex g being FinSequence of X st g is_Shortcut_of f proofend; theorem Th10: :: JGRAPH_1:10 for X being non empty set for f, g being FinSequence of X st g is_Shortcut_of f holds rng (PairF g) c= rng (PairF f) proofend; theorem Th11: :: JGRAPH_1:11 for X being non empty set for f, g being FinSequence of X st f . 1 <> f . (len f) & g is_Shortcut_of f holds g is one-to-one proofend; definition let n be Element of NAT ; let IT be FinSequence of (TOP-REAL n); attrIT is nodic means :Def4: :: JGRAPH_1:def 4 for i, j being Element of NAT holds ( not LSeg (IT,i) meets LSeg (IT,j) or ( (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; :: deftheorem Def4 defines nodic JGRAPH_1:def_4_:_ for n being Element of NAT for IT being FinSequence of (TOP-REAL n) holds ( IT is nodic iff for i, j being Element of NAT holds ( not LSeg (IT,i) meets LSeg (IT,j) or ( (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) ) ); theorem :: JGRAPH_1:12 for f being FinSequence of (TOP-REAL 2) st f is s.n.c. holds f is s.c.c. proofend; theorem Th13: :: 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. proofend; theorem Th14: :: 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. proofend; theorem Th15: :: 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. proofend; theorem Th16: :: JGRAPH_1:16 for n being Element of NAT for p1, p2, p3 being Point of (TOP-REAL n) holds ( for x being set holds ( not x <> p2 or not x in (LSeg (p1,p2)) /\ (LSeg (p2,p3)) ) or p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) proofend; theorem Th17: :: 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 proofend; theorem Th18: :: JGRAPH_1:18 for X being non empty set for f being FinSequence of X st PairF f is Simple & f . 1 <> f . (len f) holds ( f is one-to-one & len f <> 1 ) proofend; theorem :: JGRAPH_1:19 for X being non empty set for f being FinSequence of X st f is one-to-one & len f > 1 holds ( PairF f is Simple & f . 1 <> f . (len f) ) proofend; 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 proofend; theorem Th21: :: JGRAPH_1:21 for f, g being FinSequence of (TOP-REAL 2) for i being Element of NAT 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) ) proofend; theorem Th22: :: JGRAPH_1:22 for f, g being FinSequence of (TOP-REAL 2) st g is_Shortcut_of f holds rng g c= rng f proofend; theorem Th23: :: JGRAPH_1:23 for f, g being FinSequence of (TOP-REAL 2) st g is_Shortcut_of f holds L~ g c= L~ f proofend; theorem Th24: :: 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 proofend; theorem Th25: :: 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 ) proofend; :: Goboard Theorem for general special sequences theorem Th26: :: 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 proofend; begin theorem Th27: :: JGRAPH_1:27 for a, b, r1, r2 being Real st a <= r1 & r1 <= b & a <= r2 & r2 <= b holds abs (r1 - r2) <= b - a proofend; theorem Th28: :: JGRAPH_1:28 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for x1, x2 being Point of (Euclid n) st x1 = p1 & x2 = p2 holds |.(p1 - p2).| = dist (x1,x2) proofend; theorem Th29: :: JGRAPH_1:29 for p being Point of (TOP-REAL 2) holds |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) proofend; theorem Th30: :: JGRAPH_1:30 for p being Point of (TOP-REAL 2) holds |.p.| = sqrt (((p `1) ^2) + ((p `2) ^2)) proofend; theorem Th31: :: JGRAPH_1:31 for p being Point of (TOP-REAL 2) holds |.p.| <= (abs (p `1)) + (abs (p `2)) proofend; theorem Th32: :: JGRAPH_1:32 for p1, p2 being Point of (TOP-REAL 2) holds |.(p1 - p2).| <= (abs ((p1 `1) - (p2 `1))) + (abs ((p1 `2) - (p2 `2))) proofend; theorem Th33: :: JGRAPH_1:33 for p being Point of (TOP-REAL 2) holds ( abs (p `1) <= |.p.| & abs (p `2) <= |.p.| ) proofend; theorem Th34: :: JGRAPH_1:34 for p1, p2 being Point of (TOP-REAL 2) holds ( abs ((p1 `1) - (p2 `1)) <= |.(p1 - p2).| & abs ((p1 `2) - (p2 `2)) <= |.(p1 - p2).| ) proofend; theorem Th35: :: JGRAPH_1:35 for n being Element of NAT for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds ex r being Real st ( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) ) proofend; theorem Th36: :: JGRAPH_1:36 for n being Element of NAT for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| ) proofend; begin theorem Th37: :: JGRAPH_1:37 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds min_dist_min (P,Q) >= 0 proofend; theorem Th38: :: JGRAPH_1:38 for M being non empty MetrSpace 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 ) proofend; :: Approximation of finite sequence by special finite sequence theorem Th39: :: JGRAPH_1:39 for f being FinSequence of (TOP-REAL 2) for 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 being Element of NAT st 1 <= i & i + 1 <= len f holds |.((f /. i) - (f /. (i + 1))).| < a ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= 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 being Element of NAT st j in dom g holds ex k being Element of NAT st ( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Element of NAT st 1 <= j & j + 1 <= len g holds |.((g /. j) - (g /. (j + 1))).| < a ) ) proofend; theorem Th40: :: JGRAPH_1:40 for f being FinSequence of (TOP-REAL 2) for a, c, d being Real st 1 <= len f & Y_axis f lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_axis f lies_between c,d & a > 0 & ( for i being Element of NAT st 1 <= i & i + 1 <= len f holds |.((f /. i) - (f /. (i + 1))).| < a ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= 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 being Element of NAT st j in dom g holds ex k being Element of NAT st ( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Element of NAT st 1 <= j & j + 1 <= len g holds |.((g /. j) - (g /. (j + 1))).| < a ) ) proofend; theorem Th41: :: JGRAPH_1:41 for f being FinSequence of (TOP-REAL 2) st 1 <= len f holds ( len (X_axis f) = len f & (X_axis f) . 1 = (f /. 1) `1 & (X_axis f) . (len f) = (f /. (len f)) `1 ) proofend; theorem Th42: :: JGRAPH_1:42 for f being FinSequence of (TOP-REAL 2) st 1 <= len f holds ( len (Y_axis f) = len f & (Y_axis f) . 1 = (f /. 1) `2 & (Y_axis f) . (len f) = (f /. (len f)) `2 ) proofend; theorem Th43: :: JGRAPH_1:43 for i being Element of NAT for f being FinSequence of (TOP-REAL 2) st i in dom f holds ( (X_axis f) . i = (f /. i) `1 & (Y_axis f) . i = (f /. i) `2 ) proofend; :: Goboard Theorem in continuous case theorem Th44: :: JGRAPH_1:44 for P, Q being non empty Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( for p being Point of (TOP-REAL 2) st p in P holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds ( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds ( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds P meets Q proofend; theorem Th45: :: JGRAPH_1:45 for X, Y being non empty TopSpace for f being Function of X,Y for P being non empty Subset of Y for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds f1 is continuous proofend; theorem Th46: :: JGRAPH_1:46 for X, Y being non empty TopSpace for f being Function of X,Y for P being non empty Subset of Y st X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f holds ex f1 being Function of X,(Y | P) st ( f = f1 & f1 is being_homeomorphism ) proofend; :: [WP: ] Fashoda_Meet_Theorem theorem :: JGRAPH_1:47 for f, g being Function of I[01],(TOP-REAL 2) for a, b, c, d being real number for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds ( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds rng f meets rng g proofend;