:: Properties of the Internal Approximation of {J}ordan's Curve :: by Robert Milewski :: :: Received June 27, 2002 :: Copyright (c) 2002-2019 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, FUNCT_1, GOBOARD5, JORDAN2C, TOPREAL1, GOBOARD9, CONNSP_1, SUBSET_1, GOBOARD1, FINSEQ_1, EUCLID, XXREAL_0, ARYTM_3, RCOMP_1, MATRIX_1, PARTFUN1, RELAT_1, ARYTM_1, PRE_TOPC, TREES_1, TOPS_1, MCART_1, REAL_1, RELAT_2, TOPREAL2, JORDAN8, JORDAN1H, JORDAN11, TARSKI, RLTOPSP1, JORDAN13, XBOOLE_0, CARD_1, GOBRD13, ORDINAL4, STRUCT_0, PSCOMP_1, SPPOL_1, NEWTON, COMPLEX1, JORDAN14, CONVEX1, XXREAL_2, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, PARTFUN1, FINSEQ_1, SEQM_3, STRUCT_0, MATRIX_0, PRE_TOPC, TOPREAL2, TOPS_1, COMPTS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, GOBRD13, JORDAN1H, JORDAN11, JORDAN13, XXREAL_0; constructors REAL_1, FINSEQ_4, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPREAL4, JORDAN1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, JORDAN1H, JORDAN11, JORDAN13, CONVEX1, RELSET_1, GOBRD13; registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, TOPREAL1, TOPREAL2, TOPREAL5, SPRECT_2, SPRECT_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD14, EUCLID, RLTOPSP1, JORDAN1, XREAL_0, NAT_1, NEWTON; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI; expansions TARSKI; theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, PSCOMP_1, FINSEQ_5, GOBOARD7, TOPREAL1, JORDAN5B, GOBOARD5, GOBOARD9, SUBSET_1, GOBRD11, SPRECT_3, GOBOARD6, TOPS_1, JORDAN8, GOBRD13, SPRECT_4, CONNSP_1, XBOOLE_0, XBOOLE_1, NEWTON, GOBRD14, TOPREAL6, INT_1, JORDAN2C, PRE_TOPC, JORDAN9, JORDAN1H, TSEP_1, GOBRD12, JORDAN1A, JORDAN1C, JORDAN11, JORDAN13, XREAL_1, XXREAL_0, CARD_1, MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3; schemes NAT_1; begin theorem Th1: for f be non constant standard special_circular_sequence holds BDD L~f = RightComp f or BDD L~f = LeftComp f proof let f be non constant standard special_circular_sequence; BDD L~f is_inside_component_of L~f by JORDAN2C:108; then BDD L~f is_a_component_of (L~f)` by JORDAN2C:def 2; hence thesis by JORDAN1H:24; end; theorem for f be non constant standard special_circular_sequence holds UBD L~f = RightComp f or UBD L~f = LeftComp f proof let f be non constant standard special_circular_sequence; UBD L~f is_outside_component_of L~f by JORDAN2C:68; then UBD L~f is_a_component_of (L~f)` by JORDAN2C:def 3; hence thesis by JORDAN1H:24; end; theorem for G be Go-board for f be FinSequence of TOP-REAL 2 for k be Nat holds 1 <= k & k+1 <= len f & f is_sequence_on G implies left_cell(f,k,G) is closed proof let G be Go-board; let f be FinSequence of TOP-REAL 2; let k be Nat; assume that A1: 1 <= k and A2: k+1 <= len f and A3: f is_sequence_on G; consider i1,j1,i2,j2 be Nat such that A4: [i1,j1] in Indices G and A5: f/.k = G*(i1,j1) and A6: [i2,j2] in Indices G and A7: f/.(k+1) = G*(i2,j2) and A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3; i1 = i2 & j1+1 = j2 & left_cell(f,k,G) = cell(G,i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k,G) = cell(G,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f ,k,G) = cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k,G) = cell(G,i1, j2) by A1,A2,A3,A4,A5,A6,A7,A8,GOBRD13:def 3; hence thesis by GOBRD11:33; end; theorem Th4: for G be Go-board for p be Point of TOP-REAL 2 for i,j be Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G holds p in Int 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 proof let G be Go-board; let p be Point of TOP-REAL 2; let i,j be Nat; assume that A1: 1 <= i and A2: i+1 <= len G and A3: 1 <= j and A4: j+1 <= width G; set Z = {|[r,s]| where r,s is Real : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1, j)`2 < s & s < G*(1,j+1)`2}; A5: j < width G by A4,NAT_1:13; i+1 >= 1 by NAT_1:11; then A6: G*(i+1,1)`1 = G*(i+1,j)`1 by A2,A3,A5,GOBOARD5:2; A7: i < len G by A2,NAT_1:13; then A8: G*(1,j)`2 = G*(i,j)`2 by A1,A3,A5,GOBOARD5:1; j+1 >= 1 by NAT_1:11; then A9: G*(1,j+1)`2 = G*(i,j+1)`2 by A1,A4,A7,GOBOARD5:1; A10: G*(i,1)`1 = G*(i,j)`1 by A1,A3,A7,A5,GOBOARD5:2; thus p in Int cell(G,i,j) implies 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 proof assume p in Int cell(G,i,j); then p in Z by A1,A3,A7,A5,GOBOARD6:26; then ex r,s be Real st p = |[r,s]| & G*(i,1)`1 < r & r < G*(i +1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2; hence thesis by A10,A6,A8,A9,EUCLID:52; end; assume that A11: G*(i,j)`1 < p`1 and A12: p`1 < G*(i+1,j)`1 and A13: G*(i,j)`2 < p`2 and A14: p`2 < G*(i,j+1)`2; p = |[p`1,p`2]| by EUCLID:53; then p in Z by A10,A6,A8,A9,A11,A12,A13,A14; hence thesis by A1,A3,A7,A5,GOBOARD6:26; end; theorem Th5: for f be non constant standard special_circular_sequence holds BDD L~f is connected proof let f be non constant standard special_circular_sequence; BDD L~f = RightComp f or BDD L~f = LeftComp f by Th1; hence thesis; end; registration let f be non constant standard special_circular_sequence; cluster BDD L~f -> connected; coherence by Th5; end; definition let C be Simple_closed_curve; let n be Nat; func SpanStart(C,n) -> Point of TOP-REAL 2 equals Gauge(C,n)*(X-SpanStart(C, n),Y-SpanStart(C,n)); coherence; end; theorem Th6: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds SpanStart(C,n) in BDD C proof let C be Simple_closed_curve; let n be Nat; A1: 1 <= X-SpanStart(C,n)-'1 by JORDAN1H:50; A2: X-SpanStart(C,n)-'1 < len Gauge(C,n) by JORDAN1H:50; assume A3: n is_sufficiently_large_for C; then A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) c= BDD C by JORDAN11:6; A5: Y-SpanStart(C,n) <= width Gauge(C,n) by A3,JORDAN11:7; 1 < Y-SpanStart(C,n) by A3,JORDAN11:7; then LSeg(Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*( X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n))) c= cell(Gauge(C,n),X-SpanStart(C,n)-'1 ,Y-SpanStart(C,n)) by A1,A2,A5,GOBOARD5:22; then A6: LSeg(Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*( X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n))) c= BDD C by A4; A7: 2 < X-SpanStart(C,n) by JORDAN1H:49; Gauge(C,n)*(X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n)) in LSeg(Gauge(C,n)* (X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*(X-SpanStart(C,n)-'1+1, Y-SpanStart(C,n))) by RLTOPSP1:68; then Gauge(C,n)*(X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n)) in BDD C by A6; hence thesis by A7,XREAL_1:235,XXREAL_0:2; end; theorem Th7: for C be Simple_closed_curve for n,k be Nat st n is_sufficiently_large_for C holds 1 <= k & k+1 <= len Span(C,n) implies right_cell(Span(C,n),k,Gauge(C,n)) misses C & left_cell(Span(C,n),k,Gauge(C,n)) meets C proof let C be Simple_closed_curve; let n,k be Nat; set G = Gauge(C,n); set f = Span(C,n); defpred P[Nat] means for m be Nat st 1 <= m & m+1 <= len(f|$1) holds right_cell(f|$1,m,G) misses C & left_cell(f|$1,m,G) meets C; A1: f|len f = f by FINSEQ_1:58; assume A2: n is_sufficiently_large_for C; then A3: f is_sequence_on G by JORDAN13:def 1; A4: f/.2 = G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) by A2,JORDAN13:def 1; A5: f/.1 = G*(X-SpanStart(C,n),Y-SpanStart(C,n)) by A2,JORDAN13:def 1; A6: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A7: for m be Nat st 1 <= m & m+1 <= len(f|k) holds right_cell(f|k,m,G) misses C & left_cell(f|k,m,G) meets C; A8: f|(k+1) is_sequence_on G by A3,GOBOARD1:22; A9: f|k is_sequence_on G by A3,GOBOARD1:22; per cases; suppose A10: k >= len f; then A11: f|(k+1) = f by FINSEQ_1:58,NAT_1:12; f|k = f by A10,FINSEQ_1:58; hence thesis by A7,A11; end; suppose A12: k < len f; let m be Nat; assume that A13: 1 <= m and A14: m+1 <= len(f|(k+1)); A15: k+1 <= len f by A12,NAT_1:13; then A16: len(f|(k+1)) = k+1 by FINSEQ_1:59; A17: len(f|k) = k by A12,FINSEQ_1:59; now per cases by NAT_1:25; suppose A18: k = 0; 1 <= m+1 by NAT_1:12; then m+1 = 0+1 by A14,A18,XXREAL_0:1; hence thesis by A13; end; suppose A19: k = 1; set j = Y-SpanStart(C,n); set i = X-SpanStart(C,n); A20: f|(k+1) = <*G*(i,j),G*(i-'1,j)*> by A5,A4,A15,A19,FINSEQ_5:81; then A21: (f|(k+1))/.1 = G*(i,j) by FINSEQ_4:17; 1+1 <= m+1 by A13,XREAL_1:6; then A22: m+1 = 1+1 by A16,A14,A19,XXREAL_0:1; A23: [i-'1,j] in Indices G by A2,JORDAN11:9; A24: [i,j] in Indices G by A2,JORDAN11:8; i-'1 <= i by NAT_D:35; then A25: i+1 <> i-'1 by NAT_1:13; A26: j <> j+1; A27: (f|(k+1))/.2 = G*(i-'1,j) by A20,FINSEQ_4:17; then right_cell(f|(k+1),m,G) = cell(G,i-'1,j) by A8,A14,A21,A24,A23 ,A22,A26,A25,GOBRD13:def 2; hence right_cell(f|(k+1),m,G) misses C by A2,JORDAN11:11; left_cell(f|(k+1),m,G) = cell(G,i-'1,j-'1) by A8,A14,A21,A27,A24,A23 ,A22,A26,A25,GOBRD13:def 3; hence left_cell(f|(k+1),m,G) meets C by A2,JORDAN11:10; end; suppose A28: k > 1; A29: len(f|k) <= len f by FINSEQ_5:16; A30: 1 <= (len(f|k))-'1 by A17,A28,NAT_D:49; A31: (len(f|k))-'1+1 = len(f|k) by A17,A28,XREAL_1:235; then A32: (len(f|k))-'1+(1+1) = (len(f|k))+1; now per cases; suppose A33: m+1 = len(f|(k+1)); left_cell(f|k,(len(f|k))-'1,G) meets C by A7,A30,A31; then A34: left_cell(f,(len(f|k))-'1,G) meets C by A3,A17,A30,A31,A29, GOBRD13:31; consider i1,j1,i2,j2 be Nat such that A35: [i1,j1] in Indices G and A36: f/.(len(f|k)-'1) = G*(i1,j1) and A37: [i2,j2] in Indices G and A38: f/.(len(f|k)) = G*(i2,j2) and i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,A12,A17,A30,A31,JORDAN8:3; 1 <= i2 by A37,MATRIX_0:32; then A39: i2-'1+1 = i2 by XREAL_1:235; A40: 1 <= j2 by A37,MATRIX_0:32; then A41: j2-'1+1 = j2 by XREAL_1:235; right_cell(f|k,(len(f|k))-'1,G) misses C by A7,A30,A31; then A42: right_cell(f,(len(f|k))-'1,G) misses C by A3,A17,A30,A31,A29, GOBRD13:31; now per cases; suppose A43: front_right_cell(f,(len(f|k))-'1,G) misses C & front_left_cell(f,(len(f|k))-'1,G) misses C; then A44: f turns_left (len(f|k))-'1,G by A2,A15,A17,A30,A32, JORDAN13:def 1; now per cases by A31,A35,A36,A37,A38,A44,GOBRD13:def 7; suppose that A45: i1 = i2 & j1+1 = j2 and A46: [i2-'1,j2] in Indices G and A47: f/.((len(f|k))-'1+2) = G*(i2-'1,j2); cell(G,i1-'1,j1+1) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A43,A45,GOBRD13:34; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A39,A45,A46,A47,GOBRD13:26; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; A48: j1+1-'1 = j1 by NAT_D:34; cell(G,i1-'1,j1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A34,A45,GOBRD13:21; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33 ,A37,A38,A39,A45,A46,A47,A48,GOBRD13:25; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A49: i1+1 = i2 & j1 = j2 and A50: [i2,j2+1] in Indices G and A51: f/.((len(f|k))-'1+2) = G*(i2,j2+1); cell(G,i2,j2) misses C by A3,A30,A31,A29,A35,A36,A37,A38 ,A43,A49,GOBRD13:36; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A50,A51,GOBRD13:22; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; A52: i1+1-'1 = i1 by NAT_D:34; cell(G,i1,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37 ,A38,A34,A49,GOBRD13:23; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33 ,A37,A38,A49,A50,A51,A52,GOBRD13:21; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A53: i1 = i2+1 & j1 = j2 and A54: [i2,j2-'1] in Indices G and A55: f/.((len(f|k))-'1+2) = G*(i2,j2-'1); cell(G,i2-'1,j2-'1) misses C by A3,A30,A31,A29,A35,A36 ,A37,A38,A43,A53,GOBRD13:38; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A41,A54,A55,GOBRD13:28; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A34,A53,GOBRD13:25; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33 ,A37,A38,A41,A54,A55,GOBRD13:27; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A56: i1 = i2 & j1 = j2+1 and A57: [i2+1,j2] in Indices G and A58: f/.((len(f|k))-'1+2) = G*(i2+1,j2); cell(G,i1,j2-'1) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A43,A56,GOBRD13:40; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A56,A57,A58,GOBRD13:24; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i1,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37 ,A38,A34,A56,GOBRD13:27; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33 ,A37,A38,A56,A57,A58,GOBRD13:23; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; end; hence thesis; end; suppose A59: front_right_cell(f,(len(f|k))-'1,G) misses C & front_left_cell(f,(len(f|k))-'1,G) meets C; then A60: f goes_straight (len(f|k))-'1,G by A2,A15,A17,A30,A32, JORDAN13:def 1; now per cases by A31,A35,A36,A37,A38,A60,GOBRD13:def 8; suppose that A61: i1 = i2 & j1+1 = j2 and A62: [i2,j2+1] in Indices G and A63: f/.((len(f|k))-'1+2) = G*(i2,j2+1); cell(G,i1,j1+1) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A59,A61,GOBRD13:35; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A61,A62,A63,GOBRD13:22; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2-'1,j2) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A59,A61,GOBRD13:34; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A62,A63,GOBRD13:21; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A64: i1+1 = i2 & j1 = j2 and A65: [i2+1,j2] in Indices G and A66: f/.((len(f|k))-'1+2) = G*(i2+1,j2); cell(G,i1+1,j1-'1) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A59,A64,GOBRD13:37; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A64,A65,A66,GOBRD13:24; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i1+1,j1) meets C by A3,A12,A17,A30,A31,A35,A36,A37 ,A38,A59,A64,GOBRD13:36; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A64,A65,A66,GOBRD13:23; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A67: i1 = i2+1 & j1 = j2 and A68: [i2-'1,j2] in Indices G and A69: f/.((len(f|k))-'1+2) = G*(i2-'1,j2); cell(G,i2-'1,j2) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A59,A67,GOBRD13:39; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A39,A68,A69,GOBRD13:26; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2-'1,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A59,A67,GOBRD13:38; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A39,A68,A69,GOBRD13:25; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A70: i1 = i2 & j1 = j2+1 and A71: [i2,j2-'1] in Indices G and A72: f/.((len(f|k))-'1+2) = G*(i2,j2-'1); A73: j2-'1+1=j2 by A40,XREAL_1:235; cell(G,i2-'1,j2-'1) misses C by A3,A30,A31,A29,A35,A36 ,A37,A38,A59,A70,GOBRD13:41; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A71,A72,A73,GOBRD13:28; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A59,A70,GOBRD13:40; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A41,A71,A72,GOBRD13:27; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; end; hence thesis; end; suppose A74: front_right_cell(f,(len(f|k))-'1,G) meets C; then A75: f turns_right (len(f|k))-'1,G by A2,A15,A17,A30,A32, JORDAN13:def 1; now per cases by A31,A35,A36,A37,A38,A75,GOBRD13:def 6; suppose that A76: i1 = i2 & j1+1 = j2 and A77: [i2+1,j2] in Indices G and A78: f/.((len(f|k))-'1+2) = G*(i2+1,j2); A79: j1+1-'1 = j1 by NAT_D:34; cell(G,i1,j1) misses C by A3,A30,A31,A29,A35,A36,A37,A38 ,A42,A76,GOBRD13:22; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A76,A77,A78,A79,GOBRD13:24; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37 ,A38,A74,A76,GOBRD13:35; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A77,A78,GOBRD13:23; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A80: i1+1 = i2 & j1 = j2 and A81: [i2,j2-'1] in Indices G and A82: f/.((len(f|k))-'1+2) = G*(i2,j2-'1); A83: i1+1-'1 = i1 by NAT_D:34; cell(G,i1,j1-'1) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A42,A80,GOBRD13:24; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A41,A80,A81,A82,A83,GOBRD13:28; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A74,A80,GOBRD13:37; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A41,A81,A82,GOBRD13:27; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A84: i1 = i2+1 & j1 = j2 and A85: [i2,j2+1] in Indices G and A86: f/.((len(f|k))-'1+2) = G*(i2,j2+1); cell(G,i2,j2) misses C by A3,A30,A31,A29,A35,A36,A37,A38 ,A42,A84,GOBRD13:26; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A85,A86,GOBRD13:22; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2-'1,j2) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A74,A84,GOBRD13:39; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A85,A86,GOBRD13:21; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; suppose that A87: i1 = i2 & j1 = j2+1 and A88: [i2-'1,j2] in Indices G and A89: f/.((len(f|k))-'1+2) = G*(i2-'1,j2); cell(G,i2-'1,j2) misses C by A3,A30,A31,A29,A35,A36,A37 ,A38,A42,A87,GOBRD13:28; then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A39,A88,A89,GOBRD13:26; hence right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33, GOBRD13:31; cell(G,i2-'1,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36 ,A37,A38,A74,A87,GOBRD13:41; then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31 ,A33,A37,A38,A39,A88,A89,GOBRD13:25; hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13 ,A33,GOBRD13:31; end; end; hence thesis; end; end; hence thesis; end; suppose m+1 <> len(f|(k+1)); then m+1 < len(f|(k+1)) by A14,XXREAL_0:1; then A90: m+1 <= len(f|k) by A16,A17,NAT_1:13; then consider i1,j1,i2,j2 be Nat such that A91: [i1,j1] in Indices G and A92: (f|k)/.m = G*(i1,j1) and A93: [i2,j2] in Indices G and A94: (f|k)/.(m+1) = G*(i2,j2) and A95: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+ 1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A9,A13,JORDAN8:3; A96: right_cell(f|k,m,G) misses C by A7,A13,A90; A97: f|(k+1) = (f|k)^<*f/.(k+1)*> by A15,FINSEQ_5:82; 1 <= m+1 by NAT_1:12; then m+1 in dom(f|k) by A90,FINSEQ_3:25; then A98: (f|(k+1))/.(m+1) = G*(i2,j2) by A94,A97,FINSEQ_4:68; A99: left_cell(f|k,m,G) meets C by A7,A13,A90; m <= len(f|k) by A90,NAT_1:13; then m in dom(f|k) by A13,FINSEQ_3:25; then A100: (f|(k+1))/.m = G*(i1,j1) by A92,A97,FINSEQ_4:68; now per cases by A95; suppose A101: i1 = i2 & j1+1 = j2; then A102: left_cell(f|k,m,G) = cell(G,i1-'1,j1) by A9,A13,A90,A91,A92 ,A93,A94,GOBRD13:21; right_cell(f|k,m,G) = cell(G,i1,j1) by A9,A13,A90,A91,A92,A93 ,A94,A101,GOBRD13:22; hence thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A101,A102, GOBRD13:21,22; end; suppose A103: i1+1 = i2 & j1 = j2; then A104: left_cell(f|k,m,G) = cell(G,i1,j1) by A9,A13,A90,A91,A92,A93 ,A94,GOBRD13:23; right_cell(f|k,m,G) = cell(G,i1,j1-'1) by A9,A13,A90,A91,A92 ,A93,A94,A103,GOBRD13:24; hence thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A103,A104, GOBRD13:23,24; end; suppose A105: i1 = i2+1 & j1 = j2; then A106: left_cell(f|k,m,G) = cell(G,i2,j2-'1) by A9,A13,A90,A91,A92 ,A93,A94,GOBRD13:25; right_cell(f|k,m,G) = cell(G,i2,j2) by A9,A13,A90,A91,A92,A93 ,A94,A105,GOBRD13:26; hence thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A105,A106, GOBRD13:25,26; end; suppose A107: i1 = i2 & j1 = j2+1; then A108: left_cell(f|k,m,G) = cell(G,i1,j2) by A9,A13,A90,A91,A92,A93 ,A94,GOBRD13:27; right_cell(f|k,m,G) = cell(G,i2-'1,j2) by A9,A13,A90,A91,A92 ,A93,A94,A107,GOBRD13:28; hence thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A107,A108, GOBRD13:27,28; end; end; hence thesis; end; end; hence thesis; end; end; hence thesis; end; end; A109: P[0] by CARD_1:27; for k be Nat holds P[k] from NAT_1:sch 2(A109,A6); hence thesis by A1; end; theorem Th8: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C misses L~Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; set G = Gauge(C,n); set f = Span(C,n); assume not thesis; then consider c be object such that A2: c in C and A3: c in L~f by XBOOLE_0:3; L~f = union { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f } by TOPREAL1:def 4; then consider Z be set such that A4: c in Z and A5: Z in { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f } by A3,TARSKI:def 4; consider i be Nat such that A6: Z = LSeg(f,i) and A7: 1 <= i and A8: i+1 <= len f by A5; f is_sequence_on G by A1,JORDAN13:def 1; then LSeg(f,i) = left_cell(f,i,G) /\ right_cell(f,i,G) by A7,A8,GOBRD13:29; then A9: c in right_cell(f,i,G) by A4,A6,XBOOLE_0:def 4; right_cell(f,i,G) misses C by A1,A7,A8,Th7; hence contradiction by A2,A9,XBOOLE_0:3; end; registration let C be Simple_closed_curve; let n be Nat; cluster Cl RightComp Span(C,n) -> compact; coherence by GOBRD14:32; end; theorem Th9: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C meets LeftComp Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; then A2: Span(C,n) is_sequence_on Gauge(C,n) by JORDAN13:def 1; A3: 1+1 <= len Span(C,n) by GOBOARD7:34,XXREAL_0:2; then left_cell(Span(C,n),1,Gauge(C,n)) meets C by A1,Th7; then left_cell(Span(C,n),1,Gauge(C,n))\L~Span(C,n) meets C by A1,Th8, XBOOLE_1:84; hence thesis by A3,A2,JORDAN9:27,XBOOLE_1:63; end; theorem Th10: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C misses RightComp Span(C,n) proof let C be Simple_closed_curve; let n be Nat; set f = Span(C,n); RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2; then A1: ex L be Subset of (TOP-REAL 2)|(L~f)` st L = RightComp f & L is a_component by CONNSP_1:def 6; LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then A2: ex R be Subset of (TOP-REAL 2)|(L~f)` st R = LeftComp f & R is a_component by CONNSP_1:def 6; assume A3: n is_sufficiently_large_for C; then A4: C misses L~f by Th8; C c= the carrier of (TOP-REAL 2)|(L~f)` proof let c be object; assume A5: c in C; then not c in L~f by A4,XBOOLE_0:3; then c in (L~f)` by A5,SUBSET_1:29; hence thesis by PRE_TOPC:8; end; then reconsider C1 = C as Subset of (TOP-REAL 2)|(L~f)`; assume A6: C meets RightComp f; A7: C1 is connected by CONNSP_1:23; C meets LeftComp f by A3,Th9; hence contradiction by A6,A1,A2,A7,JORDAN2C:92,SPRECT_4:6; end; theorem Th11: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C c= LeftComp Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; let c be object; set f = Span(C,n); assume A2: c in C; C misses L~f by A1,Th8; then A3: not c in L~f by A2,XBOOLE_0:3; C misses RightComp f by A1,Th10; then not c in RightComp f by A2,XBOOLE_0:3; hence thesis by A2,A3,GOBRD14:18; end; theorem Th12: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C c= UBD L~Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume n is_sufficiently_large_for C; then A1: C c= LeftComp Span(C,n) by Th11; LeftComp Span(C,n) c= UBD L~Span(C,n) by GOBRD14:34,JORDAN2C:23; hence thesis by A1; end; theorem Th13: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds BDD L~Span(C,n) c= BDD C proof let C be Simple_closed_curve; let n be Nat; assume that A1: n is_sufficiently_large_for C and A2: not BDD L~Span(C,n) c= BDD C; set f = Span(C,n); A3: Cl BDD L~f = Cl RightComp f by GOBRD14:37 .= (RightComp f) \/ L~f by GOBRD14:21; len f >= 1 by GOBOARD7:34,XXREAL_0:2; then A4: 1 in dom f by FINSEQ_3:25; len f > 4 by GOBOARD7:34; then f/.1 in L~f by A4,GOBOARD1:1,XXREAL_0:2; then SpanStart(C,n) in L~f by A1,JORDAN13:def 1; then A5: SpanStart(C,n) in Cl BDD L~f by A3,XBOOLE_0:def 3; SpanStart(C,n) in BDD C by A1,Th6; then A6: BDD L~f meets BDD C by A5,PRE_TOPC:def 7; BDD C misses UBD C by JORDAN2C:24; then A7: BDD C,UBD C are_separated by TSEP_1:37; BDD L~f misses UBD L~f by JORDAN2C:24; then C misses BDD L~f by A1,Th12,XBOOLE_1:63; then A8: BDD L~f c= C` by SUBSET_1:23; BDD C \/ UBD C = C` by JORDAN2C:27; then BDD L~f c= UBD C by A2,A8,A7,CONNSP_1:16; then BDD C meets UBD C by A6,XBOOLE_1:63; hence contradiction by JORDAN2C:24; end; theorem Th14: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds UBD C c= UBD L~Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; let x be object; A2: BDD C misses UBD C by JORDAN2C:24; assume A3: x in UBD C; then reconsider p = x as Point of TOP-REAL 2; A4: Cl BDD L~Span(C,n) c= Cl BDD C by A1,Th13,PRE_TOPC:19; A5: now assume x in L~Span(C,n); then p in (RightComp Span(C,n)) \/ L~Span(C,n) by XBOOLE_0:def 3; then p in Cl RightComp Span(C,n) by GOBRD14:21; then p in Cl BDD L~Span(C,n) by GOBRD14:37; hence contradiction by A4,A2,A3,PRE_TOPC:def 7; end; BDD L~Span(C,n) c= BDD C by A1,Th13; then not x in BDD L~Span(C,n) by A2,A3,XBOOLE_0:3; then not x in RightComp Span(C,n) by GOBRD14:37; then p in LeftComp Span(C,n) by A5,GOBRD14:17; hence thesis by GOBRD14:36; end; theorem for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds RightComp Span(C,n) c= BDD C proof let C be Simple_closed_curve; let n be Nat; assume n is_sufficiently_large_for C; then BDD L~Span(C,n) c= BDD C by Th13; hence thesis by GOBRD14:37; end; theorem Th16: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds UBD C c= LeftComp Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume n is_sufficiently_large_for C; then UBD C c= UBD L~Span(C,n) by Th14; hence thesis by GOBRD14:36; end; theorem Th17: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds UBD C misses BDD L~Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume that A1: n is_sufficiently_large_for C and A2: UBD C meets BDD L~Span(C,n); UBD L~Span(C,n) meets BDD L~Span(C,n) by A1,A2,Th14,XBOOLE_1:63; hence contradiction by JORDAN2C:24; end; theorem for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds UBD C misses RightComp Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume n is_sufficiently_large_for C; then UBD C misses BDD L~Span(C,n) by Th17; hence thesis by GOBRD14:37; end; theorem Th19: for C be Simple_closed_curve for P be Subset of TOP-REAL 2 for n be Nat st n is_sufficiently_large_for C holds P is_outside_component_of C implies P misses L~Span(C,n) proof let C be Simple_closed_curve; let P be Subset of TOP-REAL 2; let n be Nat; assume that A1: n is_sufficiently_large_for C and A2: P is_outside_component_of C and A3: P meets L~Span(C,n); A4: UBD C c= LeftComp Span(C,n) by A1,Th16; consider x be object such that A5: x in P and A6: x in L~Span(C,n) by A3,XBOOLE_0:3; P c= UBD C by A2,JORDAN2C:23; then x in UBD C by A5; hence contradiction by A6,A4,GOBRD14:17; end; theorem Th20: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds UBD C misses L~Span(C,n) proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; assume UBD C meets L~Span(C,n); then consider x be object such that A2: x in UBD C and A3: x in L~Span(C,n) by XBOOLE_0:3; UBD C = union {B where B is Subset of TOP-REAL 2: B is_outside_component_of C} by JORDAN2C:def 5; then consider Z be set such that A4: x in Z and A5: Z in {B where B is Subset of TOP-REAL 2: B is_outside_component_of C } by A2,TARSKI:def 4; consider B be Subset of TOP-REAL 2 such that A6: Z = B and A7: B is_outside_component_of C by A5; B misses L~Span(C,n) by A1,A7,Th19; hence thesis by A3,A4,A6,XBOOLE_0:3; end; theorem Th21: for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds L~Span(C,n) c= BDD C proof let C be Simple_closed_curve; let n be Nat; assume A1: n is_sufficiently_large_for C; then C misses L~Span(C,n) by Th8; then L~Span(C,n) c= C` by SUBSET_1:23; then A2: L~Span(C,n) c= BDD C \/ UBD C by JORDAN2C:27; UBD C misses L~Span(C,n) by A1,Th20; hence thesis by A2,XBOOLE_1:73; end; theorem Th22: for C be Simple_closed_curve for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds i > 1 proof let C be Simple_closed_curve; let i,j,k,n be Nat; assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len Span(C,n) and A4: [i,j] in Indices Gauge(C,n) and A5: Span(C,n)/.k = Gauge(C,n)*(i,j); A6: len Span(C,n) > 4 by GOBOARD7:34; SpanStart(C,n) in BDD C by A1,Th6; then A7: W-bound C <= W-bound BDD C by JORDAN1C:6; A8: j <= width Gauge(C,n) by A4,MATRIX_0:32; k in dom Span(C,n) by A2,A3,FINSEQ_3:25; then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2; then A9: W-bound L~Span(C,n) <= Gauge(C,n)*(i,j)`1 by A5,PSCOMP_1:24; A10: BDD C c= Cl BDD C by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl BDD C is compact by TOPREAL6:79; SpanStart(C,n) in BDD C by A1,Th6; then A13: W-bound BDD C = W-bound Cl BDD C by A11,TOPREAL6:85; L~Span(C,n) c= BDD C by A1,Th21; then W-bound L~Span(C,n) >= W-bound Cl BDD C by A12,A10,PSCOMP_1:69 ,XBOOLE_1:1; then A14: W-bound BDD C <= Gauge(C,n)*(i,j)`1 by A13,A9,XXREAL_0:2; len Gauge(C,n) >= 4 by JORDAN8:10; then A15: len Gauge(C,n) >= 2 by XXREAL_0:2; A16: 1 <= i by A4,MATRIX_0:32; A17: 1 <= j by A4,MATRIX_0:32; len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then Gauge(C,n)*(2,j)`1 = W-bound C by A17,A8,JORDAN8:11; then Gauge(C,n)*(2,j)`1 <= Gauge(C,n)*(i,j)`1 by A7,A14,XXREAL_0:2; then i >= 1+1 by A16,A17,A8,A15,GOBOARD5:3; hence thesis by NAT_1:13; end; theorem Th23: for C be Simple_closed_curve for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds i < len Gauge(C,n) proof let C be Simple_closed_curve; let i,j,k,n be Nat; assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len Span(C,n) and A4: [i,j] in Indices Gauge(C,n) and A5: Span(C,n)/.k = Gauge(C,n)*(i,j); A6: len Span(C,n) > 4 by GOBOARD7:34; SpanStart(C,n) in BDD C by A1,Th6; then A7: E-bound C >= E-bound BDD C by JORDAN1C:7; A8: 1 <= j by A4,MATRIX_0:32; k in dom Span(C,n) by A2,A3,FINSEQ_3:25; then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2; then A9: E-bound L~Span(C,n) >= Gauge(C,n)*(i,j)`1 by A5,PSCOMP_1:24; A10: BDD C c= Cl BDD C by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl BDD C is compact by TOPREAL6:79; SpanStart(C,n) in BDD C by A1,Th6; then A13: E-bound BDD C = E-bound Cl BDD C by A11,TOPREAL6:86; L~Span(C,n) c= BDD C by A1,Th21; then E-bound L~Span(C,n) <= E-bound Cl BDD C by A12,A10,PSCOMP_1:67 ,XBOOLE_1:1; then A14: E-bound BDD C >= Gauge(C,n)*(i,j)`1 by A13,A9,XXREAL_0:2; A15: len Gauge(C,n) >= 4 by JORDAN8:10; then len Gauge(C,n) >= 1+1 by XXREAL_0:2; then A16: len Gauge(C,n)-1 >= 1 by XREAL_1:19; A17: len Gauge(C,n)-'1 >= 1 by A16,XREAL_0:def 2; A18: j <= width Gauge(C,n) by A4,MATRIX_0:32; len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; then Gauge(C,n)*(len Gauge(C,n)-'1,j)`1 = E-bound C by A8,A18,JORDAN8:12; then A19: Gauge(C,n)*(len Gauge(C,n)-'1,j)`1 >= Gauge(C,n)*(i,j)`1 by A7,A14, XXREAL_0:2; i <= len Gauge(C,n) by A4,MATRIX_0:32; then i <= len Gauge(C,n)-'1 by A8,A18,A17,A19,GOBOARD5:3; then i < len Gauge(C,n)-'1+1 by NAT_1:13; hence thesis by A15,XREAL_1:235,XXREAL_0:2; end; theorem Th24: for C be Simple_closed_curve for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds j > 1 proof let C be Simple_closed_curve; let i,j,k,n be Nat; assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len Span(C,n) and A4: [i,j] in Indices Gauge(C,n) and A5: Span(C,n)/.k = Gauge(C,n)*(i,j); A6: len Span(C,n) > 4 by GOBOARD7:34; SpanStart(C,n) in BDD C by A1,Th6; then A7: S-bound C <= S-bound BDD C by JORDAN1C:8; A8: i <= len Gauge(C,n) by A4,MATRIX_0:32; k in dom Span(C,n) by A2,A3,FINSEQ_3:25; then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2; then A9: S-bound L~Span(C,n) <= Gauge(C,n)*(i,j)`2 by A5,PSCOMP_1:24; A10: BDD C c= Cl BDD C by PRE_TOPC:18; A11: BDD C is bounded by JORDAN2C:106; then A12: Cl BDD C is compact by TOPREAL6:79; SpanStart(C,n) in BDD C by A1,Th6; then A13: S-bound BDD C = S-bound Cl BDD C by A11,TOPREAL6:88; L~Span(C,n) c= BDD C by A1,Th21; then S-bound L~Span(C,n) >= S-bound Cl BDD C by A12,A10,PSCOMP_1:68 ,XBOOLE_1:1; then A14: S-bound BDD C <= Gauge(C,n)*(i,j)`2 by A13,A9,XXREAL_0:2; len Gauge(C,n) >= 4 by JORDAN8:10; then A15: len Gauge(C,n) >= 2 by XXREAL_0:2; A16: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; A17: 1 <= i by A4,MATRIX_0:32; then Gauge(C,n)*(i,2)`2 = S-bound C by A8,JORDAN8:13; then A18: Gauge(C,n)*(i,2)`2 <= Gauge(C,n)*(i,j)`2 by A7,A14,XXREAL_0:2; 1 <= j by A4,MATRIX_0:32; then j >= 1+1 by A17,A8,A16,A15,A18,GOBOARD5:4; hence thesis by NAT_1:13; end; theorem Th25: for C be Simple_closed_curve for i,j,k,n be Nat st n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds j < width Gauge(C,n) proof let C be Simple_closed_curve; let i,j,k,n be Nat; assume that A1: n is_sufficiently_large_for C and A2: 1 <= k and A3: k <= len Span(C,n) and A4: [i,j] in Indices Gauge(C,n) and A5: Span(C,n)/.k = Gauge(C,n)*(i,j); A6: len Span(C,n) > 4 by GOBOARD7:34; k in dom Span(C,n) by A2,A3,FINSEQ_3:25; then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2; then A7: N-bound L~Span(C,n) >= Gauge(C,n)*(i,j)`2 by A5,PSCOMP_1:24; A8: BDD C c= Cl BDD C by PRE_TOPC:18; A9: BDD C is bounded by JORDAN2C:106; then A10: Cl BDD C is compact by TOPREAL6:79; SpanStart(C,n) in BDD C by A1,Th6; then A11: N-bound BDD C = N-bound Cl BDD C by A9,TOPREAL6:87; L~Span(C,n) c= BDD C by A1,Th21; then N-bound L~Span(C,n) <= N-bound Cl BDD C by A10,A8,PSCOMP_1:66,XBOOLE_1:1 ; then A12: N-bound BDD C >= Gauge(C,n)*(i,j)`2 by A11,A7,XXREAL_0:2; A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1; A14: len Gauge(C,n) >= 4 by JORDAN8:10; then len Gauge(C,n) >= 1+1 by XXREAL_0:2; then A15: len Gauge(C,n)-1 >= 1 by XREAL_1:19; SpanStart(C,n) in BDD C by A1,Th6; then A16: N-bound C >= N-bound BDD C by JORDAN1C:9; A17: i <= len Gauge(C,n) by A4,MATRIX_0:32; A18: 1 <= i by A4,MATRIX_0:32; then Gauge(C,n)*(i,len Gauge(C,n)-'1)`2 = N-bound C by A17,JORDAN8:14; then A19: Gauge(C,n)*(i,len Gauge(C,n)-'1)`2 >= Gauge(C,n)*(i,j)`2 by A16,A12, XXREAL_0:2; A20: len Gauge(C,n)-'1 >= 1 by A15,XREAL_0:def 2; j <= width Gauge(C,n) by A4,MATRIX_0:32; then j <= len Gauge(C,n)-'1 by A18,A17,A20,A19,GOBOARD5:4; then j < len Gauge(C,n)-'1+1 by NAT_1:13; hence thesis by A13,A14,XREAL_1:235,XXREAL_0:2; end; theorem for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds Y-SpanStart(C,n) < width Gauge(C,n) proof let C be Simple_closed_curve; let n be Nat; A1: len Span(C,n) > 1 by GOBOARD7:34,XXREAL_0:2; assume A2: n is_sufficiently_large_for C; then A3: Span(C,n)/.1 = Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) by JORDAN13:def 1; [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices Gauge(C,n) by A2,JORDAN11:8; hence thesis by A2,A1,A3,Th25; end; theorem Th27: for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n,m be Nat st m >= n & n >= 1 holds X-SpanStart(C,m) = 2|^(m-' n)*(X-SpanStart(C,n)-2)+2 proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n,m be Nat; A1: X-SpanStart(C,n) = 2|^(n-'1) + 2 by JORDAN1H:def 2; assume A2: m >=n; assume A3: n >= 1; then (m-'n)+(n-'1) = (m-'n)+(n-1) by XREAL_1:233 .= (m-'n)+ n-1 .= m-1 by A2,XREAL_1:235 .= m-'1 by A2,A3,XREAL_1:233,XXREAL_0:2; then 2|^(m-'1) = 2|^(m-'n)*(X-SpanStart(C,n)-2) by A1,NEWTON:8; hence thesis by JORDAN1H:def 2; end; theorem Th28: for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n,m be Nat st n <= m & n is_sufficiently_large_for C holds m is_sufficiently_large_for C proof let C be compact non vertical non horizontal Subset of TOP-REAL 2; let n,m be Nat; assume that A1: n <= m and A2: n is_sufficiently_large_for C; consider j be Nat such that A3: j < width Gauge(C,n) and A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C by A2,JORDAN1H:def 3; set iin = X-SpanStart(C,n); set iim = X-SpanStart(C,m); n >= 1 by A2,JORDAN1H:51; then A5: iim = 2|^(m-'n)*(iin-2)+2 by A1,Th27; A6: j > 1 proof A7: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:50; assume A8: j <= 1; per cases by A8,NAT_1:25; suppose A9: j = 0; width Gauge(C,n) >= 0; then A10: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A7,JORDAN1A:24; cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A7,JORDAN1A:49; hence contradiction by A4,A9,A10,JORDAN2C:24,XBOOLE_1:68; end; suppose A11: j = 1; set i1 = X-SpanStart(C,n); A12: i1-'1 <= i1 by NAT_D:44; i1 < len Gauge(C,n) by JORDAN1H:49; then A13: i1-'1 < len Gauge(C,n) by A12,XXREAL_0:2; BDD C c= C` by JORDAN2C:25; then A14: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A4,A11; UBD C is_outside_component_of C by JORDAN2C:68; then A15: UBD C is_a_component_of C` by JORDAN2C:def 3; width Gauge(C,n) <> 0 by MATRIX_0:def 10; then A16: 0+1 <= width Gauge(C,n) by NAT_1:14; then A17: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A7,JORDAN1A:24; A18: 1 <= i1-'1 by JORDAN1H:50; 0 < width Gauge(C,n) by A16; then cell(Gauge(C,n),i1-'1,0)/\cell(Gauge(C,n),i1-'1,0+1) = LSeg(Gauge(C ,n)*(i1-'1,0+1),Gauge(C,n)*(i1-'1+1,0+1)) by A13,A18,GOBOARD5:26; then A19: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0+1) by XBOOLE_0:def 7; cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A7,JORDAN1A:49; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A16,A13,A19,A15 ,A14,GOBOARD9:4,JORDAN1A:25; hence contradiction by A4,A11,A17,JORDAN2C:24,XBOOLE_1:68; end; end; then 2|^(m-'n)*(j-2)+2 > 1 by A1,A3,JORDAN1A:32; then reconsider j1 = 2|^(m-'n)*(j-2)+2 as Element of NAT by INT_1:3; iin > 2 by JORDAN1H:49; then A20: iin >= 2+1 by NAT_1:13; A21: j+1 < width Gauge(C,n) proof assume j+1 >= width Gauge(C,n); then A22: j+1 > width Gauge(C,n) or j+1 = width Gauge(C,n) by XXREAL_0:1; A23: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:50; per cases by A3,A22,NAT_1:13; suppose A24: j = width Gauge(C,n); A25: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A23, JORDAN1A:50; cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) is non empty by A23,A24, JORDAN1A:24; hence contradiction by A4,A24,A25,JORDAN2C:24,XBOOLE_1:68; end; suppose j + 1 = width Gauge(C,n); then A26: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= BDD C by A4,NAT_D:34; BDD C c= C` by JORDAN2C:25; then A27: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= C` by A26; A28: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A23, JORDAN1A:50; set i1 = X-SpanStart(C,n); A29: i1-'1 <= i1 by NAT_D:44; i1 < len Gauge(C,n) by JORDAN1H:49; then A30: i1-'1 < len Gauge(C,n) by A29,XXREAL_0:2; UBD C is_outside_component_of C by JORDAN2C:68; then A31: UBD C is_a_component_of C` by JORDAN2C:def 3; width Gauge(C,n)-'1 <= width Gauge(C,n) by NAT_D:44; then A32: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is non empty by A23,JORDAN1A:24; A33: width Gauge(C,n)-1 < width Gauge(C,n) by XREAL_1:146; A34: 1 <= i1-'1 by JORDAN1H:50; A35: width Gauge(C,n)<>0 by MATRIX_0:def 10; then width Gauge(C,n)-'1+1 = width Gauge(C,n) by NAT_1:14,XREAL_1:235; then cell(Gauge(C,n),i1-'1,width Gauge(C,n))/\ cell(Gauge(C,n),i1-'1, width Gauge(C,n)-'1) = LSeg(Gauge(C,n)*(i1-'1,width Gauge(C,n)), Gauge(C,n)*(i1 -'1+1,width Gauge(C,n))) by A30,A33,A34,GOBOARD5:26; then A36: cell(Gauge(C,n),i1-'1,width Gauge(C,n)) meets cell(Gauge(C,n),i1-'1 ,width Gauge(C,n)-'1) by XBOOLE_0:def 7; width Gauge(C,n)-'1 < width Gauge(C,n) by A35,A33,NAT_1:14,XREAL_1:233; then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= UBD C by A28,A30,A36,A31,A27,GOBOARD9:4,JORDAN1A:25; hence contradiction by A26,A32,JORDAN2C:24,XBOOLE_1:68; end; end; iin < len Gauge(C,n) by JORDAN1H:49; then cell(Gauge(C,m),iim-'1,j1) c= cell(Gauge(C,n),iin-'1,j) by A1,A5,A20,A6 ,A21,JORDAN1A:48; then A37: cell(Gauge(C,m),X-SpanStart(C,m)-'1,j1) c= BDD C by A4; j1 < width Gauge(C,m) by A1,A3,A6,JORDAN1A:32; hence thesis by A37,JORDAN1H:def 3; end; theorem Th29: for G be Go-board for f be FinSequence of TOP-REAL 2 for i,j be Nat holds f is_sequence_on G & f is special & i <= len G & j <= width G implies cell(G,i,j)\L~f is connected proof let G be Go-board; let f be FinSequence of TOP-REAL 2; let i,j be Nat; assume that A1: f is_sequence_on G and A2: f is special and A3: i<=len G and A4: j<=width G; Int cell(G,i,j) misses L~f by A1,A2,A3,A4,JORDAN9:14; then A5: Int cell(G,i,j) c= (L~f)` by SUBSET_1:23; cell(G,i,j)\L~f c= cell(G,i,j) by XBOOLE_1:36; then A6: cell(G,i,j)\L~f c= Cl Int cell(G,i,j) by A3,A4,GOBRD11:35; A7: Int cell(G,i,j) c= cell(G,i,j) by TOPS_1:16; A8: Int cell(G,i,j) is convex by A3,A4,GOBOARD9:17; cell(G,i,j)\L~f = cell(G,i,j) /\ (L~f)` by SUBSET_1:13; then Int cell(G,i,j) c= cell(G,i,j)\L~f by A5,A7,XBOOLE_1:19; hence thesis by A6,A8,CONNSP_1:18; end; theorem Th30: for C be Simple_closed_curve for n,k be Nat st n is_sufficiently_large_for C & Y-SpanStart(C,n) <= k & k <= 2|^(n-'ApproxIndex C )*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,k)\L~Span(C,n) c= BDD L~Span(C,n) proof let C be Simple_closed_curve; let n,k be Nat; set G = Gauge(C,n); set f = Span(C,n); set AI = ApproxIndex C; set YI = Y-InitStart C; set XS = X-SpanStart(C,n); set YS = Y-SpanStart(C,n); assume that A1: n is_sufficiently_large_for C and A2: YS <= k and A3: k <= 2|^(n-'AI)*(YI-'2)+2; A4: f is_sequence_on G by A1,JORDAN13:def 1; reconsider ro = k-YS as Element of NAT by A2,INT_1:5; A5: ro <= 2|^(n-'AI)*(YI-'2)+2-YS by A3,XREAL_1:9; A6: k = YS+ro; defpred P[Nat] means $1 <= 2|^(n-'AI)*(YI-'2)+2-YS implies cell(G ,XS-'1,YS+$1)\L~f c= BDD L~f; A7: 1 <= XS-'1 by JORDAN1H:50; XS > 2 by JORDAN1H:49; then A8: XS-'1+1 = XS by XREAL_1:235,XXREAL_0:2; A9: XS-'1 < len G by JORDAN1H:50; A10: for t being Nat st P[t] holds P[t+1] proof let t be Nat; assume A11: t <= 2|^(n-'AI)*(YI-'2)+2-YS implies cell(G,XS-'1,YS+t)\L~f c= BDD L~f; set Ls = LSeg(G*(XS-'1,YS+(t+1)),G*(XS,YS+(t+1))); A12: t < t+1 by NAT_1:13; set p = (1/2)*(G*(XS-'1,YS+(t+1))+G*(XS,YS+(t+1))); A13: cell(G,XS-'1,YS+(t+1))\L~f c= (L~f)` proof let y be object; assume A14: y in cell(G,XS-'1,YS+(t+1))\L~f; then not y in L~f by XBOOLE_0:def 5; hence thesis by A14,SUBSET_1:29; end; A15: p in Ls by RLTOPSP1:69; A16: YS+t+1 = YS+(t+1); then A17: 1 <= YS+(t+1) by NAT_1:11; A18: YI > 1 by JORDAN11:2; then YI >= 1+1+0 by NAT_1:13; then YI-2 >= 0 by XREAL_1:19; then A19: YI-'2 = YI-2 by XREAL_0:def 2; assume A20: t+1 <= 2|^(n-'AI)*(YI-'2)+2-YS; then A21: t+1+YS <= 2|^(n-'AI)*(YI-'2)+2 by XREAL_1:19; assume not cell(G,XS-'1,YS+(t+1))\L~f c= BDD L~f; then consider x be object such that A22: x in cell(G,XS-'1,YS+(t+1))\L~f and A23: not x in BDD L~f; not x in L~f by A22,XBOOLE_0:def 5; then x in (L~f)` by A22,SUBSET_1:29; then x in (BDD L~f) \/ (UBD L~f) by JORDAN2C:27; then x in UBD L~f by A23,XBOOLE_0:def 3; then A24: cell(G,XS-'1,YS+(t+1))\L~f meets UBD L~f by A22,XBOOLE_0:3; A25: YI < width Gauge(C,AI) by JORDAN11:def 2; AI <= n by A1,JORDAN11:def 1; then 2|^(n-'AI)*(YI-2)+2 < width Gauge(C,n) by A18,A25,JORDAN1A:32; then A26: YS+t+1 <= width G by A19,A21,XXREAL_0:2; A27: YS+t+1 <= 2|^(n-'AI)*(YI-'2)+2 by A21; A28: now A29: YS <= YS+(t+1) by NAT_1:11; A30: XS < len G by JORDAN1H:49; assume p in L~f; then consider i be Nat such that A31: 1 <= i and A32: i+1 <= len f and A33: p in LSeg(f,i) by SPPOL_2:13; A34: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A31,A32,TOPREAL1:def 3; consider i1,j1,i2,j2 be Nat such that A35: [i1,j1] in Indices G and A36: f/.i = G*(i1,j1) and A37: [i2,j2] in Indices G and A38: f/.(i+1) = G*(i2,j2) and A39: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A4,A31,A32,JORDAN8:3; A40: 1 <= i1 by A35,MATRIX_0:32; A41: i2 <= len G by A37,MATRIX_0:32; A42: 1 <= i2 by A37,MATRIX_0:32; A43: j1 <= width G by A35,MATRIX_0:32; A44: 1 <= j2 by A37,MATRIX_0:32; A45: i1 <= len G by A35,MATRIX_0:32; A46: j2 <= width G by A37,MATRIX_0:32; A47: 1 <= j1 by A35,MATRIX_0:32; per cases by A39; suppose i1 = i2 & j1+1 = j2; hence contradiction by A7,A8,A26,A17,A33,A34,A36,A38,A40,A45,A47,A46 ,A30,GOBOARD7:27; end; suppose A48: i1+1 = i2 & j1 = j2; then A49: YS+(t+1) = j1 by A7,A8,A26,A17,A33,A34,A36,A38,A40,A47,A43,A41,A30, GOBOARD7:26; A50: cell(G,XS-'1,YS+(t+1)) c= BDD C by A1,A21,A29,JORDAN11:def 3; A51: left_cell(f,i,G) = cell(G,i1,j1) by A4,A31,A32,A35,A36,A37,A38,A48, GOBRD13:23; XS-'1 = i1 by A7,A8,A26,A17,A33,A34,A36,A38,A40,A47,A43,A41,A30,A48, GOBOARD7:26; then cell(G,XS-'1,YS+(t+1)) meets C by A1,A31,A32,A49,A51,Th7; hence contradiction by A50,JORDAN1A:7,XBOOLE_1:63; end; suppose A52: i1 = i2+1 & j1 = j2; then A53: left_cell(f,i,G) = cell(G,i2,j2-'1) by A4,A31,A32,A35,A36,A37,A38, GOBRD13:25; A54: YS+(t+1) = j2 by A7,A8,A26,A17,A33,A34,A36,A38,A45,A47,A43,A42,A30,A52, GOBOARD7:26; XS-'1 = i2 by A7,A8,A26,A17,A33,A34,A36,A38,A45,A47,A43,A42,A30,A52, GOBOARD7:26; then cell(G,XS-'1,YS+(t+1)-'1) meets C by A1,A31,A32,A54,A53,Th7; then A55: cell(G,XS-'1,YS+t) meets C by A16,NAT_D:34; A56: YS <= YS+t by NAT_1:11; YS+t <= 2|^(n-'AI)*(YI-'2)+2 by A27,NAT_1:13; then cell(G,XS-'1,YS+t) c= BDD C by A1,A56,JORDAN11:def 3; hence contradiction by A55,JORDAN1A:7,XBOOLE_1:63; end; suppose i1 = i2 & j1 = j2+1; hence contradiction by A7,A8,A26,A17,A33,A34,A36,A38,A40,A45,A43,A44 ,A30,GOBOARD7:27; end; end; YS+t < width G by A26,NAT_1:13; then Ls c= cell(G,XS-'1,YS+t) by A7,A9,A8,A16,GOBOARD5:21; then A57: p in cell(G,XS-'1,YS+t)\L~f by A28,A15,XBOOLE_0:def 5; Ls c= cell(G,XS-'1,YS+(t+1)) by A7,A9,A8,A26,A17,GOBOARD5:22; then A58: p in cell(G,XS-'1,YS+(t+1))\L~f by A28,A15,XBOOLE_0:def 5; LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then UBD L~f is_a_component_of (L~f)` by GOBRD14:36; then cell(G,XS-'1,YS+(t+1))\L~f c= UBD L~f by A4,A9,A26,A24,A13,Th29, GOBOARD9:4; then BDD L~f meets UBD L~f by A11,A20,A12,A57,A58,XBOOLE_0:3,XXREAL_0:2; hence contradiction by JORDAN2C:24; end; A59: P[0] proof assume 0 <= 2|^(n-'AI)*(YI-'2)+2-YS; A60: f/.(1+1) = G*(XS-'1,YS) by A1,JORDAN13:def 1; A61: [XS,YS] in Indices Gauge(C,n) by A1,JORDAN11:8; A62: [XS-'1,YS] in Indices Gauge(C,n) by A1,JORDAN11:9; A63: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2; then A64: right_cell(f,1,G)\L~f c= RightComp f by A4,JORDAN9:27; f/.1 = G*(XS,YS) by A1,JORDAN13:def 1; then right_cell(f,1,G) = cell(G,XS-'1,YS) by A4,A8,A63,A60,A61,A62, GOBRD13:26; hence thesis by A64,GOBRD14:37; end; for t be Nat holds P[t] from NAT_1:sch 2(A59,A10); hence thesis by A6,A5; end; theorem Th31: for C be Subset of TOP-REAL 2 for n,m,i be Nat st m <= n & 1 < i & i+1 < len Gauge(C,m) holds 2|^(n-'m)*(i-2)+2+1 < len Gauge(C,n) proof let C be Subset of TOP-REAL 2; let n,m,i be Nat; assume that A1: m <= n and A2: 1 < i and A3: i+1 < len Gauge(C,m); 1+1 <= i by A2,NAT_1:13; then reconsider i2 = i-2 as Element of NAT by INT_1:5; A4: 2|^(n-'m) > 0 by NEWTON:83; len Gauge(C,m) = 2|^m + (2+1) by JORDAN8:def 1 .= 2|^m + 2+1; then i < 2|^m + 2 by A3,XREAL_1:7; then i2 < 2|^m by XREAL_1:19; then 2|^(n-'m)*i2 < 2|^(n-'m)*2|^m by A4,XREAL_1:68; then 2|^(n-'m)*i2 < 2|^(n-'m+m) by NEWTON:8; then 2|^(n-'m)*i2 < 2|^n by A1,XREAL_1:235; then 2|^(n-'m)*(i2)+2 < 2|^n + 2 by XREAL_1:8; then 2|^(n-'m)*(i-2)+2+1 < 2|^n + 2+1 by XREAL_1:8; then 2|^(n-'m)*(i-2)+2+1 < 2|^n + (1+2); hence thesis by JORDAN8:def 1; end; theorem Th32: for C be Simple_closed_curve for n,m be Nat st n is_sufficiently_large_for C & n <= m holds RightComp Span(C,n) meets RightComp Span(C,m) proof let C be Simple_closed_curve; let n,m be Nat; assume that A1: n is_sufficiently_large_for C and A2: n <= m; set i1 = X-SpanStart(C,m); set G1 = Gauge(C,m); set YI = Y-InitStart C; set AI = ApproxIndex C; A3: m is_sufficiently_large_for C by A1,A2,Th28; then A4: AI <= m by JORDAN11:def 1; set i = X-SpanStart(C,n); set G = Gauge(C,n); A5: 1 <= i1-'1 by JORDAN1H:50; set j1 = Y-SpanStart(C,m); set f1 = Span(C,m); j1 <= 2|^(m-'AI)*(YI-'2)+2 by A3,JORDAN11:5; then A6: cell(G1,i1-'1,2|^(m-'AI)*(YI-'2)+2)\L~f1 c= BDD L~f1 by A1,A2,Th28,Th30; A7: i < len G by JORDAN1H:49; then i+1 <= len G by NAT_1:13; then A8: i <= len G - 1 by XREAL_1:19; set XSAI = X-SpanStart(C,AI); set p2 = Gauge(C,AI)*(XSAI,YI); A9: 1 < XSAI by JORDAN1H:49,XXREAL_0:2; A10: YI + 1 < width Gauge(C,AI) by JORDAN11:3; then A11: YI < width Gauge(C,AI) by NAT_1:13; set j4 = 2|^(n-'AI)*(YI-'2)+2; A12: i1 < len G1 by JORDAN1H:49; set j = Y-SpanStart(C,n); set f = Span(C,n); j <= 2|^(n-'AI)*(YI-'2)+2 by A1,JORDAN11:5; then A13: cell(G,i-'1,2|^(n-'AI)*(YI-'2)+2)\L~f c= BDD L~f by A1,Th30; A14: Int cell(G,i-'1,j4) c= cell(G,i-'1,j4) by TOPS_1:16; A15: 2 < i by JORDAN1H:49; then A16: i-'1+1 = i by XREAL_1:235,XXREAL_0:2; then A17: i-'1 >= 1+1 by A15,NAT_1:13; set j3 = 2|^(m-'AI)*(YI-'2)+2; A18: i < len G by JORDAN1H:49; A19: YI > 1 by JORDAN11:2; then YI >= 1+1+0 by NAT_1:13; then A20: YI-2 >= 0 by XREAL_1:19; then A21: 2|^(n-'AI)*(YI-'2)+2 = 2|^(n-'AI)*(YI-2)+2 by XREAL_0:def 2; A22: 2|^(m-'AI)*(YI-'2)+2 = 2|^(m-'AI)*(YI-2)+2 by A20,XREAL_0:def 2; then A23: 1 < 2|^(m-'AI)*(YI-'2)+2 by A4,A11,A19,JORDAN1A:32; set p3 = 1/2*(G1*(i1-'1,j3)+G1*(i1,j3+1)); A24: i1-'1 < len G1 by JORDAN1H:50; A25: 2|^(m-'AI)*(YI-'2)+2 < width G1 by A4,A11,A19,A22,JORDAN1A:32; then A26: j3+1 <= width G1 by NAT_1:13; 2 < i1 by JORDAN1H:49; then A27: i1-'1+1 = i1 by XREAL_1:235,XXREAL_0:2; then A28: p3 in Int cell(G1,i1-'1,j3) by A12,A23,A5,A26,GOBOARD6:31; then A29: G1*(i1-'1,j3)`2 < p3`2 by A12,A23,A27,A5,A26,Th4; A30: p3`2 < G1*(i1-'1,j3+1)`2 by A12,A23,A27,A5,A26,A28,Th4; A31: G1*(i1-'1,j3)`1 < p3`1 by A12,A23,A27,A5,A26,A28,Th4; A32: 1 < i1 by JORDAN1H:49,XXREAL_0:2; then A33: G1*(i1,j3)`2 = G1*(1,j3)`2 by A12,A23,A25,GOBOARD5:1 .= G1*(i1-'1,j3)`2 by A23,A25,A5,A24,GOBOARD5:1; A34: j3+1 >= 1 by NAT_1:11; then A35: G1*(i1,j3+1)`2 = G1*(1,j3+1)`2 by A12,A32,A26,GOBOARD5:1 .= G1*(i1-'1,j3+1)`2 by A5,A24,A26,A34,GOBOARD5:1; A36: 1 <= i-'1 by JORDAN1H:50; A37: AI <= n by A1,JORDAN11:def 1; then A38: 1 < 2|^(n-'AI)*(YI-'2)+2 by A11,A19,A21,JORDAN1A:32; YI+1 < len Gauge(C,AI) by A10,JORDAN8:def 1; then 2|^(n-'AI)*(YI-'2)+2+1 < len G by A37,A21,Th31,JORDAN11:2; then 2|^(n-'AI)*(YI-'2)+2+1+1 <= len G by NAT_1:13; then A39: j4+1 <= len G - 1 by XREAL_1:19; A40: i-'1 < len G by JORDAN1H:50; then i-'1+1 <= len G by NAT_1:13; then A41: i-'1 <= len G - 1 by XREAL_1:19; A42: 2|^(n-'AI)*(YI-'2)+2 < width G by A37,A11,A19,A21,JORDAN1A:32; then A43: j4+1 <= width G by NAT_1:13; j4 < len G by A42,JORDAN8:def 1; then j4+1 <= len G by NAT_1:13; then A44: j4 <= len G - 1 by XREAL_1:19; A45: XSAI < len Gauge(C,AI) by JORDAN1H:49; i1 = 2|^(m-'AI)*(XSAI-2)+2 by A1,A2,Th28,JORDAN11:4; then A46: p2 = G1*(i1,2|^(m-'AI)*(YI-'2)+2) by A4,A9,A45,A11,A19,A22,JORDAN1A:33; A47: i = 2|^(n-'AI)*(XSAI-2)+2 by A1,JORDAN11:4; then A48: p2 = G*(i,2|^(n-'AI)*(YI-'2)+2) by A37,A9,A45,A11,A19,A21,JORDAN1A:33; A49: 1 < i by JORDAN1H:49,XXREAL_0:2; then G*(i,j4)`2 = G*(1,j4)`2 by A18,A38,A42,GOBOARD5:1 .= G*(i-'1,j4)`2 by A38,A42,A36,A40,GOBOARD5:1; then A50: G*(i-'1,j4)`2 < p3`2 by A47,A37,A9,A45,A11,A19,A21,A46,A29,A33,JORDAN1A:33 ; p3`1 < G1*(i1,j3)`1 by A12,A23,A27,A5,A26,A28,Th4; then A51: p3`1 < G*(i,j4)`1 by A47,A37,A9,A45,A11,A19,A21,A46,JORDAN1A:33; j4 >= 1+1 by A38,NAT_1:13; then ex c,d be Nat st 2 <= c & c <= len G1 - 1 & 2 <= d & d <= len G1 - 1 & [c,d] in Indices G1 & G*(i-'1,j4) = G1*(c,d) & c = 2 + 2|^(m -'n)*(i-'1-'2) & d = 2 + 2|^(m-'n)*(j4-'2) by A2,A17,A41,A44,GOBRD14:8; then G*(i-'1,j4) in {G1*(ii,jj) where ii,jj is Nat: [ii,jj] in Indices G1}; then G*(i-'1,j4) in Values G1 by MATRIX_0:39; then G*(i-'1,j4)`1 <= G1*(i1-'1,j3)`1 by A48,A46,A49,A18,A38,A42,A12,A32,A23,A25, GOBRD13:14; then A52: G*(i-'1,j4)`1 < p3`1 by A31,XXREAL_0:2; j4+1 > 1+1 by A38,XREAL_1:6; then ex c, d be Nat st 2 <= c & c <= len G1 - 1 & 2 <= d & d <= len G1 - 1 & [c,d] in Indices G1 & G*(i,j4+1) = G1*(c,d) & c = 2 + 2|^(m -'n)*(i-'2) & d = 2 + 2|^(m-'n)*(j4+1-'2) by A2,A15,A8,A39,GOBRD14:8; then G*(i,j4+1) in {G1*(ii,jj) where ii,jj is Nat: [ii,jj] in Indices G1}; then G*(i,j4+1) in Values G1 by MATRIX_0:39; then A53: G1*(i1,j3+1)`2 <= G*(i,j4+1)`2 by A48,A46,A49,A18,A38,A42,A12,A32,A23,A25, GOBRD13:15; A54: j4+1 >= 1 by NAT_1:11; then G*(i,j4+1)`2 = G*(1,j4+1)`2 by A49,A18,A43,GOBOARD5:1 .= G*(i-'1,j4+1)`2 by A36,A40,A43,A54,GOBOARD5:1; then p3`2 < G*(i-'1,j4+1)`2 by A30,A35,A53,XXREAL_0:2; then A55: p3 in Int cell(G,i-'1,j4) by A7,A38,A16,A36,A52,A51,A43,A50,Th4; f is_sequence_on G by A1,JORDAN13:def 1; then Int cell(G,i-'1,j4) misses L~f by A42,A40,JORDAN9:14; then not p3 in L~f by A55,XBOOLE_0:3; then p3 in cell(G,i-'1,j4)\L~f by A55,A14,XBOOLE_0:def 5; then p3 in BDD L~f by A13; then A56: p3 in RightComp Span(C,n) by GOBRD14:37; f1 is_sequence_on G1 by A3,JORDAN13:def 1; then Int cell(G1,i1-'1,j3) misses L~f1 by A25,A24,JORDAN9:14; then A57: not p3 in L~f1 by A28,XBOOLE_0:3; Int cell(G1,i1-'1,j3) c= cell(G1,i1-'1,j3) by TOPS_1:16; then p3 in cell(G1,i1-'1,j3)\L~f1 by A28,A57,XBOOLE_0:def 5; then p3 in BDD L~f1 by A6; then p3 in RightComp Span(C,m) by GOBRD14:37; hence thesis by A56,XBOOLE_0:3; end; theorem Th33: for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G & f is special for i,j be Nat st i <= len G & j <= width G holds Int cell(G,i,j) c= (L~f)` by JORDAN9:14,SUBSET_1:23; theorem Th34: for C be Simple_closed_curve for n,m be Nat st n is_sufficiently_large_for C & n <= m holds L~Span(C,m) c= Cl LeftComp(Span(C,n) ) proof let C be Simple_closed_curve; let i,j be Nat; assume that A1: i is_sufficiently_large_for C and A2: i <= j and A3: not L~Span(C,j) c= Cl LeftComp(Span(C,i)); A4: j is_sufficiently_large_for C by A1,A2,Th28; then A5: Span(C,j) is_sequence_on Gauge(C,j) by JORDAN13:def 1; set G = Gauge(C,j); set f = Span(C,j); consider p be Point of TOP-REAL 2 such that A6: p in L~Span(C,j) and A7: not p in Cl LeftComp(Span(C,i)) by A3; consider i1 be Nat such that A8: 1 <= i1 and A9: i1+1 <= len Span(C,j) and A10: p in LSeg(Span(C,j),i1) by A6,SPPOL_2:13; A11: i1 < len Span(C,j) by A9,NAT_1:13; A12: Span(C,i) is_sequence_on Gauge(C,i) by A1,JORDAN13:def 1; now ex i2,j2 be Nat st 1 <= i2 & i2+1 <= len Gauge(C,i) & 1 <= j2 & j2+1 <= width Gauge(C,i) & left_cell(Span(C,j),i1,G) c= cell(Gauge(C,i),i2 ,j2) proof A13: 1 <= i1+1 by NAT_1:11; then A14: i1+1 in dom f by A9,FINSEQ_3:25; then consider i5,j5 be Nat such that A15: [i5,j5] in Indices Gauge(C,j) and A16: f/.(i1+1) = (Gauge(C,j))*(i5,j5) by A5,GOBOARD1:def 9; A17: 1 <= i5 by A15,MATRIX_0:32; A18: j5 <= width Gauge(C,j) by A15,MATRIX_0:32; A19: i5 <= len Gauge(C,j) by A15,MATRIX_0:32; A20: 1 <= j5 by A15,MATRIX_0:32; A21: i1 in dom f by A8,A11,FINSEQ_3:25; then consider i4,j4 be Nat such that A22: [i4,j4] in Indices Gauge(C,j) and A23: f/.i1 = (Gauge(C,j))*(i4,j4) by A5,GOBOARD1:def 9; A24: 1 <= i4 by A22,MATRIX_0:32; |.i4-i5.|+|.j4-j5.| = 1 by A5,A21,A22,A23,A14,A15,A16,GOBOARD1:def 9; then A25: |.i4-i5.|=1 & j4=j5 or |.j4-j5.|=1 & i4=i5 by SEQM_3:42; A26: 1 <= j4 by A22,MATRIX_0:32; left_cell(f,i1,G) = left_cell(f,i1,G); then A27: i4 = i5 & j4+1 = j5 & left_cell(f,i1,G) = cell(G,i4-'1,j4) or i4+1 = i5 & j4 = j5 & left_cell(f,i1,G) = cell(G,i4,j4) or i4 = i5+1 & j4 = j5 & left_cell(f,i1,G) = cell(G,i5,j5-'1) or i4 = i5 & j4 = j5+1 & left_cell(f,i1,G) = cell(G,i4,j5) by A5,A8,A9,A22,A23,A15,A16,GOBRD13:def 3; A28: j4 <= width Gauge(C,j) by A22,MATRIX_0:32; A29: i4 <= len Gauge(C,j) by A22,MATRIX_0:32; per cases by A25,SEQM_3:41; suppose A30: i4 = i5 & j4+1 = j5; 1 < i4 by A1,A2,A8,A11,A22,A23,Th22,Th28; then 1+1 <= i4 by NAT_1:13; then A31: 1 <= i4-'1 by JORDAN5B:2; i4-'1+1 = i4 by A24,XREAL_1:235; hence thesis by A2,A29,A26,A18,A27,A30,A31,JORDAN1H:38; end; suppose A32: i4+1 = i5 & j4 = j5; j4 < width Gauge(C,j) by A1,A2,A8,A11,A22,A23,Th25,Th28; then j4+1 <= width Gauge(C,j) by NAT_1:13; hence thesis by A2,A24,A26,A19,A27,A32,JORDAN1H:38; end; suppose A33: i4 = i5+1 & j4 = j5; 1 < j5 by A1,A2,A9,A13,A15,A16,Th24,Th28; then 1+1 <= j5 by NAT_1:13; then A34: 1 <= j5-'1 by JORDAN5B:2; j5-'1+1 = j5 by A20,XREAL_1:235; hence thesis by A2,A29,A17,A18,A27,A33,A34,JORDAN1H:38; end; suppose A35: i4 = i5 & j4 = j5+1; i4 < len Gauge(C,j) by A1,A2,A8,A11,A22,A23,Th23,Th28; then i4+1 <= len Gauge(C,j) by NAT_1:13; hence thesis by A2,A24,A28,A20,A27,A35,JORDAN1H:38; end; end; then consider i2,j2 be Nat such that 1 <= i2 and A36: i2+1 <= len Gauge(C,i) and 1 <= j2 and A37: j2+1 <= width Gauge(C,i) and A38: left_cell(Span(C,j),i1,G) c= cell(Gauge(C,i),i2,j2); A39: j2 < width Gauge(C,i) by A37,NAT_1:13; A40: LeftComp Span(C,i) is_a_component_of (L~Span(C,i))` by GOBOARD9:def 1; A41: Cl RightComp Span(C,i) \/ LeftComp Span(C,i) = L~Span(C,i) \/ RightComp Span(C,i) \/ LeftComp Span(C,i) by GOBRD14:21 .= the carrier of TOP-REAL 2 by GOBRD14:15; assume not left_cell(Span(C,j),i1,G) c= Cl RightComp Span(C,i); then not cell(Gauge(C,i),i2,j2) c= Cl RightComp Span(C,i) by A38; then A42: cell(Gauge(C,i),i2,j2) meets LeftComp Span(C,i) by A41,XBOOLE_1:73; A43: i2< len Gauge(C,i) by A36,NAT_1:13; then cell(Gauge(C,i),i2,j2) = Cl Int cell(Gauge(C,i),i2,j2) by A39, GOBRD11:35; then A44: Int cell(Gauge(C,i),i2,j2) meets LeftComp Span(C,i) by A42,TSEP_1:36; A45: Int left_cell(Span(C,j),i1,G) c= Int cell(Gauge(C,i),i2,j2) by A38, TOPS_1:19; A46: Int cell(Gauge(C,i),i2,j2) is convex by A43,A39,GOBOARD9:17; Int cell(Gauge(C,i),i2,j2) c= (L~Span(C,i))` by A12,A43,A39,Th33; then Int cell(Gauge(C,i),i2,j2) c= LeftComp Span(C,i) by A44,A40,A46,GOBOARD9:4; then Int left_cell(Span(C,j),i1,G) c= LeftComp Span(C,i) by A45; then Cl Int left_cell(Span(C,j),i1,G) c= Cl LeftComp Span(C,i) by PRE_TOPC:19; then A47: left_cell(Span(C,j),i1,G) c= Cl LeftComp Span(C,i) by A5,A8,A9,JORDAN9:11; LSeg(Span(C,j),i1) c= left_cell(Span(C,j),i1,G) by A5,A8,A9,JORDAN1H:20; then LSeg(Span(C,j),i1) c= Cl LeftComp Span(C,i) by A47; hence contradiction by A7,A10; end; then A48: C meets Cl RightComp Span(C,i) by A4,A8,A9,Th7,XBOOLE_1:63; A49: Cl RightComp Span(C,i) = RightComp Span(C,i) \/ L~Span(C,i) by GOBRD14:21; C misses L~Span(C,i) by A1,Th8; then A50: C meets RightComp Span(C,i) by A48,A49,XBOOLE_1:70; C meets C; then A51: C meets LeftComp Span(C,i) by A1,Th11,XBOOLE_1:63; reconsider D = (L~Span(C,i))` as Subset of TOP-REAL 2; D = RightComp Span(C,i) \/ LeftComp Span(C,i) by GOBRD12:10; then A52: LeftComp Span(C,i) c= D by XBOOLE_1:7; C c= LeftComp Span(C,i) by A1,Th11; then A53: C c= D by A52; A54: LeftComp Span(C,i) is_a_component_of D by GOBOARD9:def 1; RightComp Span(C,i) is_a_component_of D by GOBOARD9:def 2; hence contradiction by A50,A53,A54,A51,JORDAN9:1,SPRECT_4:6; end; theorem Th35: for C be Simple_closed_curve for n,m be Nat st n is_sufficiently_large_for C & n <= m holds RightComp(Span(C,n)) c= RightComp( Span(C,m)) proof let C be Simple_closed_curve; let n,m be Nat; assume that A1: n is_sufficiently_large_for C and A2: n <= m; A3: L~Span(C,n) misses RightComp(Span(C,n)) by SPRECT_3:25; A4: RightComp Span(C,n) misses LeftComp Span(C,n) by GOBRD14:14; Cl LeftComp Span(C,n) = (LeftComp Span(C,n)) \/ L~Span(C,n) by GOBRD14:22; then Cl LeftComp(Span(C,n)) misses RightComp(Span(C,n)) by A3,A4,XBOOLE_1:70; then L~Span(C,m) misses RightComp(Span(C,n)) by A1,A2,Th34,XBOOLE_1:63; then A5: RightComp(Span(C,n)) c= (L~Span(C,m))` by SUBSET_1:23; A6: RightComp(Span(C,m)) is_a_component_of (L~Span(C,m))` by GOBOARD9:def 2; RightComp(Span(C,n)) meets RightComp(Span(C,m)) by A1,A2,Th32; hence thesis by A6,A5,GOBOARD9:4; end; theorem for C be Simple_closed_curve for n,m be Nat st n is_sufficiently_large_for C & n <= m holds LeftComp(Span(C,m)) c= LeftComp(Span (C,n)) proof let C be Simple_closed_curve; let n,m be Nat; assume that A1: n is_sufficiently_large_for C and A2: n <= m; A3: (Cl RightComp(Span(C,n)))` = LeftComp(Span(C,n)) by JORDAN1H:43; A4: (Cl RightComp(Span(C,m)))` = LeftComp(Span(C,m)) by JORDAN1H:43; Cl RightComp(Span(C,n)) c= Cl RightComp(Span(C,m)) by A1,A2,Th35,PRE_TOPC:19; hence thesis by A3,A4,SUBSET_1:12; end;