:: Some Remarks on Finite Sequences on Go-boards
:: by Adam Naumowicz
::
:: Received August 29, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th1: :: JORDAN1F:1

for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:2

for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:3

for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:4

for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )

proof end;

theorem Th5: :: JORDAN1F:5

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))

proof end;

theorem Th6: :: JORDAN1F:6

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))

proof end;

theorem Th7: :: JORDAN1F:7

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))

proof end;

theorem Th8: :: JORDAN1F:8

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n)))

proof end;

theorem Th9: :: JORDAN1F:9

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )

proof end;

theorem Th10: :: JORDAN1F:10

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq (C,n) is_sequence_on Gauge (C,n)

proof end;

theorem Th11: :: JORDAN1F:11

for G being Go-board
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
<*p*> ^ f is_sequence_on G

proof end;

theorem Th12: :: JORDAN1F:12

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)

proof end;

theorem :: JORDAN1F:13

for i being Nat
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )

proof end;