:: Some Properties of Cells and Gauges :: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec :: :: Received October 13, 2000 :: Copyright (c) 2000-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, TOPREAL2, SUBSET_1, PRE_TOPC, EUCLID, INT_1, ARYTM_3, ARYTM_1, CARD_1, RELAT_1, PCOMPS_1, STRUCT_0, XXREAL_0, MATRIX_1, JORDAN8, METRIC_1, MCART_1, TREES_1, FINSEQ_1, PSCOMP_1, NEWTON, GOBOARD5, TARSKI, JORDAN2C, XXREAL_2, REAL_1, COMPLEX1, XXREAL_1, XBOOLE_0, RCOMP_1, FUNCT_1, TOPREAL1, SPPOL_1, TOPS_1, SEQ_4, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELSET_1, INT_1, XXREAL_2, SEQ_4, STRUCT_0, NAT_D, FINSEQ_1, MATRIX_0, RCOMP_1, TOPS_1, FUNCT_2, PRE_TOPC, NEWTON, COMPTS_1, EUCLID, PCOMPS_1, METRIC_1, METRIC_6, RLTOPSP1, TOPREAL1, TOPREAL2, GOBOARD5, JORDAN8, JORDAN2C, SPPOL_1, PSCOMP_1, TOPREAL6, SEQ_2; constructors REAL_1, RCOMP_1, NEWTON, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL2, GOBOARD1, SPPOL_1, GOBOARD5, PSCOMP_1, JORDAN2C, TOPREAL6, JORDAN8, NAT_D, SEQ_4, RELSET_1, FUNCSDOM, PCOMPS_1, SEQ_2, SQUARE_1, COMSEQ_2; registrations RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED, SEQ_2, STRUCT_0, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2, TOPREAL5, JORDAN2C, TOPREAL6, JORDAN8, VALUED_0, SPRECT_1, NEWTON, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve C for Simple_closed_curve, i, j, n for Nat, p for Point of TOP-REAL 2; theorem :: JORDAN1C:1 [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) = Gauge(C,n)*(i+1,j)`1 - Gauge( C,n)*(i,j)`1; theorem :: JORDAN1C:2 [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) = Gauge(C,n)*(i,j+1)`2 - Gauge( C,n)*(i,j)`2; theorem :: JORDAN1C:3 for S being Subset of TOP-REAL 2 st S is bounded holds proj1.:S is real-bounded; theorem :: JORDAN1C:4 for C1 being non empty compact Subset of TOP-REAL 2, C2, S being non empty Subset of TOP-REAL 2 holds S = C1 \/ C2 & proj1.:C2 is non empty bounded_below implies W-bound S = min(W-bound C1, W-bound C2); theorem :: JORDAN1C:5 for X being Subset of TOP-REAL 2 holds p in X & X is bounded implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2 & p`2 <= N-bound X; theorem :: JORDAN1C:6 for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies W-bound C <= W-bound BDD C; theorem :: JORDAN1C:7 for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies E-bound C >= E-bound BDD C; theorem :: JORDAN1C:8 for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies S-bound C <= S-bound BDD C; theorem :: JORDAN1C:9 for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies N-bound C >= N-bound BDD C; theorem :: JORDAN1C:10 for C being compact non vertical Subset of TOP-REAL 2 for I being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds 1 < I; theorem :: JORDAN1C:11 for C being compact non vertical Subset of TOP-REAL 2 for I being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds I + 1 <= len Gauge (C, n); theorem :: JORDAN1C:12 for C being compact non horizontal Subset of TOP-REAL 2 for J being Integer st p in BDD C & J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds 1 < J & J+1 <= width Gauge (C, n); theorem :: JORDAN1C:13 for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds (W-bound C) + (((E-bound C)-(W-bound C))/(2|^n) )*(I-2) <= p`1; theorem :: JORDAN1C:14 for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds p`1 < (W-bound C) + (((E-bound C)-(W-bound C))/ (2|^n))*(I-1); theorem :: JORDAN1C:15 for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds (S-bound C) + ((N-bound C - S-bound C)/(2|^n))* (J-2) <= p`2; theorem :: JORDAN1C:16 for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds p`2 < (S-bound C) + ((N-bound C - S-bound C)/(2 |^n))*(J-1); theorem :: JORDAN1C:17 for C being closed Subset of TOP-REAL 2, p being Point of Euclid 2 st p in BDD C ex r being Real st r > 0 & Ball(p,r) c= BDD C; theorem :: JORDAN1C:18 for p, q being Point of TOP-REAL 2, r being Real st dist(Gauge( C,n)*(1,1),Gauge(C,n)*(1,2)) < r & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r & p in cell (Gauge (C, n), i, j) & q in cell (Gauge (C, n), i, j) & 1 <= i & i+ 1 <= len Gauge (C,n) & 1 <= j & j+1 <= width Gauge(C,n) holds dist (p,q) < 2 * r; theorem :: JORDAN1C:19 for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2 <> N-bound BDD C; theorem :: JORDAN1C:20 for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1 <> E-bound BDD C; theorem :: JORDAN1C:21 for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2 <> S-bound BDD C; theorem :: JORDAN1C:22 for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1 <> W-bound BDD C; theorem :: JORDAN1C:23 p in BDD C implies ex n,i,j being Nat st 1 < i & i < len Gauge(C,n) & 1 < j & j < width Gauge(C,n) & p`1 <> (Gauge(C,n)*(i,j))`1 & p in cell(Gauge(C,n),i,j) & cell(Gauge(C,n),i,j) c= BDD C; theorem :: JORDAN1C:24 for C being Subset of TOP-REAL 2 st C is bounded holds UBD C is non empty;