:: Gauges
:: by Czes\law Byli\'nski
::
:: Received January 22, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem :: JORDAN8:1
for D being set
for G being Matrix of D holds <*> D is_sequence_on G
proofend;

theorem :: JORDAN8:2
for m being Element of NAT
for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
proofend;

theorem Th3: :: JORDAN8:3
for k being Element of NAT
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k &amp; k + 1 <= len f &amp; f is_sequence_on G holds
ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G &amp; f /. k = G * (i1,j1) &amp; [i2,j2] in Indices G &amp; f /. (k + 1) = G * (i2,j2) &amp; ( ( i1 = i2 &amp; j1 + 1 = j2 ) or ( i1 + 1 = i2 &amp; j1 = j2 ) or ( i1 = i2 + 1 &amp; j1 = j2 ) or ( i1 = i2 &amp; j1 = j2 + 1 ) ) )
proofend;

theorem :: JORDAN8:4
for G being Go-board
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
( f is standard &amp; f is special )
proofend;

theorem :: JORDAN8:5
for G being Go-board
for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 &amp; f is_sequence_on G holds
not f is constant
proofend;

theorem :: JORDAN8:6
for G being Go-board
for p being Point of (TOP-REAL 2)
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G &amp; ex i, j being Element of NAT st
( [i,j] in Indices G &amp; p = G * (i,j) ) &amp; ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G &amp; [i2,j2] in Indices G &amp; f /. (len f) = G * (i1,j1) &amp; p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
f ^ <*p*> is_sequence_on G
proofend;

theorem :: JORDAN8:7
for i, k, j being Element of NAT
for G being Go-board st i + k < len G &amp; 1 <= j &amp; j < width G &amp; cell (G,i,j) meets cell (G,(i + k),j) holds
k <= 1
proofend;

theorem Th8: :: JORDAN8:8
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is vertical iff E-bound C <= W-bound C )
proofend;

theorem Th9: :: JORDAN8:9
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is horizontal iff N-bound C <= S-bound C )
proofend;

definition
let C be Subset of (TOP-REAL 2);
let n be Nat;
deffunc H1( Nat, Nat) ->  Element of the carrier of (TOP-REAL 2) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ($1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ($2 - 2)))]|;
A1: (2 |^ n) + 3 > 0 by NAT_1:3;
func Gauge (C,n) ->  Matrix of (TOP-REAL 2) means :Def1: :: JORDAN8:def 1
( len it = (2 |^ n) + 3 &amp; len it = width it &amp; ( for i, j being Nat st [i,j] in Indices it holds
it * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) );
existence
 ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = (2 |^ n) + 3 &amp; len b1 = width b1 &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
proofend;
uniqueness
 for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = (2 |^ n) + 3 &amp; len b1 = width b1 &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) &amp; len b2 = (2 |^ n) + 3 &amp; len b2 = width b2 &amp; ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Gauge JORDAN8:def_1_:_
 for C being Subset of (TOP-REAL 2)
for n being Nat
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = Gauge (C,n) iff ( len b3 = (2 |^ n) + 3 &amp; len b3 = width b3 &amp; ( for i, j being Nat st [i,j] in Indices b3 holds
b3 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) ) );

registration
let C be non empty Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge (C,n) -> V3() X_equal-in-line Y_equal-in-column ;
coherence
 ( not Gauge (C,n) is empty-yielding &amp; Gauge (C,n) is X_equal-in-line &amp; Gauge (C,n) is Y_equal-in-column )
proofend;
end;

registration
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge (C,n) ->  Y_increasing-in-line X_increasing-in-column ;
coherence
 ( Gauge (C,n) is Y_increasing-in-line &amp; Gauge (C,n) is X_increasing-in-column )
proofend;
end;

theorem Th10: :: JORDAN8:10
for T being non empty Subset of (TOP-REAL 2)
for n being Nat holds len (Gauge (T,n)) >= 4
proofend;

theorem :: JORDAN8:11
for j, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= j &amp; j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (2,j)) `1 = W-bound T
proofend;

theorem :: JORDAN8:12
for j, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= j &amp; j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
proofend;

theorem :: JORDAN8:13
for i, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= i &amp; i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,2)) `2 = S-bound T
proofend;

theorem :: JORDAN8:14
for i, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= i &amp; i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T
proofend;

theorem :: JORDAN8:15
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
proofend;

theorem :: JORDAN8:16
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C
proofend;

theorem :: JORDAN8:17
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,0) misses C
proofend;

theorem :: JORDAN8:18
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) misses C
proofend;