The abstract of the Mizar article:

Some Properties of Cells and Gauges

by

Adam Grabowski,

Artur Kornilowicz, and

Andrzej Trybulec

Received October 13, 2000

MML identifier: JORDAN1C

[ Mizar article, MML identifier index ]

environ

 vocabulary TOPREAL2, PRE_TOPC, EUCLID, JORDAN2C, ARYTM, ARYTM_1, INT_1,
      ARYTM_3, PCOMPS_1, MATRIX_1, JORDAN8, METRIC_1, ABSVALUE, MCART_1,
      TREES_1, FINSEQ_1, PSCOMP_1, GROUP_1, GOBOARD5, FUNCT_5, RELAT_1,
      LATTICES, SQUARE_1, RCOMP_1, COMPTS_1, BOOLE, SEQ_2, ORDINAL2, REALSET1,
      FUNCT_1, JORDAN1A, CONNSP_1, SUBSET_1, RELAT_2, CONNSP_3, TOPS_1,
      SPPOL_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1,
      INT_1, SQUARE_1, STRUCT_0, NAT_1, FINSEQ_1, MATRIX_1, ABSVALUE, RELAT_1,
      RCOMP_1, TOPS_1, SEQ_4, FUNCT_2, PRE_TOPC, CARD_4, BINARITH, CONNSP_1,
      COMPTS_1, EUCLID, PCOMPS_1, METRIC_1, METRIC_6, TOPREAL2, GOBOARD5,
      JORDAN8, JORDAN2C, CONNSP_3, SPPOL_1, PSCOMP_1, GOBRD14, SEQ_2, JORDAN1A;
 constructors JORDAN8, REAL_1, CARD_4, PSCOMP_1, BINARITH, JORDAN2C, CONNSP_1,
      JORDAN9, GOBRD14, JORDAN1A, WSIERP_1, TOPREAL2, TBSP_1, CONNSP_3, TOPS_1,
      JORDAN1, ABSVALUE, SQUARE_1, GOBOARD2, RCOMP_1, PARTFUN1, INT_1;
 clusters XREAL_0, JORDAN8, INT_1, EUCLID, GOBRD14, BORSUK_2, JORDAN1A,
      JORDAN1B, STRUCT_0, PSCOMP_1, PRE_TOPC, WAYBEL_2, SPRECT_4, SEQ_2,
      RELSET_1, SEQ_1, TOPREAL6, MEMBERED, ORDINAL2, NUMBERS;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

reserve C for Simple_closed_curve,
        i, j, n for Nat,
        p for Point of TOP-REAL 2;

canceled;

theorem :: JORDAN1C:2
  [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) =
    Gauge(C,n)*(i+1,j)`1 - Gauge(C,n)*(i,j)`1;

theorem :: JORDAN1C:3
  [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) =
    Gauge(C,n)*(i,j+1)`2 - Gauge(C,n)*(i,j)`2;

theorem :: JORDAN1C:4  :: JORDAN1A:27
 for S being Subset of TOP-REAL 2 st S is Bounded
  holds proj1.:S is bounded;

theorem :: JORDAN1C:5
    for C1 being non empty compact Subset of TOP-REAL 2,
      C2, S being non empty Subset of TOP-REAL 2 holds
   S = C1 \/ C2 & proj1.:C2 is non empty bounded_below
    implies W-bound S = min(W-bound C1, W-bound C2);

theorem :: JORDAN1C:6  :: PSCOMP_1:68
 for X being Subset of TOP-REAL 2 holds
  p in X & X is Bounded implies
   W-bound X <= p`1 & p`1 <= E-bound X &
   S-bound X <= p`2 & p`2 <= N-bound X;

theorem :: JORDAN1C:7
    p in west_halfline p & p in east_halfline p &
   p in north_halfline p & p in south_halfline p;

theorem :: JORDAN1C:8
  west_halfline p is non Bounded;

theorem :: JORDAN1C:9
  east_halfline p is non Bounded;

theorem :: JORDAN1C:10
  north_halfline p is non Bounded;

theorem :: JORDAN1C:11
  south_halfline p is non Bounded;

definition let C be compact Subset of TOP-REAL 2;
 cluster UBD C -> non empty;
end;

theorem :: JORDAN1C:12
  for C being compact Subset of TOP-REAL 2 holds
  UBD C is_a_component_of C`;

theorem :: JORDAN1C:13
  for C being compact Subset of TOP-REAL 2
  for WH being connected Subset of TOP-REAL 2 st
   WH is non Bounded & WH misses C holds WH c= UBD C;

theorem :: JORDAN1C:14
  for C being compact Subset of TOP-REAL 2
  for p being Point of TOP-REAL 2 st
   west_halfline p misses C holds west_halfline p c= UBD C;

theorem :: JORDAN1C:15
  for C being compact Subset of TOP-REAL 2
  for p being Point of TOP-REAL 2 st
   east_halfline p misses C holds east_halfline p c= UBD C;

theorem :: JORDAN1C:16
  for C being compact Subset of TOP-REAL 2
  for p being Point of TOP-REAL 2 st
   south_halfline p misses C holds south_halfline p c= UBD C;

theorem :: JORDAN1C:17
  for C being compact Subset of TOP-REAL 2
  for p being Point of TOP-REAL 2 st
   north_halfline p misses C holds north_halfline p c= UBD C;

theorem :: JORDAN1C:18
  for C being compact Subset of TOP-REAL 2 holds
  BDD C <> {} implies W-bound C <= W-bound BDD C;

theorem :: JORDAN1C:19
  for C being compact Subset of TOP-REAL 2 holds
  BDD C <> {} implies E-bound C >= E-bound BDD C;

theorem :: JORDAN1C:20
  for C being compact Subset of TOP-REAL 2 holds
  BDD C <> {} implies S-bound C <= S-bound BDD C;

theorem :: JORDAN1C:21
  for C being compact Subset of TOP-REAL 2 holds
  BDD C <> {} implies N-bound C >= N-bound BDD C;

theorem :: JORDAN1C:22
  for C being compact non vertical Subset of TOP-REAL 2
  for I being Integer st p in BDD C &
  I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds
    1 < I;

theorem :: JORDAN1C:23
  for C being compact non vertical Subset of TOP-REAL 2
  for I being Integer st p in BDD C &
  I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds
    I + 1 <= len Gauge (C, n);

theorem :: JORDAN1C:24
  for C being compact non horizontal Subset of TOP-REAL 2
  for J being Integer st p in BDD C &
   J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds
    1 < J & J+1 <= width Gauge (C, n);

theorem :: JORDAN1C:25
  for I being Integer st
    I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds
  (W-bound C) + (((E-bound C)-(W-bound C))/(2|^n))*(I-2) <= p`1;

theorem :: JORDAN1C:26
  for I being Integer st
    I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds
  p`1 < (W-bound C) + (((E-bound C)-(W-bound C))/(2|^n))*(I-1);

theorem :: JORDAN1C:27
  for J being Integer st
    J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds
  (S-bound C) + ((N-bound C - S-bound C)/(2|^n))*(J-2) <= p`2;

theorem :: JORDAN1C:28
  for J being Integer st
    J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds
  p`2 < (S-bound C) + ((N-bound C - S-bound C)/(2|^n))*(J-1);

theorem :: JORDAN1C:29
  for C being closed Subset of TOP-REAL 2,
      p being Point of Euclid 2 st p in BDD C
   ex r being Real st r > 0 & Ball(p,r) c= BDD C;

theorem :: JORDAN1C:30
  for p, q being Point of TOP-REAL 2,
      r being real number st
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r &
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r &
   p in cell (Gauge (C, n), i, j) & q in cell (Gauge (C, n), i, j) &
   1 <= i & i+1 <= len Gauge (C,n) & 1 <= j & j+1 <= width Gauge(C,n) holds
    dist (p,q) < 2 * r;

theorem :: JORDAN1C:31
    for C being compact Subset of TOP-REAL 2 holds
  p in BDD C implies p`2 <> N-bound BDD C;

theorem :: JORDAN1C:32
    for C being compact Subset of TOP-REAL 2 holds
  p in BDD C implies p`1 <> E-bound BDD C;

theorem :: JORDAN1C:33
    for C being compact Subset of TOP-REAL 2 holds
  p in BDD C implies p`2 <> S-bound BDD C;

theorem :: JORDAN1C:34
  for C being compact Subset of TOP-REAL 2 holds
  p in BDD C implies p`1 <> W-bound BDD C;

theorem :: JORDAN1C:35
   p in BDD C implies
  ex n,i,j being Nat st
   1 < i & i < len Gauge(C,n) & 1 < j & j < width Gauge(C,n) &
    p`1 <> (Gauge(C,n)*(i,j))`1 &
    p in cell(Gauge(C,n),i,j) & cell(Gauge(C,n),i,j) c= BDD C;

theorem :: JORDAN1C:36
    for C being Subset of TOP-REAL 2 st C is Bounded holds UBD C is non empty;