:: Upper and Lower Sequence on the Cage, Upper and Lower Arcs :: by Robert Milewski :: :: Received April 5, 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, SUBSET_1, GOBOARD1, XXREAL_0, TREES_1, ARYTM_3, FINSEQ_1, RELAT_1, MCART_1, XBOOLE_0, GRAPH_2, ORDINAL4, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, TOPREAL1, JORDAN9, FINSEQ_5, PSCOMP_1, PARTFUN1, TARSKI, CARD_1, FINSEQ_4, PRE_TOPC, RLTOPSP1, ARYTM_1, JORDAN1E, FINSEQ_6, RFINSEQ, JORDAN3, FUNCT_1, GOBOARD5, GOBOARD9, CONNSP_1, TOPREAL2, JORDAN8, SPPOL_2, NAT_1, GROUP_2, MATRIX_1, SPRECT_2, ZFMISC_1, JORDAN6, GOBOARD2, JORDAN2C, JORDAN1A, XXREAL_2; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, TOPS_1, CONNSP_1, MATRIX_1, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, RELSET_1, CONVEX1, DOMAIN_1; registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1G, CARD_1, FUNCT_1, EUCLID, JORDAN2C, INT_1, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve n for Nat; theorem :: JORDAN1J:1 for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds G*(i1,j1)`1 < G*(i2,j2)`1; theorem :: JORDAN1J:2 for G be Go-board for i1,i2,j1,j2 be Nat st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds G *(i1,j1)`2 < G*(i2,j2)`2; registration let f be non empty FinSequence; let g be FinSequence; cluster f^'g -> non empty; end; theorem :: JORDAN1J:3 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:E-max L~Cage(C,n)) /\ L~ (Cage(C,n):-E-max L~Cage(C,n)) = {N-min L~Cage(C,n),E-max L~Cage(C,n)}; theorem :: JORDAN1J:4 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n)):-W-min L~ Cage(C,n); theorem :: JORDAN1J:5 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds W-min L~Cage(C,n) in rng Upper_Seq(C,n) & W-min L~Cage(C,n) in L~ Upper_Seq(C,n); theorem :: JORDAN1J:6 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-max L~Cage(C,n) in rng Upper_Seq(C,n) & W-max L~Cage(C,n) in L~Upper_Seq(C,n); theorem :: JORDAN1J:7 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds N-min L~Cage(C,n) in rng Upper_Seq(C,n) & N-min L~Cage(C,n) in L~Upper_Seq(C,n); theorem :: JORDAN1J:8 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds N-max L~Cage(C,n) in rng Upper_Seq(C,n) & N-max L~Cage(C,n) in L~Upper_Seq(C,n); theorem :: JORDAN1J:9 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-max L~Cage(C,n) in rng Upper_Seq(C,n) & E-max L~Cage(C,n) in L~ Upper_Seq(C,n); theorem :: JORDAN1J:10 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-max L~Cage(C,n) in rng Lower_Seq(C,n) & E-max L~Cage(C,n) in L~ Lower_Seq(C,n); theorem :: JORDAN1J:11 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds E-min L~Cage(C,n) in rng Lower_Seq(C,n) & E-min L~Cage(C,n) in L~ Lower_Seq(C,n); theorem :: JORDAN1J:12 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds S-max L~Cage(C,n) in rng Lower_Seq(C,n) & S-max L~Cage(C,n) in L~ Lower_Seq(C,n); theorem :: JORDAN1J:13 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds S-min L~Cage(C,n) in rng Lower_Seq(C,n) & S-min L~Cage(C,n) in L~ Lower_Seq(C,n); theorem :: JORDAN1J:14 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds W-min L~Cage(C,n) in rng Lower_Seq(C,n) & W-min L~Cage(C,n) in L~ Lower_Seq(C,n); theorem :: JORDAN1J:15 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & N-min Y in X holds N-min X = N-min Y; theorem :: JORDAN1J:16 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & N-max Y in X holds N-max X = N-max Y; theorem :: JORDAN1J:17 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & E-min Y in X holds E-min X = E-min Y; theorem :: JORDAN1J:18 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & E-max Y in X holds E-max X = E-max Y; theorem :: JORDAN1J:19 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & S-min Y in X holds S-min X = S-min Y; theorem :: JORDAN1J:20 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & S-max Y in X holds S-max X = S-max Y; theorem :: JORDAN1J:21 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & W-min Y in X holds W-min X = W-min Y; theorem :: JORDAN1J:22 for X,Y be non empty compact Subset of TOP-REAL 2 st X c= Y & W-max Y in X holds W-max X = W-max Y; theorem :: JORDAN1J:23 for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X <= N-bound Y holds N-bound (X\/Y) = N-bound Y; theorem :: JORDAN1J:24 for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X <= E-bound Y holds E-bound (X\/Y) = E-bound Y; theorem :: JORDAN1J:25 for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X <= S-bound Y holds S-bound (X\/Y) = S-bound X; theorem :: JORDAN1J:26 for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X <= W-bound Y holds W-bound (X\/Y) = W-bound X; theorem :: JORDAN1J:27 for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X < N-bound Y holds N-min (X\/Y) = N-min Y; theorem :: JORDAN1J:28 for X,Y be non empty compact Subset of TOP-REAL 2 st N-bound X < N-bound Y holds N-max (X\/Y) = N-max Y; theorem :: JORDAN1J:29 for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X < E-bound Y holds E-min (X\/Y) = E-min Y; theorem :: JORDAN1J:30 for X,Y be non empty compact Subset of TOP-REAL 2 st E-bound X < E-bound Y holds E-max (X\/Y) = E-max Y; theorem :: JORDAN1J:31 for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X < S-bound Y holds S-min (X\/Y) = S-min X; theorem :: JORDAN1J:32 for X,Y be non empty compact Subset of TOP-REAL 2 st S-bound X < S-bound Y holds S-max (X\/Y) = S-max X; theorem :: JORDAN1J:33 for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X < W-bound Y holds W-min (X\/Y) = W-min X; theorem :: JORDAN1J:34 for X,Y be non empty compact Subset of TOP-REAL 2 st W-bound X < W-bound Y holds W-max (X\/Y) = W-max X; theorem :: JORDAN1J:35 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is being_S-Seq & p in L~f holds L_Cut(f,p)/.len L_Cut(f,p) = f/.len f; theorem :: JORDAN1J:36 for f be non constant standard special_circular_sequence for p,q be Point of TOP-REAL 2 for g be connected Subset of TOP-REAL 2 st p in RightComp f & q in LeftComp f & p in g & q in g holds g meets L~f; registration cluster non constant standard s.c.c. for being_S-Seq FinSequence of TOP-REAL 2; end; theorem :: JORDAN1J:37 for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in rng f holds L_Cut(f,p) = mid(f,p..f,len f); theorem :: JORDAN1J:38 for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on M for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) is_sequence_on M; theorem :: JORDAN1J:39 for M be Go-board for f be S-Sequence_in_R2 st f is_sequence_on M for p be Point of TOP-REAL 2 st p in rng f holds L_Cut(f,p) is_sequence_on M; theorem :: JORDAN1J:40 for G be Go-board for f be FinSequence of TOP-REAL 2 st f is_sequence_on G for i,j be Nat st 1 <= i & i <= len G & 1 <= j & j <= width G holds G*(i,j) in L~f implies G*(i,j) in rng f; theorem :: JORDAN1J:41 for f be S-Sequence_in_R2 for g be FinSequence of TOP-REAL 2 holds g is unfolded s.n.c. one-to-one & L~f /\ L~g = {f/.1} & f/.1 = g/.len g & (for i be Nat st 1<=i & i+2 <= len f holds LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {}) & (for i be Nat st 2<=i & i+1 <= len g holds LSeg(g,i) /\ LSeg (f/.len f,g/.1) = {}) implies f^g is s.c.c.; theorem :: JORDAN1J:42 for C be compact non vertical non horizontal non empty Subset of TOP-REAL 2 ex i be Nat st 1 <= i & i+1 <= len Gauge(C,n) & W-min C in cell(Gauge(C,n),1,i) & W-min C <> Gauge(C,n)*(2,i); theorem :: JORDAN1J:43 for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in L~f & f.len f in L~R_Cut(f,p) holds f.len f = p; theorem :: JORDAN1J:44 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 holds R_Cut (f,p) <> {}; theorem :: JORDAN1J:45 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p)/.(len R_Cut(f,p)) = p; theorem :: JORDAN1J:46 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Upper_Seq(C,n) & p`1 = E-bound L~Cage(C,n) implies p = E-max L~Cage(C,n); theorem :: JORDAN1J:47 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for p be Point of TOP-REAL 2 holds p in L~Lower_Seq(C,n) & p`1 = W-bound L~Cage(C,n) implies p = W-min L~Cage(C,n); theorem :: JORDAN1J:48 for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be Nat holds 1 <= k & k < len f & f^g is_sequence_on G implies left_cell(f^g,k,G) = left_cell(f,k,G) & right_cell(f^g,k,G) = right_cell(f,k,G) ; theorem :: JORDAN1J:49 for D be set for f,g be FinSequence of D for i be Nat st i <= len f holds (f^'g)|i = f|i; theorem :: JORDAN1J:50 for D be set for f,g be FinSequence of D holds (f^'g)|(len f) = f; theorem :: JORDAN1J:51 for G be Go-board for f,g be FinSequence of TOP-REAL 2 for k be Nat holds 1 <= k & k < len f & f^'g is_sequence_on G implies left_cell(f^'g,k,G) = left_cell(f,k,G) & right_cell(f^'g,k,G) = right_cell(f,k, G); theorem :: JORDAN1J:52 for G be Go-board for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f is_sequence_on G & p in rng f holds left_cell(R_Cut(f,p),k,G) = left_cell(f,k,G) & right_cell( R_Cut(f,p),k,G) = right_cell(f,k,G); theorem :: JORDAN1J:53 for G be Go-board for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 for k be Nat st 1 <= k & k < p..f & f is_sequence_on G holds left_cell(f-:p,k,G) = left_cell(f,k,G) & right_cell(f-:p ,k,G) = right_cell(f,k,G); theorem :: JORDAN1J:54 for f,g be FinSequence of TOP-REAL 2 st f is unfolded s.n.c. one-to-one & g is unfolded s.n.c. one-to-one & f/.len f = g/.1 & L~f /\ L~g = { g/.1} holds f^'g is s.n.c.; theorem :: JORDAN1J:55 for f,g be FinSequence of TOP-REAL 2 st f is one-to-one & g is one-to-one & rng f /\ rng g c= {g/.1} holds f^'g is one-to-one; theorem :: JORDAN1J:56 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is being_S-Seq & p in rng f & p <> f.1 holds Index(p,f)+1 = p..f; theorem :: JORDAN1J:57 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & k <= width Gauge(C,n) & Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds j <> k; theorem :: JORDAN1J:58 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg( Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN1J:59 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg( Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN1J:60 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & LSeg (Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k )} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge( C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN1J:61 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & LSeg (Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k )} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) = {Gauge( C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN1J:62 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for j be Nat holds Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Upper_Arc L~Cage(C,n+1) & 1 <= j & j <= width Gauge(C,n+1) implies LSeg( Gauge(C,1)*(Center Gauge(C,1),1),Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets Lower_Arc L~Cage(C,n+1); theorem :: JORDAN1J:63 for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1 )*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C ,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*( Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C; theorem :: JORDAN1J:64 for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) = {Gauge(C,n+1 )*(Center Gauge(C,n+1),k)} & LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C ,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) = {Gauge(C,n+1)*( Center Gauge(C,n+1),j)} implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C; :: Moved from JORDAN, AG 20.01.2006 theorem :: JORDAN1J:65 for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & ( W-min Y in X or W-max Y in X) holds W-bound X = W-bound Y; theorem :: JORDAN1J:66 for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & ( E-min Y in X or E-max Y in X) holds E-bound X = E-bound Y; theorem :: JORDAN1J:67 for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & ( N-min Y in X or N-max Y in X) holds N-bound X = N-bound Y; theorem :: JORDAN1J:68 for X, Y being non empty compact Subset of TOP-REAL 2 st X c= Y & ( S-min Y in X or S-max Y in X) holds S-bound X = S-bound Y;