:: Properties of the External Approximation of Jordan's Curve :: by Artur Korni{\l}owicz :: :: Received June 24, 1999 :: Copyright (c) 1999-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, RELAT_2, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, TOPREAL1, XXREAL_0, ARYTM_3, FINSEQ_1, JORDAN9, MATRIX_1, JORDAN8, PARTFUN1, RELAT_1, TREES_1, GOBOARD1, GOBOARD5, ARYTM_1, CARD_1, XBOOLE_0, TARSKI, RLTOPSP1, PSCOMP_1, NEWTON, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1, REAL_1, CONNSP_1, STRUCT_0, JORDAN2C, CONNSP_3, XXREAL_2, SETFAM_1, ZFMISC_1, TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, PARTFUN1, FINSEQ_1, NEWTON, DOMAIN_1, STRUCT_0, METRIC_1, TBSP_1, WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1, MATRIX_0, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4, PSCOMP_1, GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, TOPREAL6, JORDAN9, XXREAL_0; constructors REAL_1, NEWTON, TOPS_1, CONNSP_1, TBSP_1, TOPREAL4, PSCOMP_1, WEIERSTR, GOBOARD9, CONNSP_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, NAT_D, FUNCSDOM; registrations SUBSET_1, RELSET_1, FINSEQ_1, STRUCT_0, PRE_TOPC, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1, SPPOL_2, SPRECT_1, JORDAN2C, TOPREAL6, JORDAN8, FUNCT_1, NEWTON, ORDINAL1, XREAL_0, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Properties of the external approximation of Jordan's curve registration cluster connected compact non vertical non horizontal for Subset of TOP-REAL 2; end; reserve i, j, k, n for Nat, P for Subset of TOP-REAL 2, C for connected compact non vertical non horizontal Subset of TOP-REAL 2; theorem :: JORDAN10:1 1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i, j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i,j+1) implies i < len Gauge(C,n); theorem :: JORDAN10:2 1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i, j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j+1) & Cage(C,n)/.(k+ 1) = Gauge(C,n)*(i,j) implies i > 1; theorem :: JORDAN10:3 1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i+ 1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i+1,j) implies j > 1; theorem :: JORDAN10:4 1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i+ 1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i+1,j) & Cage(C,n)/.(k+ 1) = Gauge(C,n)*(i,j) implies j < width Gauge(C,n); theorem :: JORDAN10:5 C misses L~Cage(C,n); theorem :: JORDAN10:6 N-bound L~Cage(C,n) = N-bound C + (N-bound C - S-bound C)/(2|^n); theorem :: JORDAN10:7 i < j implies N-bound L~Cage(C,j) < N-bound L~Cage(C,i); registration let C be connected compact non vertical non horizontal Subset of TOP-REAL 2, n be Nat; cluster Cl RightComp Cage(C,n) -> compact; end; theorem :: JORDAN10:8 N-min C in RightComp Cage(C,n); theorem :: JORDAN10:9 C meets RightComp Cage (C,n); theorem :: JORDAN10:10 C misses LeftComp Cage(C,n); theorem :: JORDAN10:11 C c= RightComp Cage(C,n); theorem :: JORDAN10:12 C c= BDD L~Cage(C,n); theorem :: JORDAN10:13 UBD L~Cage(C,n) c= UBD C; definition let C be compact non vertical non horizontal Subset of TOP-REAL 2; func UBD-Family C -> set equals :: JORDAN10:def 1 the set of all UBD L~Cage(C,n) where n is Nat ; func BDD-Family C -> set equals :: JORDAN10:def 2 the set of all Cl BDD L~Cage(C,n) where n is Nat ; end; definition let C be compact non vertical non horizontal Subset of TOP-REAL 2; redefine func UBD-Family C -> Subset-Family of TOP-REAL 2; redefine func BDD-Family C -> Subset-Family of TOP-REAL 2; end; registration let C be compact non vertical non horizontal Subset of TOP-REAL 2; cluster UBD-Family C -> non empty; cluster BDD-Family C -> non empty; end; theorem :: JORDAN10:14 union UBD-Family C = UBD C; theorem :: JORDAN10:15 C c= meet BDD-Family C; theorem :: JORDAN10:16 BDD C misses LeftComp Cage(C,n); theorem :: JORDAN10:17 BDD C c= RightComp Cage(C,n); theorem :: JORDAN10:18 P is_inside_component_of C implies P misses L~Cage(C,n); theorem :: JORDAN10:19 BDD C misses L~Cage(C,n); theorem :: JORDAN10:20 COMPLEMENT UBD-Family C = BDD-Family C; theorem :: JORDAN10:21 meet BDD-Family C = C \/ BDD C;