:: Gauges and Cages. { P } art { II } :: by Artur Korni{\l}owicz and Robert Milewski :: :: Received November 6, 2000 :: Copyright (c) 2000-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, XBOOLE_0, EUCLID, RCOMP_1, RELAT_2, SPPOL_1, RELAT_1, CARD_1, ARYTM_3, INT_1, TARSKI, NEWTON, ABIAN, NAT_1, XXREAL_0, ARYTM_1, FINSEQ_1, JORDAN8, MCART_1, PSCOMP_1, TREES_1, MATRIX_1, GOBOARD5, REAL_1, SETFAM_1, JORDAN9, PRE_TOPC, TOPREAL1, RLTOPSP1, PARTFUN1, GOBOARD1, FUNCT_1, XCMPLX_0; notations TARSKI, XBOOLE_0, ENUMSET1, SETFAM_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, STRUCT_0, FINSEQ_1, NEWTON, PRE_TOPC, COMPTS_1, CONNSP_1, MATRIX_0, RLTOPSP1, EUCLID, GOBOARD1, TOPREAL1, GOBOARD5, PSCOMP_1, SPPOL_1, ABIAN, GOBRD13, JORDAN8, JORDAN9; constructors SETFAM_1, REAL_1, NAT_D, NEWTON, REALSET1, ABIAN, CONNSP_1, PSCOMP_1, JORDAN8, GOBRD13, JORDAN9, SEQ_4, RELSET_1; registrations RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, ABIAN, GRAPH_3, TOPREAL6, JORDAN8, JORDAN10, FUNCT_1, EUCLID; requirements NUMERALS, SUBSET, REAL, ARITHM; begin :: Preliminaries reserve a, b, i, k, m, n for Nat, r for Real, 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; registration let m be non zero Nat; cluster 2|^m -> even; end; registration let n be even Nat, m be non zero Nat; cluster n|^m -> even; end; theorem :: JORDAN1D:2 r <> 0 implies 1/r * r|^(i+1) = r|^i; begin :: Gauges and Cages theorem :: JORDAN1D:3 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:4 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:5 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:6 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:7 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:8 ex i being Nat st 1 <= i & i < len Cage(C,n) & N-max C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:9 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:10 ex i being Nat st 1 <= i & i < len Cage(C,n) & E-min C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:11 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:12 ex i being Nat st 1 <= i & i < len Cage(C,n) & E-max C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:13 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:14 ex i being Nat st 1 <= i & i < len Cage(C,n) & S-min C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:15 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:16 ex i being Nat st 1 <= i & i < len Cage(C,n) & S-max C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:17 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:18 ex i being Nat st 1 <= i & i < len Cage(C,n) & W-min C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:19 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:20 ex i being Nat st 1 <= i & i < len Cage(C,n) & W-max C in right_cell(Cage(C,n),i); theorem :: JORDAN1D:21 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:22 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:23 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:24 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:25 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:26 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:27 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:28 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:29 ex i being Nat st 1 <= i & i <= len Gauge(C,n) & Gauge(C,n) *(i,1) in rng Cage(C,n); theorem :: JORDAN1D:30 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:31 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:32 ex j being Nat st 1 <= j & j <= width Gauge(C,n) & Gauge(C, n)*(1,j) in rng Cage(C,n);