:: The {F}ashoda Meet Theorem for Continuous Mappings
:: by Yatsuka Nakamura , Andrzej Trybulec and Artur Korni{\l}owicz
::
:: Copyright (c) 2005-2021 Association of Mizar Users

Lm1:
by ;

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
let a, b, c, d be Real;
cluster closed_inside_of_rectangle (a,b,c,d) -> convex ;
coherence
closed_inside_of_rectangle (a,b,c,d) is convex
proof end;
end;

registration
let a, b, c, d be Real;
cluster Trectangle (a,b,c,d) -> convex ;
coherence
Trectangle (a,b,c,d) is convex
by PRE_TOPC:8;
end;

theorem Th1: :: JGRAPH_8:1
for n being Nat
for e being positive Real
for g being continuous Function of I,() ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I & h is increasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () 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 ()
for P being Subset of () 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 ()
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 ()
for p1, p2, q1, q2 being Point of ()
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 () st p in P holds
( p1 1 <= p 1 & p 1 <= p2 1 ) ) & ( for p being Point of () st p in Q holds
( p1 1 <= p 1 & p 1 <= p2 1 ) ) & ( for p being Point of () st p in P holds
( q1 2 <= p 2 & p 2 <= q2 2 ) ) & ( for p being Point of () 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,()
for O, I being Point of I 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 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 () 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 st h . s = v . t
proof end;