:: On the Segmentation of a Simple Closed Curve :: by Andrzej Trybulec :: :: Received August 18, 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, TOPREAL2, PRE_TOPC, EUCLID, SUBSET_1, XBOOLE_0, ORDINAL2, PSCOMP_1, RCOMP_1, RELAT_1, FUNCT_1, TOPMETR, TARSKI, XXREAL_2, ZFMISC_1, XXREAL_0, STRUCT_0, CARD_1, ARYTM_3, SEQ_4, JORDAN6, JORDAN3, COMPLEX1, ARYTM_1, CONNSP_2, SETFAM_1, XXREAL_1, PCOMPS_1, METRIC_1, REAL_1, WEIERSTR, TOPREAL1, FINSEQ_1, PARTFUN1, GOBRD10, MEASURE5, FINSET_1, JORDAN_A, NAT_1, CHORD, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_D, XXREAL_2, SEQ_4, RCOMP_1, TOPMETR, CONNSP_2, STRUCT_0, PRE_TOPC, TBSP_1, COMPTS_1, METRIC_1, RLVECT_1, EUCLID, TOPREAL1, TOPREAL2, GOBRD10, WEIERSTR, PCOMPS_1, JORDAN5C, JORDAN6, JORDAN7, MEASURE6, PSCOMP_1, JORDAN1K, XXREAL_0, BORSUK_1; constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, TBSP_1, TOPREAL1, MEASURE6, GOBRD10, JORDAN5C, JORDAN6, JORDAN7, JORDAN1K, SEQ_4, FUNCSDOM, BINOP_2, RVSUM_1, PSCOMP_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, MEMBERED, FINSEQ_1, RCOMP_1, STRUCT_0, COMPTS_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2, TOPREAL6, XXREAL_2, PCOMPS_1, PRE_TOPC, MEASURE6, ZFMISC_1, FUNCT_1, JORDAN5A; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries reserve C for Simple_closed_curve, p,q,p1 for Point of TOP-REAL 2, i,j,k,n for Nat, r,s for Real; theorem :: JORDAN_A:1 for T being non empty TopSpace, f being continuous RealMap of T, A being compact Subset of T holds f.:A is compact; theorem :: JORDAN_A:2 for A being compact Subset of REAL, B being non empty Subset of REAL st B c= A holds lower_bound B in A; theorem :: JORDAN_A:3 for A,B being compact non empty Subset of TOP-REAL n, f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:], g being RealMap of TOP-REAL n st for p being Point of TOP-REAL n ex G being Subset of REAL st G = { f.(p,q) where q is Point of TOP-REAL n : q in B } & g.p = lower_bound G holds lower_bound(f.:[:A,B:]) = lower_bound(g.:A); theorem :: JORDAN_A:4 for A,B being compact non empty Subset of TOP-REAL n, f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:], g being RealMap of TOP-REAL n st for q being Point of TOP-REAL n ex G being Subset of REAL st G = { f.(p,q) where p is Point of TOP-REAL n : p in A } & g.q = lower_bound G holds lower_bound(f.:[:A,B:]) = lower_bound(g.:B ); theorem :: JORDAN_A:5 q in Lower_Arc C & q <> W-min C implies LE E-max C, q, C; theorem :: JORDAN_A:6 q in Upper_Arc C implies LE q, E-max C, C; begin :: The Euclidean distance definition let n; func Eucl_dist n -> RealMap of [:TOP-REAL n, TOP-REAL n:] means :: JORDAN_A:def 1 for p,q being Point of TOP-REAL n holds it.(p,q) =|.p - q.|; end; definition let T be non empty TopSpace, f be RealMap of T; redefine attr f is continuous means :: JORDAN_A:def 2 for p being Point of T, N being Neighbourhood of f.p ex V being a_neighborhood of p st f.:V c= N; end; registration let n; cluster Eucl_dist n -> continuous; end; begin :: On the distance between subsets of a Euclidean space theorem :: JORDAN_A:7 :: JORDAN1K:39, JGRAPH_1:55 for A,B being non empty compact Subset of TOP-REAL n st A misses B holds dist_min(A,B) > 0; begin :: On the segments theorem :: JORDAN_A:8 LE p,q,C & LE q, E-max C, C & p <> q implies Segment(p,q,C) = Segment(Upper_Arc C,W-min C,E-max C,p,q); theorem :: JORDAN_A:9 LE E-max C, q, C implies Segment(E-max C,q,C) = Segment(Lower_Arc C,E-max C,W-min C,E-max C,q); theorem :: JORDAN_A:10 LE E-max C, q, C implies Segment(q,W-min C,C) = Segment(Lower_Arc C,E-max C,W-min C,q,W-min C); theorem :: JORDAN_A:11 LE p,q,C & LE E-max C, p, C implies Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q); theorem :: JORDAN_A:12 LE p,E-max C,C & LE E-max C, q, C implies Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p) \/ L_Segment(Lower_Arc C,E-max C,W-min C,q); theorem :: JORDAN_A:13 LE p,E-max C,C implies Segment(p,W-min C,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p) \/ L_Segment(Lower_Arc C,E-max C,W-min C,W-min C); theorem :: JORDAN_A:14 R_Segment(Upper_Arc C,W-min C,E-max C,p) = Segment(Upper_Arc C,W-min C,E-max C,p,E-max C); theorem :: JORDAN_A:15 L_Segment(Lower_Arc C,E-max C,W-min C,p) = Segment(Lower_Arc C,E-max C,W-min C,E-max C,p); theorem :: JORDAN_A:16 for p being Point of TOP-REAL 2 st p in C & p <> W-min C holds Segment(p,W-min C,C) is_an_arc_of p,W-min C; theorem :: JORDAN_A:17 for p,q being Point of TOP-REAL 2 st p<> q & LE p,q,C holds Segment(p,q,C) is_an_arc_of p,q; theorem :: JORDAN_A:18 :: poprawic JORDAN7:7 C = Segment(W-min C,W-min C,C); theorem :: JORDAN_A:19 for q being Point of TOP-REAL 2 st q in C holds Segment(q,W-min C,C) is compact; theorem :: JORDAN_A:20 for q1,q2 being Point of TOP-REAL 2 st LE q1,q2,C holds Segment(q1,q2,C) is compact; begin :: The concept of a segmentation definition let C; mode Segmentation of C -> FinSequence of TOP-REAL 2 means :: JORDAN_A:def 3 it/.1=W-min C & it is one-to-one & 8<=len it & rng it c= C & (for i being Nat st 1<=i & i non trivial for Segmentation of C; end; theorem :: JORDAN_A:21 for S being Segmentation of C, i st 1<=i & i <= len S holds S/.i in C; begin :: The segments of a segmentation definition let C; let i be Nat; let S be Segmentation of C; func Segm(S,i) -> Subset of TOP-REAL 2 equals :: JORDAN_A:def 4 Segment(S/.i,S/.(i+1),C) if 1<=i & i non empty compact; end; theorem :: JORDAN_A:23 for S being Segmentation of C, p st p in C ex i being Nat st i in dom S & p in Segm(S,i); theorem :: JORDAN_A:24 for S being Segmentation of C for i,j st 1<=i & i< j & j Real means :: JORDAN_A:def 5 ex W being Subset of Euclid n st W = C & it = diameter W; end; definition let C; let S be Segmentation of C; func diameter S -> Real means :: JORDAN_A:def 6 ex S1 being non empty finite Subset of REAL st S1 = { diameter Segm(S,i) where i is Element of NAT: i in dom S} & it = max S1; end; theorem :: JORDAN_A:32 for S being Segmentation of C, i holds diameter Segm(S,i) <= diameter S; theorem :: JORDAN_A:33 for S being Segmentation of C, e being Real st for i holds diameter Segm(S,i) < e holds diameter S < e; theorem :: JORDAN_A:34 for e being Real st e > 0 ex S being Segmentation of C st diameter S < e; begin :: The concept of the gap of a segmentation definition let C; let S be Segmentation of C; func S-Gap S -> Real means :: JORDAN_A:def 7 ex S1,S2 being non empty finite Subset of REAL st S1 = { dist_min(Segm(S,i),Segm(S,j)) where i,j is Element of NAT: 1<=i & i< j & j 0;