:: Properties of the Internal Approximation of {J}ordan's Curve :: by Robert Milewski :: :: Received June 27, 2002 :: Copyright (c) 2002-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, 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; begin theorem :: JORDAN14:1 for f be non constant standard special_circular_sequence holds BDD L~f = RightComp f or BDD L~f = LeftComp f; theorem :: JORDAN14:2 for f be non constant standard special_circular_sequence holds UBD L~f = RightComp f or UBD L~f = LeftComp f; theorem :: JORDAN14:3 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; theorem :: JORDAN14:4 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; theorem :: JORDAN14:5 for f be non constant standard special_circular_sequence holds BDD L~f is connected; registration let f be non constant standard special_circular_sequence; cluster BDD L~f -> connected; end; definition let C be Simple_closed_curve; let n be Nat; func SpanStart(C,n) -> Point of TOP-REAL 2 equals :: JORDAN14:def 1 Gauge(C,n)*(X-SpanStart(C, n),Y-SpanStart(C,n)); end; theorem :: JORDAN14:6 for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds SpanStart(C,n) in BDD C; theorem :: JORDAN14:7 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; theorem :: JORDAN14:8 for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C misses L~Span(C,n); registration let C be Simple_closed_curve; let n be Nat; cluster Cl RightComp Span(C,n) -> compact; end; theorem :: JORDAN14:9 for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C meets LeftComp Span(C,n); theorem :: JORDAN14:10 for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C misses RightComp Span(C,n); theorem :: JORDAN14:11 for C be Simple_closed_curve for n be Nat st n is_sufficiently_large_for C holds C c= LeftComp Span(C,n); theorem :: JORDAN14:12 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); theorem :: JORDAN14:13 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; theorem :: JORDAN14:14 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); theorem :: JORDAN14:15 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; theorem :: JORDAN14:16 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); theorem :: JORDAN14:17 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); theorem :: JORDAN14:18 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); theorem :: JORDAN14:19 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); theorem :: JORDAN14:20 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); theorem :: JORDAN14:21 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; theorem :: JORDAN14:22 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; theorem :: JORDAN14:23 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); theorem :: JORDAN14:24 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; theorem :: JORDAN14:25 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); theorem :: JORDAN14:26 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); theorem :: JORDAN14:27 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; theorem :: JORDAN14:28 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; theorem :: JORDAN14:29 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; theorem :: JORDAN14:30 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); theorem :: JORDAN14:31 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); theorem :: JORDAN14:32 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); theorem :: JORDAN14:33 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)`; theorem :: JORDAN14:34 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) ); theorem :: JORDAN14:35 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)); theorem :: JORDAN14:36 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));