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

theorem Th1: :: JORDAN1F:1

for i, j, k being Element of 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 Element of NAT st
( j <= n & n <= k & (G * i,n) `2 = inf (proj2 .: ((LSeg (G * i,j),(G * i,k)) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:2

for i, j, k being Element of 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 Element of NAT st
( j <= n & n <= k & (G * i,n) `2 = sup (proj2 .: ((LSeg (G * i,j),(G * i,k)) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:3

for j, i, k being Element of 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 Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = inf (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) )

proof end;

theorem :: JORDAN1F:4

for j, i, k being Element of 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 Element of NAT st
( j <= n & n <= k & (G * n,i) `1 = sup (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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st
( [i,j] in Indices G & p = G * i,j ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * i1,j1 & f /. 1 = G * i2,j2 holds
(abs (i2 - i1)) + (abs (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 Element of NAT holds Lower_Seq C,n is_sequence_on Gauge C,n

proof end;

theorem :: JORDAN1F:13

for i being Element of 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 = inf (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 Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )

proof end;