:: by Czes\law Byli\'nski

::

:: Received January 22, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

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

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

proof end;

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 & k + 1 <= len f & f is_sequence_on G holds

ex i1, j1, i2, j2 being Element of NAT st

( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

ex i1, j1, i2, j2 being Element of NAT st

( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )

proof end;

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 & f is special )

for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

( f is standard & f is special )

proof end;

theorem :: JORDAN8:5

for G being Go-board

for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds

not f is constant

for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds

not f is constant

proof end;

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 & 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 & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds

(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds

f ^ <*p*> is_sequence_on G

for p being Point of (TOP-REAL 2)

for f being non empty 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 & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds

(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds

f ^ <*p*> is_sequence_on G

proof end;

theorem :: JORDAN8:7

for i, k, j being Element of NAT

for G being Go-board st i + k < len G & 1 <= j & j < width G & cell (G,i,j) meets cell (G,(i + k),j) holds

k <= 1

for G being Go-board st i + k < len G & 1 <= j & j < width G & cell (G,i,j) meets cell (G,(i + k),j) holds

k <= 1

proof end;

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 )

( C is vertical iff E-bound C <= W-bound C )

proof end;

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 )

( C is horizontal iff N-bound C <= S-bound C )

proof end;

definition

let C be Subset of (TOP-REAL 2);

let n be Nat;

deffunc H_{1}( 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;

ex b_{1} being Matrix of (TOP-REAL 2) st

( len b_{1} = (2 |^ n) + 3 & len b_{1} = width b_{1} & ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (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)))]| ) )

for b_{1}, b_{2} being Matrix of (TOP-REAL 2) st len b_{1} = (2 |^ n) + 3 & len b_{1} = width b_{1} & ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (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)))]| ) & len b_{2} = (2 |^ n) + 3 & len b_{2} = width b_{2} & ( for i, j being Nat st [i,j] in Indices b_{2} holds

b_{2} * (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

b_{1} = b_{2}

end;
let n be Nat;

deffunc H

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 & len it = width it & ( 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 ( len it = (2 |^ n) + 3 & len it = width it & ( 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)))]| ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Gauge JORDAN8:def 1 :

for C being Subset of (TOP-REAL 2)

for n being Nat

for b_{3} being Matrix of (TOP-REAL 2) holds

( b_{3} = Gauge (C,n) iff ( len b_{3} = (2 |^ n) + 3 & len b_{3} = width b_{3} & ( for i, j being Nat st [i,j] in Indices b_{3} holds

b_{3} * (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)))]| ) ) );

for C being Subset of (TOP-REAL 2)

for n being Nat

for b

( b

b

registration

let C be non empty Subset of (TOP-REAL 2);

let n be Nat;

coherence

( not Gauge (C,n) is empty-yielding & Gauge (C,n) is X_equal-in-line & Gauge (C,n) is Y_equal-in-column )

end;
let n be Nat;

coherence

( not Gauge (C,n) is empty-yielding & Gauge (C,n) is X_equal-in-line & Gauge (C,n) is Y_equal-in-column )

proof end;

registration

let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Nat;

coherence

( Gauge (C,n) is Y_increasing-in-line & Gauge (C,n) is X_increasing-in-column )

end;
let n be Nat;

coherence

( Gauge (C,n) is Y_increasing-in-line & Gauge (C,n) is X_increasing-in-column )

proof end;

theorem :: JORDAN8:11

for j, n being Element of NAT

for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (2,j)) `1 = W-bound T

for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (2,j)) `1 = W-bound T

proof end;

theorem :: JORDAN8:12

for j, n being Element of NAT

for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T

for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T

proof end;

theorem :: JORDAN8:13

for i, n being Element of NAT

for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (i,2)) `2 = S-bound T

for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (i,2)) `2 = S-bound T

proof end;

theorem :: JORDAN8:14

for i, n being Element of NAT

for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T

for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds

((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T

proof end;

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

for i, n being Nat st i <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C

proof end;

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

for j, n being Nat st j <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C

proof end;

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

for i, n being Nat st i <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),i,0) misses C

proof end;

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

for j, n being Nat st j <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),0,j) misses C

proof end;