:: Gauges and Cages :: by Artur Korni{\l}owicz, Robert Milewski, Adam Naumowicz and :: Andrzej Trybulec :: :: Received September 12, 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, SPPOL_1, RELAT_2, GOBOARD1, PRE_TOPC, RELAT_1, ARYTM_3, INT_1, CARD_1, FINSEQ_1, ABIAN, ARYTM_1, TOPREAL2, FUNCT_1, GOBOARD5, TOPREAL1, PSCOMP_1, MCART_1, RLTOPSP1, JORDAN2C, JORDAN6, TARSKI, XXREAL_1, XXREAL_0, REAL_1, TREES_1, MATRIX_1, PARTFUN1, TOPS_1, COMPLEX1, JORDAN8, NEWTON, CONNSP_1, JORDAN9, GOBOARD9, JORDAN1A, CONVEX1, XXREAL_2, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, STRUCT_0, FINSEQ_1, NEWTON, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, GOBOARD1, MATRIX_0, RCOMP_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, SPPOL_1, ABIAN, GOBOARD5, GOBOARD9, JORDAN6, JORDAN8, JORDAN9, JORDAN2C; constructors REAL_1, SQUARE_1, NAT_D, RCOMP_1, NEWTON, ABIAN, TOPS_1, CONNSP_1, MONOID_0, PSCOMP_1, GOBOARD9, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, RELSET_1, CONVEX1; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, STRUCT_0, MONOID_0, EUCLID, JORDAN1, PSCOMP_1, SPRECT_1, SPRECT_2, SPRECT_3, JORDAN2C, TOPREAL6, JORDAN8, JORDAN10, FUNCT_1, NEWTON, INT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve i, i1, i2, j, j1, j2, k, m, n, t for Nat, D for non empty Subset of TOP-REAL 2, E for compact non vertical non horizontal Subset of TOP-REAL 2, C for compact connected non vertical non horizontal Subset of TOP-REAL 2, G for Go-board, p, q, x for Point of TOP-REAL 2, r, s for Real; definition let f be FinSequence; func Center f -> Nat equals :: JORDAN1A:def 1 len f div 2 + 1; end; theorem :: JORDAN1A:1 for f being FinSequence st len f is odd holds len f = 2 * Center f - 1; theorem :: JORDAN1A:2 for f being FinSequence st len f is even holds len f = 2 * Center f - 2; begin :: Some subsets of the plane registration cluster compact non vertical non horizontal being_simple_closed_curve non empty for Subset of TOP-REAL 2; end; theorem :: JORDAN1A:3 p in N-most D implies p`2 = N-bound D; theorem :: JORDAN1A:4 p in E-most D implies p`1 = E-bound D; theorem :: JORDAN1A:5 p in S-most D implies p`2 = S-bound D; theorem :: JORDAN1A:6 p in W-most D implies p`1 = W-bound D; theorem :: JORDAN1A:7 for D being Subset of TOP-REAL 2 holds BDD D misses D; theorem :: JORDAN1A:8 p in Vertical_Line(p`1); theorem :: JORDAN1A:9 |[r,s]| in Vertical_Line r; theorem :: JORDAN1A:10 for A being Subset of TOP-REAL 2 st A c= Vertical_Line s holds A is vertical; theorem :: JORDAN1A:11 p`1 = q`1 & r in [. proj2.p,proj2.q .] implies |[p`1,r]| in LSeg(p,q); theorem :: JORDAN1A:12 p`2 = q`2 & r in [. proj1.p,proj1.q .] implies |[r,p`2]| in LSeg(p,q); theorem :: JORDAN1A:13 p in Vertical_Line s & q in Vertical_Line s implies LSeg(p,q) c= Vertical_Line s; theorem :: JORDAN1A:14 :: Uogolnic i przenisc !!! for A,B being Subset of TOP-REAL 2 st A meets B holds proj2.:A meets proj2.:B ; theorem :: JORDAN1A:15 for A,B being Subset of TOP-REAL 2 st A misses B & A c= Vertical_Line s & B c= Vertical_Line s holds proj2.:A misses proj2.:B; begin :: Goboards theorem :: JORDAN1A:16 1 <= i & i <= len G & 1 <= j & j <= width G implies G*(i,j) in LSeg(G* (i,1),G*(i,width G)); theorem :: JORDAN1A:17 1 <= i & i <= len G & 1 <= j & j <= width G implies G*(i,j) in LSeg(G* (1,j),G*(len G,j)); theorem :: JORDAN1A:18 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 <= i2 & i2 <= len G implies G*(i1,j1)`1 <= G*(i2,j2)`1; theorem :: JORDAN1A:19 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= j2 & j2 <= width G implies G*(i1,j1)`2 <= G*(i2,j2)`2; theorem :: JORDAN1A:20 for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds G*(t,width G)`2 >= N-bound L~f; theorem :: JORDAN1A:21 for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds G*(1,t)`1 <= W-bound L~f; theorem :: JORDAN1A:22 for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds G*(t,1)`2 <= S-bound L~f; theorem :: JORDAN1A:23 for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds G*(len G,t)`1 >= E-bound L~f; theorem :: JORDAN1A:24 i<=len G & j<=width G implies cell(G,i,j) is non empty; theorem :: JORDAN1A:25 i<=len G & j<=width G implies cell(G,i,j) is connected; theorem :: JORDAN1A:26 i <= len G implies cell(G,i,0) is not bounded; theorem :: JORDAN1A:27 i <= len G implies cell(G,i,width G) is not bounded; begin :: Gauges theorem :: JORDAN1A:28 width Gauge(D,n) = 2|^n + 3; theorem :: JORDAN1A:29 i < j implies len Gauge(D,i) < len Gauge(D,j); theorem :: JORDAN1A:30 i <= j implies len Gauge(D,i) <= len Gauge(D,j); theorem :: JORDAN1A:31 m <= n & 1 < i & i < len Gauge(D,m) implies 1 < 2|^(n-'m)*(i-2)+ 2 & 2|^(n-'m)*(i-2)+2 < len Gauge(D,n); theorem :: JORDAN1A:32 m <= n & 1 < i & i < width Gauge(D,m) implies 1 < 2|^(n-'m)*(i-2 )+2 & 2|^(n-'m)*(i-2)+2 < width Gauge(D,n); theorem :: JORDAN1A:33 m <= n & 1 < i & i < len Gauge(D,m) & 1 < j & j < width Gauge(D, m) implies for i1,j1 being Nat st i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^( n-'m)*(j-2)+2 holds Gauge(D,m)*(i,j) = Gauge(D,n)*(i1,j1); theorem :: JORDAN1A:34 m <= n & 1 < i & i+1 < len Gauge(D,m) implies 1 < 2|^(n-'m)*(i-1 )+2 & 2|^(n-'m)*(i-1)+2 <= len Gauge(D,n); theorem :: JORDAN1A:35 m <= n & 1 < i & i+1 < width Gauge(D,m) implies 1 < 2|^(n-'m)*(i -1)+2 & 2|^(n-'m)*(i-1)+2 <= width Gauge(D,n); theorem :: JORDAN1A:36 1 <= i & i <= len Gauge (D,n) & 1 <= j & j <= len Gauge (D,m) & (n > 0 & m > 0 or n = 0 & m = 0) implies Gauge(D,n)*(Center Gauge(D,n), i)`1 = Gauge(D,m)*(Center Gauge(D,m), j)`1; theorem :: JORDAN1A:37 1 <= i & i <= len Gauge (D,n) & 1 <= j & j <= len Gauge (D,m) & (n > 0 & m > 0 or n = 0 & m = 0) implies Gauge(D,n)*(i, Center Gauge(D,n))`2 = Gauge(D ,m)*(j, Center Gauge(D,m))`2; theorem :: JORDAN1A:38 1 <= i & i <= len Gauge(C,1) implies Gauge(C,1)*(Center Gauge(C,1),i) `1 = (W-bound C + E-bound C) / 2; theorem :: JORDAN1A:39 1 <= i & i <= len Gauge(C,1) implies Gauge(C,1)*(i,Center Gauge(C,1)) `2 = (S-bound C + N-bound C) / 2; theorem :: JORDAN1A:40 1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n implies Gauge(E,n)*(i,len Gauge(E,n))`2 <= Gauge(E,m)*(j,len Gauge(E,m))`2 ; theorem :: JORDAN1A:41 1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n implies Gauge(E,n)*(len Gauge(E,n),i)`1 <= Gauge(E,m)*(len Gauge(E,m),j)`1; theorem :: JORDAN1A:42 1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n implies Gauge(E,m)*(1,j)`1 <= Gauge(E,n)*(1,i)`1; theorem :: JORDAN1A:43 1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n implies Gauge(E,m)*(j,1)`2 <= Gauge(E,n)*(i,1)`2; theorem :: JORDAN1A:44 1 <= m & m <= n implies LSeg(Gauge(E,n)*(Center Gauge(E,n),1), Gauge(E ,n)*(Center Gauge(E,n),len Gauge(E,n))) c= LSeg(Gauge(E,m)*(Center Gauge(E,m),1 ), Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m))); theorem :: JORDAN1A:45 1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies LSeg(Gauge(E, n)*(Center Gauge(E,n),1), Gauge(E,n)*(Center Gauge(E,n),j)) c= LSeg(Gauge(E,m)* (Center Gauge(E,m),1), Gauge(E,n)*(Center Gauge(E,n),j)); theorem :: JORDAN1A:46 1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies LSeg(Gauge(E, m)*(Center Gauge(E,m),1), Gauge(E,n)*(Center Gauge(E,n),j)) c= LSeg(Gauge(E,m)* (Center Gauge(E,m),1), Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m))); theorem :: JORDAN1A:47 m <= n & 1 < i & i+1 < len Gauge(E,m) & 1 < j & j+1 < width Gauge(E,m) implies for i1,j1 being Nat st 2|^(n-'m)*(i-2)+2 <= i1 & i1 < 2|^(n-'m)*(i-1)+2 & 2|^(n-'m)*(j-2)+2 <= j1 & j1 < 2|^(n-'m)*(j-1)+2 holds cell(Gauge(E,n),i1,j1) c= cell(Gauge(E,m),i,j); theorem :: JORDAN1A:48 m <= n & 3 <= i & i < len Gauge(E,m) & 1 < j & j+1 < width Gauge(E,m) implies for i1,j1 being Nat st i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^(n-' m)*(j-2)+2 holds cell(Gauge(E,n),i1-'1,j1) c= cell(Gauge(E,m),i-'1,j); theorem :: JORDAN1A:49 for C being compact non vertical non horizontal Subset of TOP-REAL 2 holds i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) c= UBD C; theorem :: JORDAN1A:50 for C being compact non vertical non horizontal Subset of TOP-REAL 2 holds i <= len Gauge(E,n) implies cell(Gauge(E,n),i,width Gauge(E,n)) c= UBD E; begin :: Cages theorem :: JORDAN1A:51 p in C implies north_halfline p meets L~Cage(C,n); theorem :: JORDAN1A:52 p in C implies east_halfline p meets L~Cage(C,n); theorem :: JORDAN1A:53 p in C implies south_halfline p meets L~Cage(C,n); theorem :: JORDAN1A:54 p in C implies west_halfline p meets L~Cage(C,n); theorem :: JORDAN1A:55 ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width ( Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(1,t); theorem :: JORDAN1A:56 ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= len (Gauge( C,n)) & Cage(C,n)/.k = Gauge(C,n)*(t,1); theorem :: JORDAN1A:57 ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width ( Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(len(Gauge(C,n)),t); theorem :: JORDAN1A:58 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(t,width Gauge(C,n)) implies Cage(C,n)/.k in N-most L~Cage(C,n); theorem :: JORDAN1A:59 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(1,t) implies Cage(C,n)/.k in W-most L~Cage(C,n); theorem :: JORDAN1A:60 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(t,1) implies Cage(C,n)/.k in S-most L~Cage(C,n); theorem :: JORDAN1A:61 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(len Gauge(C,n),t) implies Cage(C,n)/.k in E-most L~ Cage(C,n); theorem :: JORDAN1A:62 W-bound L~Cage(C,n) = W-bound C - (E-bound C - W-bound C)/(2|^n); theorem :: JORDAN1A:63 S-bound L~Cage(C,n) = S-bound C - (N-bound C - S-bound C)/(2|^n); theorem :: JORDAN1A:64 E-bound L~Cage(C,n) = E-bound C + (E-bound C - W-bound C)/(2|^n); theorem :: JORDAN1A:65 N-bound L~Cage(C,n) + S-bound L~Cage(C,n) = N-bound L~Cage(C,m) + S-bound L~Cage(C,m); theorem :: JORDAN1A:66 E-bound L~Cage(C,n) + W-bound L~Cage(C,n) = E-bound L~Cage(C,m) + W-bound L~Cage(C,m); theorem :: JORDAN1A:67 i < j implies E-bound L~Cage(C,j) < E-bound L~Cage(C,i); theorem :: JORDAN1A:68 i < j implies W-bound L~Cage(C,i) < W-bound L~Cage(C,j); theorem :: JORDAN1A:69 i < j implies S-bound L~Cage(C,i) < S-bound L~Cage(C,j); theorem :: JORDAN1A:70 1 <= i & i <= len Gauge(C,n) implies N-bound L~Cage(C,n) = Gauge(C,n)* (i,len Gauge(C,n))`2; theorem :: JORDAN1A:71 1 <= i & i <= len Gauge(C,n) implies E-bound L~Cage(C,n) = Gauge(C,n)* (len Gauge(C,n),i)`1; theorem :: JORDAN1A:72 1 <= i & i <= len Gauge(C,n) implies S-bound L~Cage(C,n) = Gauge(C,n)* (i,1)`2; theorem :: JORDAN1A:73 1 <= i & i <= len Gauge(C,n) implies W-bound L~Cage(C,n) = Gauge(C,n)* (1,i)`1; theorem :: JORDAN1A:74 x in C & p in north_halfline x /\ L~Cage(C,n) implies p`2 > x`2; theorem :: JORDAN1A:75 x in C & p in east_halfline x /\ L~Cage(C,n) implies p`1 > x`1; theorem :: JORDAN1A:76 x in C & p in south_halfline x /\ L~Cage(C,n) implies p`2 < x`2; theorem :: JORDAN1A:77 x in C & p in west_halfline x /\ L~Cage(C,n) implies p`1 < x`1; theorem :: JORDAN1A:78 x in N-most C & p in north_halfline x & 1 <= i & i < len Cage(C, n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is horizontal; theorem :: JORDAN1A:79 x in E-most C & p in east_halfline x & 1 <= i & i < len Cage(C, n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is vertical; theorem :: JORDAN1A:80 x in S-most C & p in south_halfline x & 1 <= i & i < len Cage(C ,n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is horizontal; theorem :: JORDAN1A:81 x in W-most C & p in west_halfline x & 1 <= i & i < len Cage(C, n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is vertical; theorem :: JORDAN1A:82 x in N-most C & p in north_halfline x /\ L~Cage(C,n) implies p `2 = N-bound L~Cage(C,n); theorem :: JORDAN1A:83 x in E-most C & p in east_halfline x /\ L~Cage(C,n) implies p`1 = E-bound L~Cage(C,n); theorem :: JORDAN1A:84 x in S-most C & p in south_halfline x /\ L~Cage(C,n) implies p `2 = S-bound L~Cage(C,n); theorem :: JORDAN1A:85 x in W-most C & p in west_halfline x /\ L~Cage(C,n) implies p`1 = W-bound L~Cage(C,n); theorem :: JORDAN1A:86 x in N-most C implies ex p being Point of TOP-REAL 2 st north_halfline x /\ L~Cage(C,n) = {p}; theorem :: JORDAN1A:87 x in E-most C implies ex p being Point of TOP-REAL 2 st east_halfline x /\ L~Cage(C,n) = {p}; theorem :: JORDAN1A:88 x in S-most C implies ex p being Point of TOP-REAL 2 st south_halfline x /\ L~Cage(C,n) = {p}; theorem :: JORDAN1A:89 x in W-most C implies ex p being Point of TOP-REAL 2 st west_halfline x /\ L~Cage(C,n) = {p};