:: Bounding Boxes for Special Sequences in ${\calE}^2$ :: by Yatsuka Nakamura and Adam Grabowski :: :: Received June 8, 1998 :: Copyright (c) 1998-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, PRE_TOPC, EUCLID, REAL_1, FUNCT_1, GOBOARD5, FINSEQ_1, XBOOLE_0, SUBSET_1, XXREAL_0, PARTFUN1, RLTOPSP1, ARYTM_1, ARYTM_3, INT_1, RELAT_1, JORDAN4, GOBOARD2, TREES_1, MCART_1, GOBOARD1, MATRIX_1, NAT_1, ZFMISC_1, PSCOMP_1, TOPREAL1, STRUCT_0, TARSKI, SEQ_4, FINSET_1, SPPOL_1, XXREAL_2, CARD_1, JORDAN5D; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MCART_1, XCMPLX_0, REAL_1, NAT_1, NAT_D, RELAT_1, FINSEQ_1, FUNCT_1, PARTFUN1, FINSET_1, MATRIX_0, XXREAL_2, STRUCT_0, TOPREAL1, SPPOL_1, GOBOARD1, GOBOARD2, GOBOARD5, PRE_TOPC, RLTOPSP1, EUCLID, JORDAN4, PSCOMP_1, XXREAL_0, SEQ_4; constructors REAL_1, NAT_D, BINARITH, COMPTS_1, GOBOARD2, SPPOL_1, PSCOMP_1, JORDAN4, GOBOARD1, SEQ_4, RELSET_1, RVSUM_1; registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, SPRECT_1, VALUED_0, XXREAL_2, FUNCT_1, SEQ_4; 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; theorem :: JORDAN5D:1 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:2 3 <= i implies i mod (i-'1) = 1; theorem :: JORDAN5D:3 p in rng h implies ex i be Nat st 1 <= i & i+1 <= len h & h.i = p; theorem :: JORDAN5D:4 for g being FinSequence of REAL st r in rng g holds Incr g.1 <= r & r <= Incr g.len Incr g; theorem :: JORDAN5D:5 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:6 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:7 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:8 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:9 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:10 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:11 1 <= i & i <= len h implies S-bound L~h <= (h/.i)`2 & (h/.i)`2 <= N-bound L~h ; theorem :: JORDAN5D:12 1 <= i & i <= len h implies W-bound L~h <= (h/.i)`1 & (h/.i)`1 <= E-bound L~h ; theorem :: JORDAN5D:13 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:14 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:15 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:16 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:17 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:18 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:19 for X being Subset of REAL st X = { q`2 : q`1 = W-bound L~h & q in L~h } holds lower_bound X = lower_bound (proj2 | W-most L~h); theorem :: JORDAN5D:20 for X being Subset of REAL st X = { q`2 : q`1 = W-bound L~h & q in L~h } holds upper_bound X = upper_bound (proj2 | W-most L~h); theorem :: JORDAN5D:21 for X being Subset of REAL st X = { q`2 : q`1 = E-bound L~h & q in L~h } holds lower_bound X = lower_bound (proj2 | E-most L~h); theorem :: JORDAN5D:22 for X being Subset of REAL st X = { q`2 : q`1 = E-bound L~h & q in L~h } holds upper_bound X = upper_bound (proj2 | E-most L~h); theorem :: JORDAN5D:23 for X being Subset of REAL st X = { q`1 : q in L~g } holds lower_bound X = lower_bound (proj1 | L~g); theorem :: JORDAN5D:24 for X being Subset of REAL st X = { q`1 : q`2 = S-bound L~h & q in L~h } holds lower_bound X = lower_bound (proj1 | S-most L~h); theorem :: JORDAN5D:25 for X being Subset of REAL st X = { q`1 : q`2 = S-bound L~h & q in L~h } holds upper_bound X = upper_bound (proj1 | S-most L~h); theorem :: JORDAN5D:26 for X being Subset of REAL st X = { q`1 : q`2 = N-bound L~h & q in L~h } holds lower_bound X = lower_bound (proj1 | N-most L~h); theorem :: JORDAN5D:27 for X being Subset of REAL st X = { q`1 : q`2 = N-bound L~h & q in L~h } holds upper_bound X = upper_bound (proj1 | N-most L~h); theorem :: JORDAN5D:28 for X being Subset of REAL st X = { q`2 : q in L~g } holds lower_bound X = lower_bound (proj2 | L~g); theorem :: JORDAN5D:29 for X being Subset of REAL st X = { q`1 : q in L~g } holds upper_bound X = upper_bound (proj1 | L~g); theorem :: JORDAN5D:30 for X being Subset of REAL st X = { q`2 : q in L~g } holds upper_bound X = upper_bound (proj2 | L~g); theorem :: JORDAN5D:31 p in L~h & 1 <= I & I <= width GoB h implies (GoB h)*(1,I)`1 <= p`1; theorem :: JORDAN5D:32 p in L~h & 1 <= I & I <= width GoB h implies p`1 <= (GoB h)*(len GoB h,I)`1; theorem :: JORDAN5D:33 p in L~h & 1 <= I & I <= len GoB h implies (GoB h)*(I,1)`2 <= p `2; theorem :: JORDAN5D:34 p in L~h & 1 <= I & I <= len GoB h implies p`2 <= (GoB h)*(I, width GoB h)`2; theorem :: JORDAN5D:35 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:36 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:37 W-bound L~h = (GoB h)*(1,1)`1; theorem :: JORDAN5D:38 S-bound L~h = (GoB h)*(1,1)`2; theorem :: JORDAN5D:39 E-bound L~h = (GoB h)*(len GoB h,1)`1; theorem :: JORDAN5D:40 N-bound L~h = (GoB h)*(1,width GoB h)`2; theorem :: JORDAN5D:41 for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len GoB f & Y = { j where j is Element of NAT: [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:42 for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width GoB h & Y = { j where j is Element of NAT: [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:43 for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width GoB h & Y = { j where j is Element of NAT: [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:44 for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len GoB f & Y = { j where j is Element of NAT: [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:45 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:46 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:47 n_w_n h <> n_w_s h; theorem :: JORDAN5D:48 n_s_w h <> n_s_e h; theorem :: JORDAN5D:49 n_e_n h <> n_e_s h; theorem :: JORDAN5D:50 n_n_w h <> n_n_e h;