:: On the Upper and Lower Approximations of the Curve :: by Robert Milewski :: :: Received September 27, 2003 :: Copyright (c) 2003-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, TOPREAL2, PROB_1, STRUCT_0, EUCLID, FUNCT_1, JORDAN6, TOPREAL1, JORDAN9, KURATO_2, GOBOARD1, XXREAL_0, TREES_1, CARD_1, ARYTM_3, FINSEQ_1, INT_1, JORDAN1A, MATRIX_1, XBOOLE_0, PSCOMP_1, JORDAN8, RELAT_1, MCART_1, ARYTM_1, NEWTON, RCOMP_1, SPPOL_1, RLTOPSP1, TARSKI, RELAT_2, JORDAN1E, JORDAN3, ORDINAL4, PARTFUN1, FINSEQ_5, PRE_TOPC, GROUP_2, SPPOL_2, SPRECT_2, METRIC_1, GOBOARD5, FINSEQ_4, GRAPH_2, FINSEQ_6, ZFMISC_1, GOBOARD9, GOBOARD2, NAT_1, CONNSP_1, JORDAN2C, SEQ_4, REAL_1, CONNSP_2, POWER, COMPLEX1, JORDAN19, XXREAL_2; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, INT_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, FINSEQ_6, POWER, METRIC_1, CONNSP_2, GRAPH_2, SEQ_4, STRUCT_0, PRE_TOPC, TOPREAL2, NEWTON, PROB_1, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, SPPOL_2, KURATO_2, GOBOARD1, TOPREAL6, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN6, JORDAN8, JORDAN9, JORDAN2C, JORDAN1A, JORDAN1E; constructors REAL_1, NAT_D, FINSEQ_4, NEWTON, POWER, CONNSP_1, REALSET2, CONNSP_2, MATRIX_1, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, KURATO_2, SEQ_4, RELSET_1, CONVEX1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, COMPTS_1, METRIC_1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, PSCOMP_1, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, JORDAN6, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1J, CARD_1, FUNCT_1, RLTOPSP1, JORDAN2C, VALUED_0, NEWTON; requirements NUMERALS, ARITHM, BOOLE, SUBSET, REAL; begin reserve n for Nat; definition let C be Simple_closed_curve; func Upper_Appr C -> SetSequence of the carrier of TOP-REAL 2 means :: JORDAN19:def 1 for i be Nat holds it.i = Upper_Arc L~Cage (C,i); func Lower_Appr C -> SetSequence of the carrier of TOP-REAL 2 means :: JORDAN19:def 2 for i being Nat holds it.i = Lower_Arc L~Cage (C,i); end; definition let C be Simple_closed_curve; func North_Arc C -> Subset of TOP-REAL 2 equals :: JORDAN19:def 3 Lim_inf Upper_Appr C; func South_Arc C -> Subset of TOP-REAL 2 equals :: JORDAN19:def 4 Lim_inf Lower_Appr C; end; theorem :: JORDAN19:1 for n,m be Nat holds n <= m & n <> 0 implies (n+1)/n >= (m+1)/m; theorem :: JORDAN19:2 for E be compact non vertical non horizontal Subset of TOP-REAL 2 for m,j be Nat st 1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) holds LSeg(Gauge(E,n)*(Center Gauge(E,n),width Gauge(E,n)), Gauge(E,n)*(Center Gauge(E,n),j)) c= LSeg(Gauge(E,m)*(Center Gauge(E,m),width Gauge(E,m)), Gauge(E,n)*(Center Gauge(E,n),j)); theorem :: JORDAN19:3 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,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets L~Upper_Seq(C,n); theorem :: JORDAN19:4 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,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets Upper_Arc L~Cage(C,n); theorem :: JORDAN19:5 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 Lower_Arc L~Cage(C,n+1) & 1 <= j & j <= width Gauge(C,n+1) implies LSeg(Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)), Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets Upper_Arc L~Cage(C,n+1); theorem :: JORDAN19:6 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for f be FinSequence of TOP-REAL 2 for k be Nat st 1 <= k & k+1 <= len f & f is_sequence_on Gauge(C,n) holds dist(f/.k,f/.(k+1)) = (N-bound C - S-bound C)/2|^n or dist(f/.k,f/.(k+1)) = (E-bound C - W-bound C)/2|^n; theorem :: JORDAN19:7 for M be symmetric triangle MetrStruct for r be Real for p,q,x be Element of M st p in Ball(x,r) & q in Ball(x,r) holds dist(p,q) < 2*r; theorem :: JORDAN19:8 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds N-bound C < N-bound L~Cage(C,n); theorem :: JORDAN19:9 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds E-bound C < E-bound L~Cage(C,n); theorem :: JORDAN19:10 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds S-bound L~Cage(C,n) < S-bound C; theorem :: JORDAN19:11 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-bound L~Cage(C,n) < W-bound C; theorem :: JORDAN19:12 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= k & k <= j & j <= width Gauge(C,n) & LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Upper_Arc C; theorem :: JORDAN19:13 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= k & k <= j & j <= width Gauge(C,n) & LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j)} holds LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Lower_Arc C; theorem :: JORDAN19:14 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)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_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 :: JORDAN19:15 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)) /\ Lower_Arc L~Cage(C,n) = {Gauge(C,n)*(i,k)} & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_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 :: JORDAN19:16 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) & Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) & Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN19:17 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) & Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) & Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN19:18 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 & Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) & Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN19:19 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 & Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) & Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN19:20 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i1,j)} & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i2,k)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C; theorem :: JORDAN19:21 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i1,j)} & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i2,k)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C; theorem :: JORDAN19:22 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i1,j)} & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i2,k)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C; theorem :: JORDAN19:23 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i1,j)} & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i2,k)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C; theorem :: JORDAN19:24 for C be Simple_closed_curve for i1,i2,j,k be Nat holds 1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(i1,k) in Lower_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(i2,j) in Upper_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/ LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Lower_Arc C; theorem :: JORDAN19:25 for C be Simple_closed_curve for i1,i2,j,k be Nat holds 1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(i1,k) in Lower_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(i2,j) in Upper_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/ LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Upper_Arc C; theorem :: JORDAN19:26 for C be Simple_closed_curve for p be Point of TOP-REAL 2 st W-bound C < p`1 & p`1 < E-bound C holds not(p in North_Arc C & p in South_Arc C); theorem :: JORDAN19:27 :: "Nie oba" for C be Simple_closed_curve for p be Point of TOP-REAL 2 st p`1 = (W-bound C + E-bound C)/2 holds not (p in North_Arc C & p in South_Arc C);