The abstract of the Mizar article:

Gauges and Cages. Part II

by

Artur Kornilowicz, and

Robert Milewski

Received November 6, 2000

MML identifier: JORDAN1D

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, EUCLID, COMPTS_1, RELAT_2, SPPOL_1, NAT_1, BOOLE, TARSKI,
      MATRIX_2, INT_1, GROUP_1, ARYTM_3, ARYTM_1, FINSEQ_1, JORDAN8, MCART_1,
      PSCOMP_1, TREES_1, MATRIX_1, GOBOARD5, SETFAM_1, JORDAN9, PRE_TOPC,
      JORDAN1A, TOPREAL1, GOBOARD1, FINSEQ_4, RELAT_1, FUNCT_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SETFAM_1, ORDINAL1, XCMPLX_0, XREAL_0,
      REAL_1, INT_1, NAT_1, FUNCT_1, STRUCT_0, FINSEQ_1, FINSEQ_4, BINARITH,
      NEWTON, PRE_TOPC, COMPTS_1, CONNSP_1, MATRIX_1, EUCLID, WSIERP_1,
      GOBOARD1, TOPREAL1, GOBOARD5, PSCOMP_1, SPPOL_1, ABIAN, GOBRD13, JORDAN8,
      JORDAN9, JORDAN1A;
 constructors JORDAN8, REAL_1, CARD_4, PSCOMP_1, BINARITH, CONNSP_1, JORDAN9,
      JORDAN1A, WSIERP_1, ABSVALUE, FINSEQ_4, GOBRD13, TOPREAL2, ENUMSET1,
      ABIAN, REALSET1, INT_1;
 clusters XREAL_0, TOPREAL6, JORDAN8, INT_1, NEWTON, RELSET_1, EUCLID,
      JORDAN1A, ABIAN, BINARITH, GRAPH_3, NAT_1, SPRECT_1, STRUCT_0, MEMBERED;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;


begin  :: Preliminaries

reserve
   a, b, i, k, m, n for Nat,
   r, s for real number,
   D for non empty Subset of TOP-REAL 2,
   C for compact connected non vertical non horizontal Subset of TOP-REAL 2;

theorem :: JORDAN1D:1
 for A, B being set st
  for x being set st x in A ex K being set st K c= B & x c= union K
 holds union A c= union B;

definition let m be even Integer;
 cluster m + 2 -> even;
end;

definition let m be odd Integer;
 cluster m + 2 -> odd;
end;

definition
  let m be non empty Nat;
 cluster 2|^m -> even;
end;

definition
  let n be even Nat, m be non empty Nat;
 cluster n|^m -> even;
end;

theorem :: JORDAN1D:2
 r <> 0 implies 1/r * r|^(i+1) = r|^i;

theorem :: JORDAN1D:3
 r/s is not Integer implies
  - [\ r/s /] = [\ (-r) / s /] + 1;

theorem :: JORDAN1D:4
 r/s is Integer implies
  - [\ r/s /] = [\ (-r) / s /];

theorem :: JORDAN1D:5
   n > 0 & k mod n <> 0 implies - (k div n) = (-k) div n + 1;

theorem :: JORDAN1D:6
   n > 0 & k mod n = 0 implies - (k div n) = (-k) div n;

begin  :: Gauges and Cages

theorem :: JORDAN1D:7
 2 <= m & m < len Gauge(D,i) &
 1 <= a & a <= len Gauge(D,i) & 1 <= b & b <= len Gauge(D,i+1)
 implies
  Gauge(D,i)*(m,a)`1 = Gauge(D,i+1)*(2*m-'2,b)`1;

theorem :: JORDAN1D:8
 2 <= n & n < len Gauge(D,i) &
 1 <= a & a <= len Gauge(D,i) & 1 <= b & b <= len Gauge(D,i+1)
 implies
  Gauge(D,i)*(a,n)`2 = Gauge(D,i+1)*(b,2*n-'2)`2;

theorem :: JORDAN1D:9
 for D being compact non vertical non horizontal Subset of TOP-REAL 2 holds
 2 <= m & m+1 < len Gauge(D,i) & 2 <= n & n+1 < len Gauge(D,i) implies
 cell(Gauge(D,i),m,n) =
  cell(Gauge(D,i+1),2*m-'2,2*n-'2) \/ cell(Gauge(D,i+1),2*m-'1,2*n-'2) \/
  cell(Gauge(D,i+1),2*m-'2,2*n-'1) \/ cell(Gauge(D,i+1),2*m-'1,2*n-'1);

theorem :: JORDAN1D:10
   for D being compact non vertical non horizontal Subset of TOP-REAL 2,
     k being Nat holds
 2 <= m & m+1 < len Gauge(D,i) & 2 <= n & n+1 < len Gauge(D,i) implies
 cell(Gauge(D,i),m,n) =
  union { cell(Gauge(D,i+k),a,b) where a, b is Nat:
   2|^k*m - 2|^(k+1) + 2 <= a & a <= 2|^k*m - 2|^k + 1 &
   2|^k*n - 2|^(k+1) + 2 <= b & b <= 2|^k*n - 2|^k + 1 };

  theorem :: JORDAN1D:11
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    N-max C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:12
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    N-max C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:13
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    E-min C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:14
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    E-min C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:15
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    E-max C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:16
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    E-max C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:17
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    S-min C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:18
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    S-min C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:19
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    S-max C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:20
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    S-max C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:21
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    W-min C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:22
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    W-min C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:23
   ex i being Nat st 1 <= i & i < len Cage(C,n) &
    W-max C in right_cell(Cage(C,n),i,Gauge(C,n));

  theorem :: JORDAN1D:24
     ex i being Nat st 1 <= i & i < len Cage(C,n) &
    W-max C in right_cell(Cage(C,n),i);

  theorem :: JORDAN1D:25
   ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    N-min L~Cage(C,n) = Gauge(C,n)*(i,width Gauge(C,n));

  theorem :: JORDAN1D:26
     ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    N-max L~Cage(C,n) = Gauge(C,n)*(i,width Gauge(C,n));

  theorem :: JORDAN1D:27
     ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    Gauge(C,n)*(i,width Gauge(C,n)) in rng Cage(C,n);

  theorem :: JORDAN1D:28
   ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    E-min L~Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),j);

  theorem :: JORDAN1D:29
     ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    E-max L~Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),j);

  theorem :: JORDAN1D:30
     ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    Gauge(C,n)*(len Gauge(C,n),j) in rng Cage(C,n);

  theorem :: JORDAN1D:31
   ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    S-min L~Cage(C,n) = Gauge(C,n)*(i,1);

  theorem :: JORDAN1D:32
     ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    S-max L~Cage(C,n) = Gauge(C,n)*(i,1);

  theorem :: JORDAN1D:33
     ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
    Gauge(C,n)*(i,1) in rng Cage(C,n);

  theorem :: JORDAN1D:34
   ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    W-min L~Cage(C,n) = Gauge(C,n)*(1,j);

  theorem :: JORDAN1D:35
     ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    W-max L~Cage(C,n) = Gauge(C,n)*(1,j);

  theorem :: JORDAN1D:36
     ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
    Gauge(C,n)*(1,j) in rng Cage(C,n);