:: Gauges
::  by Czes\law Byli\'nski
::
:: Received January 22, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, FINSEQ_1, MATRIX_1, GOBOARD1, RELAT_1,
      PARTFUN1, ARYTM_3, COMPLEX1, ARYTM_1, XBOOLE_0, RFINSEQ, XXREAL_0,
      PRE_TOPC, EUCLID, GOBOARD5, TOPREAL1, GOBOARD2, TREES_1, MCART_1, CARD_1,
      NAT_1, FUNCT_1, ORDINAL4, RCOMP_1, SPPOL_1, PSCOMP_1, NEWTON, STRUCT_0,
      ZFMISC_1, INCSP_1, JORDAN8, ORDINAL1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
      NEWTON, RFINSEQ, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, COMPTS_1,
      EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5,
      XXREAL_0;
 constructors NEWTON, RFINSEQ, NAT_D, COMPTS_1, GOBOARD2, SPPOL_1, GOBOARD5,
      PSCOMP_1, GOBOARD1, RELSET_1, REAL_1;
 registrations RELAT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2,
      SPRECT_1, NEWTON, VALUED_0, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,l,m,n for Nat;
reserve r,s,r9,s9 for Real;
reserve D for set,
  f for FinSequence of D,
  G for Matrix of D;

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

theorem :: JORDAN8:2
  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:3
  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:4
  for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G
  holds f is standard special;

theorem :: JORDAN8:5
  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:6
  for f being non empty 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 st [i1,j1] in Indices G & [i2,j2] in Indices G &
  f/.len f = G*(i1,j1) & p = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1)
  holds f^<*p*> is_sequence_on G;

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

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

theorem :: JORDAN8:9
  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 natural Number;
  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 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)]|;
end;

registration
  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;

registration
  let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2,
  n be Nat;
  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:10
  for n being Nat holds len Gauge(T,n) >= 4;

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

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

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

theorem :: JORDAN8:14
  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;
reserve i, j, n for Nat;

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

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

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

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