:: Go-Board Theorem
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

theorem Th1: :: GOBOARD4:1

for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
rng f1 meets rng f2

proof end;

theorem Th2: :: GOBOARD4:2

for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2

proof end;

theorem :: GOBOARD4:3

for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2 by Th2;

definition

let f be Relation;
let r, s be Real;

pred f lies_between r,s means :: GOBOARD4:def 1
rng f c= [.r,s.];

end;

:: deftheorem defines lies_between GOBOARD4:def 1 :
for f being Relation
for r, s being Real holds
( f lies_between r,s iff rng f c= [.r,s.] );

definition

let f be FinSequence of REAL ;
let r, s be Real;

redefine pred f lies_between r,s means :: GOBOARD4:def 2
for n being Nat st n in dom f holds
( r <= f . n & f . n <= s );

compatibility
( f lies_between r,s iff for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) )

proof end;

end;

:: deftheorem defines lies_between GOBOARD4:def 2 :
for f being FinSequence of REAL
for r, s being Real holds
( f lies_between r,s iff for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) );

theorem Th4: :: GOBOARD4:4

for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is special & f2 is special & ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) & 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

proof end;

theorem Th5: :: GOBOARD4:5

for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is one-to-one & f1 is special & 2 <= len f1 & f2 is one-to-one & f2 is special & 2 <= 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

proof end;

theorem :: GOBOARD4:6

for P1, P2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P1 meets P2

proof end;