:: by Yatsuka Nakamura , Andrzej Trybulec and Artur Korni{\l}owicz

::

:: Received September 14, 2005

:: Copyright (c) 2005-2016 Association of Mizar Users

Lm1: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))

by TOPMETR:20, TOPMETR:def 7;

Lm2: for x being set

for f being FinSequence st 1 <= len f holds

( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )

proof end;

Lm3: for f being FinSequence of REAL st ( for k being Nat st 1 <= k & k < len f holds

f /. k < f /. (k + 1) ) holds

f is increasing

proof end;

registration
end;

theorem Th1: :: JGRAPH_8:1

for n being Nat

for e being positive Real

for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st

( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat

for Q being Subset of I[01]

for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds

diameter W < e ) )

for e being positive Real

for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st

( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat

for Q being Subset of I[01]

for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds

diameter W < e ) )

proof end;

theorem Th2: :: JGRAPH_8:2

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds

P = LSeg (p1,p2)

for p1, p2 being Point of (TOP-REAL n)

for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds

P = LSeg (p1,p2)

proof end;

theorem Th3: :: JGRAPH_8:3

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds

rng g = LSeg (p1,p2)

for p1, p2 being Point of (TOP-REAL n)

for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds

rng g = LSeg (p1,p2)

proof end;

:: Goboard Theorem in continuous case

theorem Th4: :: JGRAPH_8:4

for P, Q being non empty Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for f being Path of p1,p2

for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for f being Path of p1,p2

for g being Path of q1,q2 st rng f = P & rng g = Q & ( 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

proof end;

:: Fashoda Meet Theorem

theorem Th5: :: JGRAPH_8:5

for a, b, c, d being Real

for f, g being continuous Function of I[01],(TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & (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

for f, g being continuous Function of I[01],(TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & (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

proof end;

theorem :: JGRAPH_8:6

for a, b, c, d being Real

for ar, br, cr, dr being Point of (Trectangle (a,b,c,d))

for h being Path of ar,br

for v being Path of dr,cr

for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds

ex s, t being Point of I[01] st h . s = v . t

for ar, br, cr, dr being Point of (Trectangle (a,b,c,d))

for h being Path of ar,br

for v being Path of dr,cr

for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds

ex s, t being Point of I[01] st h . s = v . t

proof end;