:: More on External Approximation of a Continuum :: by Andrzej Trybulec :: :: Received October 7, 2001 :: Copyright (c) 2001-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, REAL_1, RCOMP_1, SPPOL_1, EUCLID, GOBOARD1, PRE_TOPC, SETFAM_1, XBOOLE_0, RELAT_1, FINSEQ_1, TARSKI, FUNCOP_1, FUNCT_1, FUNCT_6, RLTOPSP1, PCOMPS_1, XXREAL_0, CARD_1, METRIC_1, ARYTM_3, ARYTM_1, FINSEQ_2, COMPLEX1, ZFMISC_1, RELAT_2, PARTFUN1, ORDERS_1, FINSET_1, PRE_POLY, ORDINAL2, GOBOARD2, NAT_1, MCART_1, GOBRD13, CARD_3, MATRIX_1, TREES_1, INCSP_1, STRUCT_0, GOBOARD5, CONNSP_1, TOPREAL1, GOBOARD9, TOPS_1, JORDAN3, RFINSEQ, FINSEQ_5, INT_1, NEWTON, JORDAN8, PSCOMP_1, JORDAN2C, FINSEQ_6, SPRECT_2, JORDAN9, JORDAN1H, CONVEX1, XXREAL_2, FUNCT_7; notations TARSKI, XBOOLE_0, SETFAM_1, ZFMISC_1, SUBSET_1, FINSEQ_6, GOBOARD5, ORDERS_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, FUNCT_1, NAT_1, INT_1, NAT_D, RELAT_1, RELAT_2, RELSET_1, PARTFUN1, NEWTON, FINSET_1, FINSEQ_1, SEQM_3, RVSUM_1, STRUCT_0, FUNCT_6, CARD_3, FUNCOP_1, FINSEQ_2, FINSEQ_5, RFINSEQ, MATRIX_0, MATRIX_1, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, SPRECT_2, TOPREAL1, GOBOARD1, GOBOARD2, JORDAN2C, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN8, GOBRD13, JORDAN9, PRE_POLY; constructors REAL_1, NEWTON, RFINSEQ, NAT_D, WSIERP_1, TOPS_1, CONNSP_1, TOPREAL4, GOBOARD2, PSCOMP_1, TRIANG_1, GOBOARD9, SPRECT_1, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, BINOP_2, RELSET_1, FUNCSDOM, CONVEX1, PCOMPS_1, SEQ_4, DOMAIN_1; registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_6, GENEALG1, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_2, GOBOARD9, WAYBEL_2, SPRECT_1, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8, MATRIX_0, VALUED_0, RELSET_1, RLTOPSP1, PRE_POLY, SEQM_3, CARD_1, JORDAN1, JORDAN2C, NEWTON; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve m,k,j,j1,i,i1,i2,n for Nat, r,s for Real, C for compact non vertical non horizontal Subset of TOP-REAL 2, G for Go-board, p for Point of TOP-REAL 2; registration let D be non empty with_non-empty_element set; cluster non empty non-empty for FinSequence of D*; end; registration let F be non-empty Function-yielding Function; cluster rngs F -> non-empty; end; theorem :: JORDAN1H:1 for p,q being Point of TOP-REAL 2 st p <> q holds p in Cl(LSeg(p, q) \ {p,q}) ; theorem :: JORDAN1H:2 for p,q being Point of TOP-REAL 2 st p <> q holds Cl(LSeg(p,q) \ {p,q}) = LSeg(p,q); theorem :: JORDAN1H:3 for S being Subset of TOP-REAL 2, p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) \ {p,q} c= S holds LSeg(p,q) c= Cl S; begin :: Transforming Finite Sets to Finite Sequences definition func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1 {[r,s] : r <= s }; end; theorem :: JORDAN1H:4 [r,s] in RealOrd implies r <= s; theorem :: JORDAN1H:5 field RealOrd = REAL; registration cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order; end; theorem :: JORDAN1H:6 RealOrd linearly_orders REAL; theorem :: JORDAN1H:7 for A being finite Subset of REAL holds SgmX(RealOrd,A) is increasing; theorem :: JORDAN1H:8 for f being FinSequence of REAL, A being finite Subset of REAL st A = rng f holds SgmX(RealOrd,A) = Incr f; registration let A be finite Subset of REAL; cluster SgmX(RealOrd,A) -> increasing; end; theorem :: JORDAN1H:9 for X being non empty set, A being finite Subset of X, R be being_linear-order Order of X holds len SgmX(R,A) = card A; begin :: On the construction of go boards theorem :: JORDAN1H:10 for f being FinSequence of TOP-REAL 2 holds X_axis f = proj1*f; theorem :: JORDAN1H:11 for f being FinSequence of TOP-REAL 2 holds Y_axis f = proj2*f; definition let D be non empty set; let M be FinSequence of D*; redefine func Values M -> Subset of D; end; registration let D be non empty with_non-empty_elements set; let M be non empty non-empty FinSequence of D*; cluster Values M -> non empty; end; theorem :: JORDAN1H:12 for D being non empty set, M being (Matrix of D), i st i in Seg width M holds rng Col(M,i) c= Values M; theorem :: JORDAN1H:13 for D being non empty set, M being (Matrix of D), i st i in dom M holds rng Line(M,i) c= Values M; theorem :: JORDAN1H:14 for G being X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2 holds len G <= card(proj1.:Values G); theorem :: JORDAN1H:15 for G being X_equal-in-line Matrix of TOP-REAL 2 holds card( proj1.:Values G) <= len G; theorem :: JORDAN1H:16 for G being X_equal-in-line X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2 holds len G = card(proj1.:Values G); theorem :: JORDAN1H:17 for G being Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2 holds width G <= card(proj2.:Values G); theorem :: JORDAN1H:18 for G being Y_equal-in-column non empty-yielding Matrix of TOP-REAL 2 holds card(proj2.:Values G) <= width G; theorem :: JORDAN1H:19 for G being Y_equal-in-column Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2 holds width G = card(proj2.:Values G); begin :: On go boards theorem :: JORDAN1H:20 for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for k be Nat st 1 <= k & k+1 <= len f holds LSeg(f, k) c= left_cell(f,k,G); theorem :: JORDAN1H:21 for f being standard special_circular_sequence st 1 <= k & k+1 <= len f holds left_cell(f,k,GoB f) = left_cell(f,k); theorem :: JORDAN1H:22 for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for k be Nat st 1 <= k & k+1 <= len f holds LSeg(f, k) c= right_cell(f,k,G); theorem :: JORDAN1H:23 for f being standard special_circular_sequence st 1 <= k & k+1 <= len f holds right_cell(f,k,GoB f) = right_cell(f,k); theorem :: JORDAN1H:24 for P being Subset of TOP-REAL 2, f being non constant standard special_circular_sequence st P is_a_component_of (L~f)` holds P = RightComp f or P = LeftComp f; theorem :: JORDAN1H:25 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 Int right_cell(f,k,G) c= RightComp f & Int left_cell(f,k,G) c= LeftComp f; theorem :: JORDAN1H:26 for i1,j1,i2,j2 being Nat, G being Go-board st [i1,j1 ] in Indices G & [i2,j2] in Indices G & G*(i1,j1) = G*(i2,j2) holds i1 = i2 & j1 = j2; theorem :: JORDAN1H:27 for f being FinSequence of TOP-REAL 2, M being Go-board holds f is_sequence_on M implies mid(f,i1,i2) is_sequence_on M; registration cluster -> non empty non-empty for Go-board; end; theorem :: JORDAN1H:28 for G being Go-board st 1 <= i & i <= len G holds SgmX(RealOrd, proj1.:Values G).i = G*(i,1)`1; theorem :: JORDAN1H:29 for G being Go-board st 1 <= j & j <= width G holds SgmX(RealOrd , proj2.:Values G).j = G*(1,j)`2; theorem :: JORDAN1H:30 for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [1,i] in Indices G & G*(1,i) in rng f ) & (ex i st [len G,i] in Indices G & G*(len G,i) in rng f) holds proj1.:rng f = proj1.:Values G; theorem :: JORDAN1H:31 for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [i,1] in Indices G & G*(i,1) in rng f ) & (ex i st [i,width G] in Indices G & G*(i,width G) in rng f) holds proj2.: rng f = proj2.:Values G; registration let G be Go-board; cluster Values G -> non empty; end; theorem :: JORDAN1H:32 for G being Go-board holds G = GoB(SgmX(RealOrd, proj1.:Values G ), SgmX(RealOrd,proj2.:Values G)); theorem :: JORDAN1H:33 for f being non empty FinSequence of TOP-REAL 2, G being Go-board st proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G holds G = GoB f; theorem :: JORDAN1H:34 for f being non empty FinSequence of TOP-REAL 2, G being Go-board st f is_sequence_on G & (ex i st [1,i] in Indices G & G*(1,i) in rng f ) & (ex i st [i,1] in Indices G & G*(i,1) in rng f) & (ex i st [len G,i] in Indices G & G*(len G,i) in rng f) & (ex i st [i,width G] in Indices G & G*(i, width G) in rng f) holds G = GoB f; begin :: More about gauges theorem :: JORDAN1H:35 1 <= i implies [\ (i-2)/2|^(n-'m)+2 /] is Element of NAT; theorem :: JORDAN1H:36 m <= n & 1 <= i & i+1 <= len Gauge(C,n) implies 1 <= [\ (i-2)/2 |^(n-'m)+2 /] & [\ (i-2)/2|^(n-'m)+2 /]+1 <= len Gauge(C,m); theorem :: JORDAN1H:37 m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n) implies ex i1,j1 st i1 = [\ (i-2)/2|^(n-'m)+2 /] & j1 = [\ (j-2)/2|^ (n-'m)+2 /] & cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1); theorem :: JORDAN1H:38 m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n) implies ex i1,j1 st 1 <= i1 & i1+1 <= len Gauge(C,m) & 1 <= j1 & j1+ 1 <= width Gauge(C,m) & cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1); theorem :: JORDAN1H:39 for P being Subset of TOP-REAL2 st P is bounded holds UBD P is not bounded; theorem :: JORDAN1H:40 for f being non constant standard special_circular_sequence st Rotate(f,p) is clockwise_oriented holds f is clockwise_oriented; theorem :: JORDAN1H:41 for f being non constant standard special_circular_sequence st LeftComp f = UBD L~f holds f is clockwise_oriented; begin :: More about cages theorem :: JORDAN1H:42 for f being non constant standard special_circular_sequence holds (Cl LeftComp(f))` = RightComp f; theorem :: JORDAN1H:43 for f being non constant standard special_circular_sequence holds (Cl RightComp(f))` = LeftComp f; theorem :: JORDAN1H:44 C is connected implies GoB Cage(C,n) = Gauge(C,n); theorem :: JORDAN1H:45 C is connected implies N-min C in right_cell(Cage(C,n),1); theorem :: JORDAN1H:46 C is connected & i <= j implies L~Cage(C,j) c= Cl RightComp(Cage (C,i)); theorem :: JORDAN1H:47 C is connected & i <= j implies LeftComp(Cage(C,i)) c= LeftComp( Cage(C,j)); theorem :: JORDAN1H:48 C is connected & i <= j implies RightComp(Cage(C,j)) c= RightComp(Cage (C, i ) ); begin :: Preparing the Internal Approximation definition let C,n; func X-SpanStart(C,n) -> Nat equals :: JORDAN1H:def 2 2|^(n-'1) + 2; end; theorem :: JORDAN1H:49 2 < X-SpanStart(C,n) & X-SpanStart(C,n) < len Gauge(C,n); theorem :: JORDAN1H:50 1 <= X-SpanStart(C,n)-'1 & X-SpanStart(C,n)-'1 < len Gauge(C,n); definition let C,n; pred n is_sufficiently_large_for C means :: JORDAN1H:def 3 ex j st j < width Gauge(C,n) & cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C; end; theorem :: JORDAN1H:51 n is_sufficiently_large_for C implies n >= 1; theorem :: JORDAN1H:52 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st left_cell(f,(len f)-'1 ,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge (C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+ 1) holds [i1-'1,j1+1] in Indices Gauge(C,n); theorem :: JORDAN1H:53 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st left_cell(f,(len f)-'1 ,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge (C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1, j1) holds [i1+1,j1+1] in Indices Gauge(C,n); theorem :: JORDAN1H:54 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st left_cell(f,(len f)-'1 ,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*( i2,j1) holds [i2,j1-'1] in Indices Gauge(C,n); theorem :: JORDAN1H:55 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st left_cell(f,(len f)-'1 ,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*( i1,j2) holds [i1+1,j2] in Indices Gauge(C,n); theorem :: JORDAN1H:56 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*( i1,j1+1) holds [i1,j1+2] in Indices Gauge(C,n); theorem :: JORDAN1H:57 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*( i1+1,j1) holds [i1+2,j1] in Indices Gauge(C,n); theorem :: JORDAN1H:58 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)* (i2,j1) holds [i2-'1,j1] in Indices Gauge(C,n); theorem :: JORDAN1H:59 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)* (i1,j2) holds [i1,j2-'1] in Indices Gauge(C,n); theorem :: JORDAN1H:60 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_right_cell(f,( len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1 ) = Gauge(C,n)*(i1,j1) & [i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n )*(i1,j1+1) holds [i1+1,j1+1] in Indices Gauge(C,n); theorem :: JORDAN1H:61 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j1 being Nat st front_right_cell(f,( len f)-'1,Gauge(C,n)) meets C & [i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1 ) = Gauge(C,n)*(i1,j1) & [i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n )*(i1+1,j1) holds [i1+1,j1-'1] in Indices Gauge(C,n); theorem :: JORDAN1H:62 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for j1,i2 being Nat st front_right_cell(f,( len f)-'1,Gauge(C,n)) meets C & [i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) & [i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge( C,n)*(i2,j1) holds [i2,j1+1] in Indices Gauge(C,n); theorem :: JORDAN1H:63 for C being compact non vertical non horizontal non empty Subset of TOP-REAL 2 for n for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) & len f > 1 for i1,j2 being Nat st front_right_cell(f,( len f)-'1,Gauge(C,n)) meets C & [i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) & [i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge( C,n)*(i1,j2) holds [i1-'1,j2] in Indices Gauge(C,n);