:: Connectedness Conditions Using Polygonal Arcs :: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz :: :: Received August 24, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin definition let P be Subset of (TOP-REAL 2); let p, q be Point of (TOP-REAL 2); predP is_S-P_arc_joining p,q means :Def1: :: TOPREAL4:def 1 ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ); end; :: deftheorem Def1 defines is_S-P_arc_joining TOPREAL4:def_1_:_ for P being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) holds ( P is_S-P_arc_joining p,q iff ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) ); definition let P be Subset of (TOP-REAL 2); attrP is being_special_polygon means :: TOPREAL4:def 2 ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ); end; :: deftheorem defines being_special_polygon TOPREAL4:def_2_:_ for P being Subset of (TOP-REAL 2) holds ( P is being_special_polygon iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) ); definition let T be TopStruct ; let P be Subset of T; attrP is being_Region means :Def3: :: TOPREAL4:def 3 ( P is open & P is connected ); end; :: deftheorem Def3 defines being_Region TOPREAL4:def_3_:_ for T being TopStruct for P being Subset of T holds ( P is being_Region iff ( P is open & P is connected ) ); theorem Th1: :: TOPREAL4:1 for P being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds P is being_S-P_arc proofend; theorem Th2: :: TOPREAL4:2 for P being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds P is_an_arc_of p,q proofend; theorem Th3: :: TOPREAL4:3 for P being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds ( p in P & q in P ) proofend; theorem :: TOPREAL4:4 for P being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds p <> q proofend; theorem :: TOPREAL4:5 for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds P is being_simple_closed_curve proofend; theorem Th6: :: TOPREAL4:6 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p `1 = q `1 & p `2 <> q `2 & p in Ball (u,r) & q in Ball (u,r) & f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> holds ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q & L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) proofend; theorem Th7: :: TOPREAL4:7 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p `1 <> q `1 & p `2 = q `2 & p in Ball (u,r) & q in Ball (u,r) & f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> holds ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q & L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) proofend; theorem Th8: :: TOPREAL4:8 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p `1 <> q `1 & p `2 <> q `2 & p in Ball (u,r) & q in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & f = <*p,|[(p `1),(q `2)]|,q*> holds ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q & L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) proofend; theorem Th9: :: TOPREAL4:9 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p `1 <> q `1 & p `2 <> q `2 & p in Ball (u,r) & q in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & f = <*p,|[(q `1),(p `2)]|,q*> holds ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q & L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) proofend; theorem Th10: :: TOPREAL4:10 for p, q being Point of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) proofend; theorem Th11: :: TOPREAL4:11 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `2 = p `2 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*> holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) proofend; theorem Th12: :: TOPREAL4:12 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*> holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) proofend; theorem Th13: :: TOPREAL4:13 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) proofend; theorem Th14: :: TOPREAL4:14 for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `2 = (f /. 1) `2 & h = <*(f /. 1),|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2)*> holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ) proofend; theorem Th15: :: TOPREAL4:15 for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `1 = (f /. 1) `1 & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2)*> holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ) proofend; theorem Th16: :: TOPREAL4:16 for f, h being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & i > 2 & i in dom f & h = f | i holds ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) ) proofend; theorem Th17: :: TOPREAL4:17 for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds ex h being FinSequence of (TOP-REAL 2) st ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) proofend; theorem Th18: :: TOPREAL4:18 for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is being_S-Seq & p in L~ f holds ex h being FinSequence of (TOP-REAL 2) st ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f ) proofend; theorem Th19: :: TOPREAL4:19 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) proofend; theorem Th20: :: TOPREAL4:20 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> & ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) proofend; theorem Th21: :: TOPREAL4:21 for p being Point of (TOP-REAL 2) for f, h being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) proofend; theorem Th22: :: TOPREAL4:22 for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st not f /. 1 in Ball (u,r) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & not p in L~ f holds ex h being FinSequence of (TOP-REAL 2) st ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) proofend; theorem Th23: :: TOPREAL4:23 for R being Subset of (TOP-REAL 2) for p, p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) for r being Real for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) proofend; Lm1: TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def_8; theorem Th24: :: TOPREAL4:24 for R, P being Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st R is being_Region & P = { q where q is Point of (TOP-REAL 2) : ( q <> p & q in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) } holds P is open proofend; theorem Th25: :: TOPREAL4:25 for p being Point of (TOP-REAL 2) for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds P is open proofend; theorem Th26: :: TOPREAL4:26 for p being Point of (TOP-REAL 2) for R, P being Subset of (TOP-REAL 2) st p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds P c= R proofend; theorem Th27: :: TOPREAL4:27 for p being Point of (TOP-REAL 2) for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds R c= P proofend; theorem :: TOPREAL4:28 for p being Point of (TOP-REAL 2) for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds R = P proofend; theorem :: TOPREAL4:29 for p, q being Point of (TOP-REAL 2) for R being Subset of (TOP-REAL 2) st R is being_Region & p in R & q in R & p <> q holds ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= R ) proofend;