The abstract of the Mizar article:

Gauges

by

Czeslaw Bylinski

Received January 22, 1999

MML identifier: JORDAN8

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, MATRIX_1, RELAT_1, FINSEQ_4, BOOLE, FUNCT_1, GOBOARD1,
      ABSVALUE, ARYTM_1, RFINSEQ, PRE_TOPC, EUCLID, GOBOARD5, TOPREAL1,
      GOBOARD2, TREES_1, MCART_1, SEQM_3, COMPTS_1, SPPOL_1, PSCOMP_1, ARYTM_3,
      GROUP_1, INCSP_1, JORDAN8;
 notation TARSKI, XBOOLE_0, ZFMISC_1, XREAL_0, REAL_1, NAT_1, STRUCT_0,
      BINARITH, ABSVALUE, RELAT_1, FUNCT_1, CARD_4, FINSEQ_1, FINSEQ_4,
      RFINSEQ, MATRIX_1, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1,
      GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5;
 constructors REAL_1, ABSVALUE, FINSEQ_4, CARD_4, RFINSEQ, SEQM_3, BINARITH,
      COMPTS_1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5;
 clusters STRUCT_0, RELAT_1, RELSET_1, EUCLID, GOBOARD2, FINSEQ_5, SPRECT_1,
      NAT_1, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve i,i1,i2,i',i1',j,j1,j2,j',j1',k,l,m,n for Nat;
reserve r,s,r',s' for Real;

reserve D for set,
        f for FinSequence of D,
        G for Matrix of D;

theorem :: JORDAN8:1
    len f >= 2 implies f|2 = <*f/.1,f/.2*>;

theorem :: JORDAN8:2
    k+1 <= len f implies f|(k+1) = (f|k)^<*f/.(k+1)*>;

theorem :: JORDAN8:3
    <*>D is_sequence_on G;

canceled;

theorem :: JORDAN8:5
   for D being non empty set, f being FinSequence of D, G being Matrix of D
   st f is_sequence_on G
  holds f/^m is_sequence_on G;

theorem :: JORDAN8:6
  1 <= k & k+1 <= len f & f is_sequence_on G
   implies ex i1,j1,i2,j2 being 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);

reserve G for Go-board,
        p for Point of TOP-REAL 2;

theorem :: JORDAN8:7
   for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G
   holds f is standard special;

theorem :: JORDAN8:8
   for f being non empty FinSequence of TOP-REAL 2 st
    len f >= 2 & f is_sequence_on G
   holds f is non constant;

theorem :: JORDAN8:9
   for f being non empty FinSequence of TOP-REAL 2
   st f is_sequence_on G &
     (ex i,j st [i,j] in Indices G & p = G*(i,j)) &
     (for i1,j1,i2,j2
      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;

theorem :: JORDAN8:10
    i+k < len G & 1 <= j & j < width G & cell(G,i,j) meets cell(G,i+k,j)
    implies k <= 1;

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

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

definition let C be Subset of TOP-REAL 2, n be Nat;

 func Gauge (C,n) -> Matrix of TOP-REAL 2 means
:: JORDAN8:def 1
 len it = 2|^n + 3 & len it = width it &
   for i,j 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)]|;
end;

definition
 let C be non empty Subset of TOP-REAL 2, n be Nat;
 cluster Gauge (C,n) -> non empty-yielding X_equal-in-line Y_equal-in-column;
end;

definition
  let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2,
      n;
 cluster Gauge (C,n) -> Y_increasing-in-line X_increasing-in-column;
end;

reserve T for non empty Subset of TOP-REAL 2;

theorem :: JORDAN8:13
 len Gauge(T,n) >= 4;

theorem :: JORDAN8:14
    1 <= j & j <= len Gauge(T,n) implies Gauge(T,n)*(2,j)`1 = W-bound T;

theorem :: JORDAN8:15
    1 <= j & j <= len Gauge(T,n) implies
    Gauge(T,n)*(len Gauge(T,n)-'1,j)`1 = E-bound T;

theorem :: JORDAN8:16
    1 <= i & i <= len Gauge(T,n) implies Gauge(T,n)*(i,2)`2 = S-bound T;

theorem :: JORDAN8:17
    1 <= i & i <= len Gauge(T,n) implies
    Gauge(T,n)*(i,len Gauge(T,n)-'1)`2 = N-bound T;

reserve C for
   compact non vertical non horizontal non empty Subset of TOP-REAL 2;

theorem :: JORDAN8:18
    i <= len Gauge(C,n) implies cell(Gauge(C,n),i,len Gauge(C,n)) misses C;

theorem :: JORDAN8:19
    j <= len Gauge(C,n) implies cell(Gauge(C,n),len Gauge(C,n),j) misses C;

theorem :: JORDAN8:20
    i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) misses C;

theorem :: JORDAN8:21
    j <= len Gauge(C,n) implies cell(Gauge(C,n),0,j) misses C;