:: Some Remarks on Finite Sequences on Go-boards :: by Adam Naumowicz :: :: Received August 29, 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, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD1, RLTOPSP1, RELAT_1, XBOOLE_0, TOPREAL1, MATRIX_1, XXREAL_0, MCART_1, RCOMP_1, PSCOMP_1, PRE_TOPC, TREES_1, TARSKI, ARYTM_3, PARTFUN1, COMPLEX1, ARYTM_1, CARD_1, SPPOL_1, JORDAN1E, JORDAN9, FINSEQ_6, FINSEQ_5, FINSEQ_4, JORDAN6, TOPREAL2, RELAT_2, JORDAN8, ORDINAL4, FUNCT_1, NAT_1, RFINSEQ, JORDAN1A, SEQ_4; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQ_6, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, RFINSEQ, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8, JORDAN9, JORDAN1A, JORDAN1E; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, PSCOMP_1; registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_6, STRUCT_0, SPPOL_2, SPRECT_1, SPRECT_2, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, FUNCT_1, EUCLID, PSCOMP_1, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin reserve i,j,k,m,n for Nat, f for FinSequence of the carrier of TOP-REAL 2, G for Go-board; theorem :: JORDAN1F:1 f is_sequence_on G & LSeg(G*(i,j),G*(i,k)) meets L~f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(i, n)`2 = lower_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f)); theorem :: JORDAN1F:2 f is_sequence_on G & LSeg(G*(i,j),G*(i,k)) meets L~f & [i,j] in Indices G & [i,k] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(i, n)`2 = upper_bound(proj2.:(LSeg(G*(i,j),G*(i,k)) /\ L~f)); theorem :: JORDAN1F:3 f is_sequence_on G & LSeg(G*(j,i),G*(k,i)) meets L~f & [j,i] in Indices G & [k,i] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(n, i)`1 = lower_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f)); theorem :: JORDAN1F:4 f is_sequence_on G & LSeg(G*(j,i),G*(k,i)) meets L~f & [j,i] in Indices G & [k,i] in Indices G & j <= k implies ex n st j <= n & n <= k & G*(n, i)`1 = upper_bound(proj1.:(LSeg(G*(j,i),G*(k,i)) /\ L~f)); theorem :: JORDAN1F:5 for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/.1 = W-min(L~Cage(C, n)); theorem :: JORDAN1F:6 for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds Lower_Seq(C,n)/.1 = E-max L~Cage(C,n); theorem :: JORDAN1F:7 for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n)/. len Upper_Seq(C,n) = E-max(L~Cage(C,n)); theorem :: JORDAN1F:8 for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = W-min L~ Cage(C,n); theorem :: JORDAN1F:9 for C being compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds L~Upper_Seq(C,n) = Upper_Arc L~Cage (C,n) & L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) or L~Upper_Seq(C,n) = Lower_Arc L~Cage(C,n) & L~Lower_Seq(C,n) = Upper_Arc L~Cage(C,n); reserve C for compact non vertical non horizontal non empty being_simple_closed_curve Subset of TOP-REAL 2, p for Point of TOP-REAL 2, i1, j1,i2,j2 for Nat; theorem :: JORDAN1F:10 for C being connected compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Upper_Seq(C,n) is_sequence_on Gauge(C,n); theorem :: JORDAN1F:11 :: symmetric to JORDAN8:9 for f being FinSequence of TOP-REAL 2 st f is_sequence_on G & ( ex i,j st [i,j] in Indices G & p = G*(i,j)) & (for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G*(i1,j1) & f/.1 = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1) holds <*p*>^f is_sequence_on G; theorem :: JORDAN1F:12 for C being connected compact non vertical non horizontal Subset of TOP-REAL 2 for n being Nat holds Lower_Seq(C,n) is_sequence_on Gauge(C,n); theorem :: JORDAN1F:13 p`1 = (W-bound C + E-bound C)/2 & p`2 = lower_bound(proj2.:(LSeg(Gauge(C,1)*( Center Gauge(C,1),1), Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1))) /\ Upper_Arc L~Cage(C,i+1))) implies ex j st 1 <= j & j <= width Gauge(C,i+1) & p = Gauge(C,i+1)*(Center Gauge(C,i+1),j);