The abstract of the Mizar article:

Bounding Boxes for Special Sequences in $\calE^2$

by

Yatsuka Nakamura, and

Adam Grabowski

Received June 8, 1998

MML identifier: JORDAN5D

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, SEQM_3, GOBOARD5, FINSEQ_1, SEQ_2, SEQ_4,
      ARYTM_1, TOPREAL1, NAT_1, RELAT_1, FUNCT_1, JORDAN4, GOBOARD2, TREES_1,
      MCART_1, GOBOARD1, MATRIX_1, PSCOMP_1, FUNCT_5, REALSET1, SUBSET_1,
      BOOLE, ORDINAL2, FINSET_1, SQUARE_1, SPPOL_1, JORDAN5D, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MCART_1,
      REAL_1, NAT_1, BINARITH, RELAT_1, FINSEQ_1, FUNCT_1, FINSEQ_4, FINSET_1,
      SEQ_4, MATRIX_1, CQC_SIM1, STRUCT_0, TOPREAL1, SPPOL_1, GOBOARD1,
      GOBOARD2, GOBOARD5, PRE_TOPC, EUCLID, PRE_CIRC, JORDAN4, PSCOMP_1;
 constructors REAL_1, SPPOL_1, CQC_SIM1, GOBOARD2, BINARITH, PRE_CIRC, JORDAN4,
      PSCOMP_1, FINSEQ_4, COMPTS_1, REALSET1;
 clusters EUCLID, GOBOARD2, GOBOARD5, RELSET_1, STRUCT_0, GROUP_2, PRELAMB,
      SPRECT_1, FINSEQ_1, XREAL_0, ARYTM_3, MEMBERED, PRE_CIRC, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

 reserve p, q for Point of TOP-REAL 2,
         r for Real,
         h for non constant standard special_circular_sequence,
         g for FinSequence of TOP-REAL 2,
         f for non empty FinSequence of TOP-REAL 2,
         I, i1, i, j, k for Nat;

canceled 2;

theorem :: JORDAN5D:3
 for n be Nat,
     h be FinSequence of TOP-REAL n st len h >= 2 holds
  h/.len h in LSeg(h,len h-'1);

theorem :: JORDAN5D:4
  3 <= i implies i mod (i-'1) = 1;

theorem :: JORDAN5D:5
  p in rng h implies ex i be Nat st 1 <= i & i+1 <= len h & h.i = p;

theorem :: JORDAN5D:6
  for g being FinSequence of REAL st r in rng g holds
    Incr g.1 <= r & r <= Incr g.len Incr g;

theorem :: JORDAN5D:7
  1 <= i & i <= len h & 1 <= I & I <= width GoB h implies
   (GoB h)*(1,I)`1 <= (h/.i)`1 & (h/.i)`1 <= (GoB h)*(len GoB h,I)`1;

theorem :: JORDAN5D:8
  1 <= i & i <= len h & 1 <= I & I <= len GoB h implies
   (GoB h)*(I,1)`2 <= (h/.i)`2 & (h/.i)`2 <= (GoB h)*(I,width GoB h)`2;

theorem :: JORDAN5D:9
  1 <= i & i <= len GoB f implies
    ex k,j st k in dom f & [i,j] in Indices GoB f & f/.k = (GoB f)*(i,j);

theorem :: JORDAN5D:10
  1 <= j & j <= width GoB f implies
    ex k,i st k in dom f & [i,j] in Indices GoB f & f/.k = (GoB f)*(i,j);

theorem :: JORDAN5D:11
  1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f implies
    ex k st k in dom f & [i,j] in Indices GoB f & (f/.k)`1 = (GoB f)*(i,j)`1;

theorem :: JORDAN5D:12
  1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f implies
    ex k st k in dom f & [i,j] in Indices GoB f & (f/.k)`2 = (GoB f)*(i,j)`2;

begin :: Extrema of projections

theorem :: JORDAN5D:13
  1 <= i & i <= len h implies
    S-bound L~h <= (h/.i)`2 & (h/.i)`2 <= N-bound L~h;

theorem :: JORDAN5D:14
  1 <= i & i <= len h implies
    W-bound L~h <= (h/.i)`1 & (h/.i)`1 <= E-bound L~h;

theorem :: JORDAN5D:15
  for X being Subset of REAL st
    X = { q`2 : q`1 = W-bound L~h & q in L~h } holds
  X = (proj2 || W-most L~h).:the carrier of (TOP-REAL 2)|(W-most L~h);

theorem :: JORDAN5D:16
  for X being Subset of REAL st
    X = { q`2 : q`1 = E-bound L~h & q in L~h } holds
  X = (proj2 || E-most L~h).:the carrier of (TOP-REAL 2)|(E-most L~h);

theorem :: JORDAN5D:17
  for X being Subset of REAL st
    X = { q`1 : q`2 = N-bound L~h & q in L~h } holds
  X = (proj1 || N-most L~h).:the carrier of (TOP-REAL 2)|(N-most L~h);

theorem :: JORDAN5D:18
  for X being Subset of REAL st
    X = { q`1 : q`2 = S-bound L~h & q in L~h } holds
  X = (proj1 || S-most L~h).:the carrier of (TOP-REAL 2)|(S-most L~h);

theorem :: JORDAN5D:19
  for X being Subset of REAL st X = { q`1 : q in L~g } holds
    X = (proj1 || L~g).:the carrier of (TOP-REAL 2)|L~g;

theorem :: JORDAN5D:20
  for X being Subset of REAL st X = { q`2 : q in L~g } holds
    X = (proj2 || L~g).:the carrier of (TOP-REAL 2)|L~g;

theorem :: JORDAN5D:21
  for X being Subset of REAL st
    X = { q`2 : q`1 = W-bound L~h & q in L~h } holds
  lower_bound X = inf (proj2 || W-most L~h);

theorem :: JORDAN5D:22
  for X being Subset of REAL st
    X = { q`2 : q`1 = W-bound L~h & q in L~h } holds
  upper_bound X = sup (proj2 || W-most L~h);

theorem :: JORDAN5D:23
  for X being Subset of REAL st
    X = { q`2 : q`1 = E-bound L~h & q in L~h } holds
  lower_bound X = inf (proj2 || E-most L~h);

theorem :: JORDAN5D:24
  for X being Subset of REAL st
    X = { q`2 : q`1 = E-bound L~h & q in L~h } holds
  upper_bound X = sup (proj2 || E-most L~h);

theorem :: JORDAN5D:25
  for X being Subset of REAL st X = { q`1 : q in L~g } holds
    lower_bound X = inf (proj1 || L~g);

theorem :: JORDAN5D:26
  for X being Subset of REAL st
    X = { q`1 : q`2 = S-bound L~h & q in L~h } holds
  lower_bound X = inf (proj1 || S-most L~h);

theorem :: JORDAN5D:27
  for X being Subset of REAL st
    X = { q`1 : q`2 = S-bound L~h & q in L~h } holds
  upper_bound X = sup (proj1 || S-most L~h);

theorem :: JORDAN5D:28
  for X being Subset of REAL st
    X = { q`1 : q`2 = N-bound L~h & q in L~h } holds
  lower_bound X = inf (proj1 || N-most L~h);

theorem :: JORDAN5D:29
  for X being Subset of REAL st
    X = { q`1 : q`2 = N-bound L~h & q in L~h } holds
  upper_bound X = sup (proj1 || N-most L~h);

theorem :: JORDAN5D:30
  for X being Subset of REAL st X = { q`2 : q in L~g } holds
    lower_bound X = inf (proj2 || L~g);

theorem :: JORDAN5D:31
  for X being Subset of REAL st X = { q`1 : q in L~g } holds
    upper_bound X = sup (proj1 || L~g);

theorem :: JORDAN5D:32
  for X being Subset of REAL st X = { q`2 : q in L~g } holds
    upper_bound X = sup (proj2 || L~g);

theorem :: JORDAN5D:33
  p in L~h & 1 <= I & I <= width GoB h implies (GoB h)*(1,I)`1 <= p`1;

theorem :: JORDAN5D:34
  p in L~h & 1 <= I & I <= width GoB h implies p`1 <= (GoB h)*(len GoB h,I)`1;

theorem :: JORDAN5D:35
  p in L~h & 1 <= I & I <= len GoB h implies (GoB h)*(I,1)`2 <= p`2;

theorem :: JORDAN5D:36
  p in L~h & 1 <= I & I <= len GoB h implies p`2 <= (GoB h)*(I,width GoB h)`2;

theorem :: JORDAN5D:37
  1 <= i & i <= len GoB h & 1 <= j & j <= width GoB h implies
    ex q st q`1 = (GoB h)*(i,j)`1 & q in L~h;

theorem :: JORDAN5D:38
  1 <= i & i <= len GoB h & 1 <= j & j <= width GoB h implies
    ex q st q`2 = (GoB h)*(i,j)`2 & q in L~h;

theorem :: JORDAN5D:39
  W-bound L~h = (GoB h)*(1,1)`1;

theorem :: JORDAN5D:40
  S-bound L~h = (GoB h)*(1,1)`2;

theorem :: JORDAN5D:41
  E-bound L~h = (GoB h)*(len GoB h,1)`1;

theorem :: JORDAN5D:42
  N-bound L~h = (GoB h)*(1,width GoB h)`2;

theorem :: JORDAN5D:43
  for Y being non empty finite Subset of NAT st
    1 <= i & i <= len f & 1 <= I & I <= len GoB f &
      Y = { j : [I,j] in Indices GoB f & ex k st k in dom f &
  f/.k = (GoB f)*(I,j) } & (f/.i)`1 = ((GoB f)*(I,1))`1 & i1 = min Y holds
    (GoB f)*(I,i1)`2 <= (f/.i)`2;

theorem :: JORDAN5D:44
  for Y being non empty finite Subset of NAT st
    1 <= i & i <= len h & 1 <= I & I <= width GoB h &
      Y = { j : [j,I] in Indices GoB h & ex k st k in dom h &
  h/.k = (GoB h)*(j,I) } & (h/.i)`2 = ((GoB h)*
(1,I))`2 & i1 = min Y holds
    (GoB h)*(i1,I)`1 <= (h/.i)`1;

theorem :: JORDAN5D:45
  for Y being non empty finite Subset of NAT st
    1 <= i & i <= len h & 1 <= I & I <= width GoB h &
      Y = { j : [j,I] in Indices GoB h & ex k st k in dom h &
  h/.k = (GoB h)*(j,I) } & (h/.i)`2 = ((GoB h)*
(1,I))`2 & i1 = max Y holds
    (GoB h)*(i1,I)`1 >= (h/.i)`1;

theorem :: JORDAN5D:46
  for Y being non empty finite Subset of NAT st
    1 <= i & i <= len f & 1 <= I & I <= len GoB f &
      Y = { j : [I,j] in Indices GoB f & ex k st k in dom f &
  f/.k = (GoB f)*(I,j) } & (f/.i)`1 = ((GoB f)*
(I,1))`1 & i1 = max Y holds
    (GoB f)*(I,i1)`2 >= (f/.i)`2;

begin :: Coordinates of the special circular sequences bounding boxes

definition let g be non constant standard special_circular_sequence;
  func i_s_w g -> Nat means
:: JORDAN5D:def 1
  [1,it] in Indices GoB g & (GoB g)*(1,it) = W-min L~g;

  func i_n_w g -> Nat means
:: JORDAN5D:def 2
  [1,it] in Indices GoB g & (GoB g)*(1,it) = W-max L~g;

  func i_s_e g -> Nat means
:: JORDAN5D:def 3
  [len GoB g,it] in Indices GoB g & (GoB g)*(len GoB g,it) = E-min L~g;

  func i_n_e g -> Nat means
:: JORDAN5D:def 4
  [len GoB g,it] in Indices GoB g & (GoB g)*(len GoB g,it) = E-max L~g;

  func i_w_s g -> Nat means
:: JORDAN5D:def 5
  [it, 1] in Indices GoB g & (GoB g)*(it,1) = S-min L~g;

  func i_e_s g -> Nat means
:: JORDAN5D:def 6
  [it, 1] in Indices GoB g & (GoB g)*(it,1) = S-max L~g;

  func i_w_n g -> Nat means
:: JORDAN5D:def 7
  [it, width GoB g] in Indices GoB g & (GoB g)*(it,width GoB g) = N-min L~g;

  func i_e_n g -> Nat means
:: JORDAN5D:def 8
  [it, width GoB g] in Indices GoB g & (GoB g)*(it,width GoB g) = N-max L~g;
end;

theorem :: JORDAN5D:47
    1 <= i_w_n h & i_w_n h <= len GoB h &
   1 <= i_e_n h & i_e_n h <= len GoB h &
    1 <= i_w_s h & i_w_s h <= len GoB h &
     1 <= i_e_s h & i_e_s h <= len GoB h;

theorem :: JORDAN5D:48
    1 <= i_n_e h & i_n_e h <= width GoB h &
   1 <= i_s_e h & i_s_e h <= width GoB h &
    1 <= i_n_w h & i_n_w h <= width GoB h &
     1 <= i_s_w h & i_s_w h <= width GoB h;

definition let g be non constant standard special_circular_sequence;
  func n_s_w g -> Nat means
:: JORDAN5D:def 9
  1 <= it & it+1 <= len g & g.it = W-min L~g;

  func n_n_w g -> Nat means
:: JORDAN5D:def 10
  1 <= it & it+1 <= len g & g.it = W-max L~g;

  func n_s_e g -> Nat means
:: JORDAN5D:def 11
  1 <= it & it+1 <= len g & g.it = E-min L~g;

  func n_n_e g -> Nat means
:: JORDAN5D:def 12
  1 <= it & it+1 <= len g & g.it = E-max L~g;

  func n_w_s g -> Nat means
:: JORDAN5D:def 13
  1 <= it & it+1 <= len g & g.it = S-min L~g;

  func n_e_s g -> Nat means
:: JORDAN5D:def 14
  1 <= it & it+1 <= len g & g.it = S-max L~g;

  func n_w_n g -> Nat means
:: JORDAN5D:def 15
  1 <= it & it+1 <= len g & g.it = N-min L~g;

  func n_e_n g -> Nat means
:: JORDAN5D:def 16
  1 <= it & it+1 <= len g & g.it = N-max L~g;
end;

theorem :: JORDAN5D:49
    n_w_n h <> n_w_s h;

theorem :: JORDAN5D:50
    n_s_w h <> n_s_e h;

theorem :: JORDAN5D:51
    n_e_n h <> n_e_s h;

theorem :: JORDAN5D:52
    n_n_w h <> n_n_e h;