:: Upper and Lower Sequence on the Cage. Part II :: by Robert Milewski :: :: Received September 28, 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, ZFMISC_1, FINSEQ_1, XBOOLE_0, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1, FINSEQ_4, ARYTM_3, RFINSEQ, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8, JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, XXREAL_0, TREES_1, PARTFUN1, FUNCT_1, ARYTM_1, RLTOPSP1, TARSKI, CARD_1, PRE_TOPC, ORDINAL4, NEWTON, NAT_1, JORDAN1A, SPPOL_2, JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6, XCMPLX_0; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, MATRIX_1, FINSEQ_6, STRUCT_0, PRE_TOPC, NEWTON, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E, NAT_1; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, TOPS_2, MATRIX_1, TOPMETR, PSCOMP_1, JORDAN3, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D; registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, GOBOARD1, SPPOL_2, SPRECT_1, SPRECT_2, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, CARD_1, EUCLID, SPPOL_1, NEWTON, ORDINAL1, SUBSET_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve n for Nat; registration cluster trivial for FinSequence; end; theorem :: JORDAN1G:1 for f be trivial FinSequence holds f is empty or ex x be object st f = <*x*>; registration let p be non trivial FinSequence; cluster Rev p -> non trivial; end; theorem :: JORDAN1G:2 for D be non empty set for f be FinSequence of D for G be Matrix of D for p be set holds f is_sequence_on G implies f-:p is_sequence_on G; theorem :: JORDAN1G:3 for D be non empty set for f be FinSequence of D for G be Matrix of D for p be Element of D st p in rng f holds f is_sequence_on G implies f:-p is_sequence_on G; theorem :: JORDAN1G:4 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_sequence_on Gauge(C,n); theorem :: JORDAN1G:5 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) is_sequence_on Gauge(C,n); registration let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; cluster Upper_Seq(C,n) -> standard; cluster Lower_Seq(C,n) -> standard; end; theorem :: JORDAN1G:6 for G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`2 = G*(i2,j2)`2 implies j1 = j2; theorem :: JORDAN1G:7 for G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`1 = G*(i2,j2)`1 implies i1 = i2; theorem :: JORDAN1G:8 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~ f & f/.len f <> N-max L~f) holds (N-min L~f)`1 < (N-max L~f)`1; theorem :: JORDAN1G:9 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds N-min L~f <> N-max L~f; theorem :: JORDAN1G:10 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~ f & f/.len f <> S-max L~f) holds (S-min L~f)`1 < (S-max L~f)`1; theorem :: JORDAN1G:11 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds S-min L~f <> S-max L~f; theorem :: JORDAN1G:12 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~ f & f/.len f <> W-max L~f) holds (W-min L~f)`2 < (W-max L~f)`2; theorem :: JORDAN1G:13 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds W-min L~f <> W-max L~f; theorem :: JORDAN1G:14 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~ f & f/.len f <> E-max L~f) holds (E-min L~f)`2 < (E-max L~f)`2; theorem :: JORDAN1G:15 for f be standard special unfolded non trivial FinSequence of TOP-REAL 2 st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds E-min L~f <> E-max L~f; theorem :: JORDAN1G:16 for D be non empty set for f be FinSequence of D for p,q be Element of D st p in rng f & q in rng f & q..f <= p..f holds (f-:p):-q = (f:-q) -:p; theorem :: JORDAN1G:17 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:W-min L~Cage(C,n)) /\ L~ (Cage(C,n):-W-min L~Cage(C,n)) = {N-min L~Cage(C,n),W-min L~Cage(C,n)}; theorem :: JORDAN1G:18 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~ Cage(C,n); theorem :: JORDAN1G:19 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1; theorem :: JORDAN1G:20 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C, n); theorem :: JORDAN1G:21 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C ,n); theorem :: JORDAN1G:22 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C, n); theorem :: JORDAN1G:23 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-max L~Cage(C,n))..Upper_Seq(C,n) <= (E-max L~Cage(C,n))..Upper_Seq(C ,n); theorem :: JORDAN1G:24 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n); theorem :: JORDAN1G:25 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1; theorem :: JORDAN1G:26 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n)).. Lower_Seq(C,n); theorem :: JORDAN1G:27 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n)).. Lower_Seq(C,n); theorem :: JORDAN1G:28 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-max L~Cage(C,n))..Lower_Seq(C,n) < (S-min L~Cage(C,n)).. Lower_Seq(C,n); theorem :: JORDAN1G:29 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-min L~Cage(C,n))..Lower_Seq(C,n) <= (W-min L~Cage(C,n)).. Lower_Seq(C,n); theorem :: JORDAN1G:30 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n); theorem :: JORDAN1G:31 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Upper_Seq(C,n)/.2)`1 = W-bound L~Cage(C,n); theorem :: JORDAN1G:32 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Lower_Seq(C,n)/.2)`1 = E-bound L~Cage(C,n); theorem :: JORDAN1G:33 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C; theorem :: JORDAN1G:34 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds S-bound L~Cage(C,n) + N-bound L~Cage(C,n) = S-bound C + N-bound C; theorem :: JORDAN1G:35 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat, i be Nat st 1 <= i & i <= width Gauge(C,n) & n > 0 holds Gauge(C,n)*(Center Gauge(C,n),i)`1 = (W-bound C + E-bound C) / 2; theorem :: JORDAN1G:36 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n,i be Nat st 1 <= i & i <= len Gauge(C,n) & n > 0 holds Gauge(C,n)*(i,Center Gauge(C,n))`2 = (S-bound C + N-bound C) / 2; theorem :: JORDAN1G:37 for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.1 in L~mid(f,k1,k2) holds k1 = 1 or k2 = 1; theorem :: JORDAN1G:38 for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.(len f) in L~mid(f,k1,k2) holds k1 = len f or k2 = len f; theorem :: JORDAN1G:39 for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds rng Upper_Seq(C,n) c= rng Cage(C,n) & rng Lower_Seq(C,n) c= rng Cage(C,n); theorem :: JORDAN1G:40 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_a_h.c._for Cage(C,n); theorem :: JORDAN1G:41 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n); theorem :: JORDAN1G:42 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n); theorem :: JORDAN1G:43 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in rng Lower_Seq(C,n); theorem :: JORDAN1G:44 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n); theorem :: JORDAN1G:45 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in L~Lower_Seq(C,n); theorem :: JORDAN1G:46 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds LSeg(Gauge(C,n)*( i,1),Gauge(C,n)*(i,j)) meets L~Lower_Seq(C,n); theorem :: JORDAN1G:47 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+ E-bound L~Cage(C,n))/2)) in rng Upper_Seq(C,n); theorem :: JORDAN1G:48 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds Last_Point(L~Lower_Seq(C,n), E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+ E-bound L~Cage(C,n))/2)) in rng Lower_Seq(C,n); theorem :: JORDAN1G:49 for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) = mid(f,1,p..f); theorem :: JORDAN1G:50 for f be S-Sequence_in_R2 for Q be closed Subset of TOP-REAL 2 st L~f meets Q & not f/.1 in Q & First_Point(L~f,f/.1,f/.len f,Q) in rng f holds L~mid(f,1,First_Point(L~f,f/.1,f/.len f,Q)..f) /\ Q = {First_Point(L~f,f /.1,f/.len f,Q)}; theorem :: JORDAN1G:51 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Upper_Seq(C,n) holds (Upper_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; theorem :: JORDAN1G:52 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Rev Lower_Seq(C, n) holds (Rev Lower_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/ 2; theorem :: JORDAN1G:53 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for q be Point of TOP-REAL 2 holds q in rng mid(Upper_Seq(C,n),2,First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n), E-max L~Cage(C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) ..Upper_Seq(C,n)) implies q`1 <= (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; theorem :: JORDAN1G:54 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage (C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2; theorem :: JORDAN1G:55 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n); theorem :: JORDAN1G:56 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n); theorem :: JORDAN1G:57 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~ Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets Lower_Arc L~Cage( C,n);