:: Cages, external approximation of Jordan's curve :: by Czes{\l}aw Byli\'nski and Mariusz \.Zynel :: :: Received June 22, 1999 :: Copyright (c) 1999-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, FINSEQ_1, XXREAL_0, ARYTM_1, ARYTM_3, PRE_TOPC, RELAT_2, CONNSP_1, TARSKI, RELAT_1, FINSEQ_5, PARTFUN1, GOBOARD1, EUCLID, REAL_1, MATRIX_1, COMPLEX1, GOBRD13, FUNCT_1, TOPREAL1, RFINSEQ, RLTOPSP1, GOBOARD5, TOPS_1, TREES_1, SPPOL_1, MCART_1, CARD_1, GOBOARD9, RCOMP_1, NAT_1, JORDAN8, PSCOMP_1, NEWTON, SPRECT_2, ORDINAL4, STRUCT_0, PCOMPS_1, METRIC_1, JORDAN9, CONVEX1; notations TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, COMPLEX1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, NEWTON, RFINSEQ, STRUCT_0, XXREAL_0, MATRIX_0, MATRIX_1, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, SPPOL_1, PSCOMP_1, SPRECT_2, GOBOARD9, JORDAN8, GOBRD13; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, COMPTS_1, SPPOL_1, PSCOMP_1, GOBOARD9, SPRECT_2, JORDAN8, GOBRD13, RELSET_1, FUNCSDOM, PCOMPS_1, CONVEX1, MATRIX_1; registrations RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, SPPOL_2, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN8, NEWTON, FINSET_1, SPPOL_1, JORDAN1, MATRIX_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Generalities reserve i,j,k,n for Nat, D for non empty set, f, g for FinSequence of D; theorem :: JORDAN9:1 for T being non empty TopSpace for B,C1,C2,D being Subset of T st B is connected & C1 is_a_component_of D & C2 is_a_component_of D & B meets C1 & B meets C2 & B c= D holds C1 = C2; theorem :: JORDAN9:2 (for n holds f|n = g|n) implies f = g; theorem :: JORDAN9:3 n in dom f implies ex k st k in dom Rev f & n+k = len f+1 & f/.n = (Rev f)/.k ; theorem :: JORDAN9:4 n in dom Rev f implies ex k st k in dom f & n+k = len f+1 & (Rev f)/.n = f/.k ; begin :: Go-board preliminaries reserve G for Go-board, f, g for FinSequence of TOP-REAL 2, p for Point of TOP-REAL 2, r, s for Real, x for set; theorem :: JORDAN9:5 for D being non empty set for G being Matrix of D for f being FinSequence of D holds f is_sequence_on G iff Rev f is_sequence_on G; theorem :: JORDAN9:6 for G being Matrix of TOP-REAL 2 for f being FinSequence of TOP-REAL 2 st f is_sequence_on G for k being Nat st 1 <= k & k <= len f holds f/.k in Values G; theorem :: JORDAN9:7 n <= len f & x in L~(f/^n) implies ex i being Nat st n+1 <= i & i+1 <= len f & x in LSeg(f,i); theorem :: JORDAN9:8 f is_sequence_on G implies for k being Nat st 1 <= k & k+1 <= len f holds f/.k in left_cell(f,k,G) & f/.k in right_cell(f,k,G); theorem :: JORDAN9:9 f is_sequence_on G implies for k being Nat st 1 <= k & k+1 <= len f holds Int left_cell(f,k,G) <> {} & Int right_cell(f,k,G) <> {}; theorem :: JORDAN9:10 f is_sequence_on G implies for k being Nat st 1 <= k & k+1 <= len f holds Int left_cell(f,k,G) is convex & Int right_cell(f,k,G) is convex; theorem :: JORDAN9:11 f is_sequence_on G & 1 <= k & k+1 <= len f implies Cl Int left_cell(f,k,G) = left_cell(f,k,G) & Cl Int right_cell(f,k,G) = right_cell(f,k ,G); theorem :: JORDAN9:12 f is_sequence_on G & LSeg(f,k) is horizontal implies ex j st 1 <= j & j <= width G & for p st p in LSeg(f,k) holds p`2 = G*(1,j)`2; theorem :: JORDAN9:13 f is_sequence_on G & LSeg(f,k) is vertical implies ex i st 1 <= i & i <= len G & for p st p in LSeg(f,k) holds p`1 = G*(i,1)`1; theorem :: JORDAN9:14 f is_sequence_on G & f is special implies for i,j being Nat st i <= len G & j <= width G holds Int cell(G,i,j) misses L~f; theorem :: JORDAN9:15 f is_sequence_on G & f is special implies for k being Nat st 1 <= k & k+1 <= len f holds Int left_cell(f,k,G) misses L~f & Int right_cell(f,k,G) misses L~f; theorem :: JORDAN9:16 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies G*(i,j) `1 = G*(i,j+1)`1 & G*(i,j)`2 = G*(i+1,j)`2 & G*(i+1,j+1)`1 = G*(i+1,j)`1 & G*(i +1,j+1)`2 = G*(i,j+1)`2; theorem :: JORDAN9:17 for i,j being Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G holds p in cell(G,i,j) iff G*(i,j)`1 <= p`1 & p`1 <= G*(i+1,j)`1 & G*(i,j)`2 <= p`2 & p`2 <= G*(i,j+1)`2; theorem :: JORDAN9:18 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies cell(G,i,j) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 & G*(i,j)`2 <= s & s <= G*(i,j+1) `2 }; theorem :: JORDAN9:19 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G & p in Values G & p in cell(G,i,j) implies p = G*(i,j) or p = G*(i,j+1) or p = G*(i+1,j+1) or p = G*(i+1,j); theorem :: JORDAN9:20 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies G*(i,j) in cell(G,i,j) & G*(i,j+1) in cell(G,i,j) & G*(i+1,j+1) in cell(G,i,j) & G*(i+1 ,j) in cell(G,i,j); theorem :: JORDAN9:21 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G & p in Values G & p in cell(G,i,j) implies p is_extremal_in cell(G,i,j); theorem :: JORDAN9:22 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f implies ex i,j being Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G & LSeg( f,k) c= cell(G,i,j); theorem :: JORDAN9:23 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f & p in Values G & p in LSeg(f,k) implies p = f/.k or p = f/.(k+1); theorem :: JORDAN9:24 [i,j] in Indices G & 1 <= k & k <= width G implies G*(i,j)`1 <= G* ( len G,k)`1; theorem :: JORDAN9:25 [i,j] in Indices G & 1 <= k & k <= len G implies G*(i,j)`2 <= G* (k, width G)`2; theorem :: JORDAN9:26 f is_sequence_on G & f is special & L~g c= L~f & 1 <= k & k+1 <= len f implies for A being Subset of TOP-REAL 2 st A = right_cell(f,k,G)\L~g or A = left_cell(f,k,G)\L~g holds A is connected; theorem :: JORDAN9:27 for f being non constant standard special_circular_sequence st f is_sequence_on G for k st 1 <= k & k+1 <= len f holds right_cell(f,k,G)\L~f c= RightComp f & left_cell(f,k,G)\L~f c= LeftComp f; begin :: Cages reserve C for compact non vertical non horizontal non empty Subset of TOP-REAL 2, l, m, i1, i2, j1, j2 for Nat; theorem :: JORDAN9:28 for n being Nat ex i st 1 <= i & i+1 <= len Gauge(C,n) & N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) & N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1); theorem :: JORDAN9:29 for n, i1, i2 being Nat holds 1 <= i1 & i1+1 <= len Gauge(C,n) & N-min C in cell(Gauge(C,n),i1,width Gauge(C,n)-'1) & N-min C <> Gauge(C,n)*(i1, width Gauge(C,n)-'1) & 1 <= i2 & i2+1 <= len Gauge(C,n) & N-min C in cell(Gauge (C,n),i2,width Gauge(C,n)-'1) & N-min C <> Gauge(C,n)*(i2,width Gauge(C,n)-'1) implies i1 = i2; theorem :: JORDAN9:30 for n being Nat for f being standard non constant special_circular_sequence st f is_sequence_on Gauge(C,n) & (for k being Nat st 1 <= k & k +1 <= len f holds left_cell(f,k,Gauge(C,n)) misses C & right_cell(f,k,Gauge(C,n )) meets C) & (ex i being Nat st 1 <= i & i+1 <= len Gauge(C,n) & f/.1 = Gauge(C,n)*(i, width Gauge(C,n)) & f/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) & N-min C in cell( Gauge(C,n),i,width Gauge(C,n)-'1) & N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-' 1)) holds N-min L~f = f/.1; definition let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2; let n be Nat; assume C is connected; func Cage(C,n) -> clockwise_oriented standard non constant special_circular_sequence means :: JORDAN9:def 1 it is_sequence_on Gauge(C,n) & (ex i being Nat st 1 <= i & i+1 <= len Gauge(C,n) & it/.1 = Gauge(C,n)*(i,width Gauge(C,n)) & it/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) & N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) & N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1)) & for k being Nat st 1 <= k & k+2 <= len it holds (front_left_cell(it,k,Gauge(C,n)) misses C & front_right_cell(it,k,Gauge(C,n)) misses C implies it turns_right k,Gauge(C,n)) & (front_left_cell(it,k,Gauge(C,n)) misses C & front_right_cell(it,k,Gauge(C,n) ) meets C implies it goes_straight k,Gauge(C,n)) & (front_left_cell(it,k,Gauge( C,n)) meets C implies it turns_left k,Gauge(C,n)); end; theorem :: JORDAN9:31 C is connected implies for n,k being Nat st 1 <= k & k+1 <= len Cage(C,n) holds left_cell (Cage(C,n),k,Gauge(C,n)) misses C & right_cell(Cage(C,n),k,Gauge(C,n)) meets C; theorem :: JORDAN9:32 C is connected implies for n being Nat holds N-min L~Cage(C,n) = (Cage(C,n))/.1;