:: On the Segmentation of a Simple Closed Curve :: by Andrzej Trybulec :: :: Received August 18, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin theorem Th1: :: JORDAN_A:1 for T being non empty TopSpace for f being continuous RealMap of T for A being compact Subset of T holds f .: A is compact proofend; theorem Th2: :: JORDAN_A:2 for A being compact Subset of REAL for B being non empty Subset of REAL st B c= A holds lower_bound B in A proofend; theorem :: JORDAN_A:3 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for 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) proofend; theorem :: JORDAN_A:4 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for 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) proofend; theorem Th5: :: JORDAN_A:5 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds LE E-max C,q,C proofend; theorem Th6: :: JORDAN_A:6 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds LE q, E-max C,C proofend; begin definition let n be Element of NAT ; A1: [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def_2; func Eucl_dist n -> RealMap of [:(TOP-REAL n),(TOP-REAL n):] means :Def1: :: JORDAN_A:def 1 for p, q being Point of (TOP-REAL n) holds it . (p,q) = |.(p - q).|; existence ex b1 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).| proofend; uniqueness for b1, b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Eucl_dist JORDAN_A:def_1_:_ for n being Element of NAT for b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds ( b2 = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| ); definition let T be non empty TopSpace; let f be RealMap of T; redefine attr f is continuous means :: JORDAN_A:def 2 for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N; compatibility ( f is continuous iff for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) proofend; end; :: deftheorem defines continuous JORDAN_A:def_2_:_ for T being non empty TopSpace for f being RealMap of T holds ( f is continuous iff for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ); Lm1: for X, Y being TopSpace holds TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] proofend; registration let n be Element of NAT ; cluster Eucl_dist n -> continuous ; coherence Eucl_dist n is continuous proofend; end; begin theorem Th7: :: JORDAN_A:7 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds dist_min (A,B) > 0 proofend; begin theorem Th8: :: JORDAN_A:8 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) proofend; theorem Th9: :: JORDAN_A:9 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) proofend; theorem Th10: :: JORDAN_A:10 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) proofend; theorem Th11: :: JORDAN_A:11 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) proofend; theorem Th12: :: JORDAN_A:12 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds 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)) proofend; theorem Th13: :: JORDAN_A:13 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds 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))) proofend; theorem Th14: :: JORDAN_A:14 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) holds 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)) proofend; theorem Th15: :: JORDAN_A:15 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) holds 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) proofend; theorem Th16: :: JORDAN_A:16 for C being Simple_closed_curve 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 proofend; theorem Th17: :: JORDAN_A:17 for C being Simple_closed_curve 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 proofend; theorem Th18: :: JORDAN_A:18 for C being Simple_closed_curve holds C = Segment ((W-min C),(W-min C),C) proofend; theorem Th19: :: JORDAN_A:19 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in C holds Segment (q,(W-min C),C) is compact proofend; theorem Th20: :: JORDAN_A:20 for C being Simple_closed_curve for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds Segment (q1,q2,C) is compact proofend; begin definition let C be Simple_closed_curve; mode Segmentation of C -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3 ( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Element of NAT st 1 <= i & i < len it holds LE it /. i,it /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len it holds (Segment ((it /. i),(it /. (i + 1)),C)) /\ (Segment ((it /. (i + 1)),(it /. (i + 2)),C)) = {(it /. (i + 1))} ) & (Segment ((it /. (len it)),(it /. 1),C)) /\ (Segment ((it /. 1),(it /. 2),C)) = {(it /. 1)} & (Segment ((it /. ((len it) -' 1)),(it /. (len it)),C)) /\ (Segment ((it /. (len it)),(it /. 1),C)) = {(it /. (len it))} & Segment ((it /. ((len it) -' 1)),(it /. (len it)),C) misses Segment ((it /. 1),(it /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len it & not i,j are_adjacent1 holds Segment ((it /. i),(it /. (i + 1)),C) misses Segment ((it /. j),(it /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len it holds Segment ((it /. (len it)),(it /. 1),C) misses Segment ((it /. i),(it /. (i + 1)),C) ) ); existence ex b1 being FinSequence of (TOP-REAL 2) st ( b1 /. 1 = W-min C & b1 is one-to-one & 8 <= len b1 & rng b1 c= C & ( for i being Element of NAT st 1 <= i & i < len b1 holds LE b1 /. i,b1 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b1 holds (Segment ((b1 /. i),(b1 /. (i + 1)),C)) /\ (Segment ((b1 /. (i + 1)),(b1 /. (i + 2)),C)) = {(b1 /. (i + 1))} ) & (Segment ((b1 /. (len b1)),(b1 /. 1),C)) /\ (Segment ((b1 /. 1),(b1 /. 2),C)) = {(b1 /. 1)} & (Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C)) /\ (Segment ((b1 /. (len b1)),(b1 /. 1),C)) = {(b1 /. (len b1))} & Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C) misses Segment ((b1 /. 1),(b1 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b1 & not i,j are_adjacent1 holds Segment ((b1 /. i),(b1 /. (i + 1)),C) misses Segment ((b1 /. j),(b1 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b1 holds Segment ((b1 /. (len b1)),(b1 /. 1),C) misses Segment ((b1 /. i),(b1 /. (i + 1)),C) ) ) proofend; end; :: deftheorem Def3 defines Segmentation JORDAN_A:def_3_:_ for C being Simple_closed_curve for b2 being FinSequence of (TOP-REAL 2) holds ( b2 is Segmentation of C iff ( b2 /. 1 = W-min C & b2 is one-to-one & 8 <= len b2 & rng b2 c= C & ( for i being Element of NAT st 1 <= i & i < len b2 holds LE b2 /. i,b2 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b2 holds (Segment ((b2 /. i),(b2 /. (i + 1)),C)) /\ (Segment ((b2 /. (i + 1)),(b2 /. (i + 2)),C)) = {(b2 /. (i + 1))} ) & (Segment ((b2 /. (len b2)),(b2 /. 1),C)) /\ (Segment ((b2 /. 1),(b2 /. 2),C)) = {(b2 /. 1)} & (Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C)) /\ (Segment ((b2 /. (len b2)),(b2 /. 1),C)) = {(b2 /. (len b2))} & Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C) misses Segment ((b2 /. 1),(b2 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b2 & not i,j are_adjacent1 holds Segment ((b2 /. i),(b2 /. (i + 1)),C) misses Segment ((b2 /. j),(b2 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b2 holds Segment ((b2 /. (len b2)),(b2 /. 1),C) misses Segment ((b2 /. i),(b2 /. (i + 1)),C) ) ) ); registration let C be Simple_closed_curve; cluster -> non trivial for Segmentation of C; coherence for b1 being Segmentation of C holds not b1 is trivial proofend; end; theorem Th21: :: JORDAN_A:21 for C being Simple_closed_curve for S being Segmentation of C for i being Element of NAT st 1 <= i & i <= len S holds S /. i in C proofend; begin definition let C be Simple_closed_curve; let i be Nat; let S be Segmentation of C; func Segm (S,i) -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4 Segment ((S /. i),(S /. (i + 1)),C) if ( 1 <= i & i < len S ) otherwise Segment ((S /. (len S)),(S /. 1),C); correctness coherence ( ( 1 <= i & i < len S implies Segment ((S /. i),(S /. (i + 1)),C) is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment ((S /. (len S)),(S /. 1),C) is Subset of (TOP-REAL 2) ) ); consistency for b1 being Subset of (TOP-REAL 2) holds verum; ; end; :: deftheorem Def4 defines Segm JORDAN_A:def_4_:_ for C being Simple_closed_curve for i being Nat for S being Segmentation of C holds ( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) ); theorem :: JORDAN_A:22 for C being Simple_closed_curve for i being Element of NAT for S being Segmentation of C st i in dom S holds Segm (S,i) c= C proofend; registration let C be Simple_closed_curve; let S be Segmentation of C; let i be Element of NAT ; cluster Segm (S,i) -> non empty compact ; coherence ( not Segm (S,i) is empty & Segm (S,i) is compact ) proofend; end; theorem :: JORDAN_A:23 for C being Simple_closed_curve for S being Segmentation of C for p being Point of (TOP-REAL 2) st p in C holds ex i being Nat st ( i in dom S & p in Segm (S,i) ) proofend; theorem Th24: :: JORDAN_A:24 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds Segm (S,i) misses Segm (S,j) proofend; theorem Th25: :: JORDAN_A:25 for C being Simple_closed_curve for S being Segmentation of C for j being Element of NAT st 1 < j & j < (len S) -' 1 holds Segm (S,(len S)) misses Segm (S,j) proofend; theorem Th26: :: JORDAN_A:26 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} proofend; theorem Th27: :: JORDAN_A:27 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds Segm (S,i) meets Segm (S,j) proofend; theorem Th28: :: JORDAN_A:28 for C being Simple_closed_curve for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} proofend; theorem Th29: :: JORDAN_A:29 for C being Simple_closed_curve for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1) proofend; theorem Th30: :: JORDAN_A:30 for C being Simple_closed_curve for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} proofend; theorem Th31: :: JORDAN_A:31 for C being Simple_closed_curve for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1)) proofend; begin definition let n be Element of NAT ; let C be Subset of (TOP-REAL n); func diameter C -> Real means :Def5: :: JORDAN_A:def 5 ex W being Subset of (Euclid n) st ( W = C & it = diameter W ); existence ex b1 being Real ex W being Subset of (Euclid n) st ( W = C & b1 = diameter W ) proofend; correctness uniqueness for b1, b2 being Real st ex W being Subset of (Euclid n) st ( W = C & b1 = diameter W ) & ex W being Subset of (Euclid n) st ( W = C & b2 = diameter W ) holds b1 = b2; ; end; :: deftheorem Def5 defines diameter JORDAN_A:def_5_:_ for n being Element of NAT for C being Subset of (TOP-REAL n) for b3 being Real holds ( b3 = diameter C iff ex W being Subset of (Euclid n) st ( W = C & b3 = diameter W ) ); definition let C be Simple_closed_curve; let S be Segmentation of C; func diameter S -> Real means :Def6: :: 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 ); existence ex b1 being Real 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 } & b1 = max S1 ) proofend; correctness uniqueness for b1, b2 being Real st 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 } & b1 = max S1 ) & 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 } & b2 = max S1 ) holds b1 = b2; ; end; :: deftheorem Def6 defines diameter JORDAN_A:def_6_:_ for C being Simple_closed_curve for S being Segmentation of C for b3 being Real holds ( b3 = diameter S iff 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 } & b3 = max S1 ) ); theorem :: JORDAN_A:32 for C being Simple_closed_curve for S being Segmentation of C for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S proofend; theorem Th33: :: JORDAN_A:33 for C being Simple_closed_curve for S being Segmentation of C for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds diameter S < e proofend; theorem :: JORDAN_A:34 for C being Simple_closed_curve for e being Real st e > 0 holds ex S being Segmentation of C st diameter S < e proofend; begin definition let C be Simple_closed_curve; let S be Segmentation of C; func S-Gap S -> Real means :Def7: :: 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 < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & it = min ((min S1),(min S2)) ); existence ex b1 being Real 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 < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) ) proofend; correctness uniqueness for b1, b2 being Real st 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 < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) ) & 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 < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b2 = min ((min S1),(min S2)) ) holds b1 = b2; ; end; :: deftheorem Def7 defines S-Gap JORDAN_A:def_7_:_ for C being Simple_closed_curve for S being Segmentation of C for b3 being Real holds ( b3 = S-Gap S iff 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 < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b3 = min ((min S1),(min S2)) ) ); theorem Th35: :: JORDAN_A:35 for C being Simple_closed_curve for S being Segmentation of C ex F being non empty finite Subset of REAL st ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F ) proofend; theorem :: JORDAN_A:36 for C being Simple_closed_curve for S being Segmentation of C holds S-Gap S > 0 proofend;