:: Connectedness Conditions Using Polygonal Arcs
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

definition

let P be Subset of (TOP-REAL 2);
let p, q be Point of (TOP-REAL 2);

pred P is_S-P_arc_joining p,q means :: 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 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);

attr P 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;

attr P is being_Region means :: TOPREAL4:def 3
( P is open & P is connected );

end;

:: deftheorem 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 ;

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 by TOPREAL1:25;

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 )

proof end;

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

proof end;

theorem :: TOPREAL4:5

for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds
P is being_simple_closed_curve

proof end;

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) )

proof end;

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) )

proof end;

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) )

proof end;

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) )

proof end;

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) )

proof end;

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)) )

proof end;

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)) )

proof end;

theorem Th13: :: TOPREAL4:13

for p being Point of (TOP-REAL 2)
for f, h being FinSequence of (TOP-REAL 2)
for i being 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)) )

proof end;

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))) )

proof end;

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))) )

proof end;

theorem Th16: :: TOPREAL4:16

for f, h being FinSequence of (TOP-REAL 2)
for i being 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))) )

proof end;

theorem Th17: :: TOPREAL4:17

for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for n being 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)) )

proof end;

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 )

proof end;

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)) )

proof end;

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)) )

proof end;

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)) )

proof end;

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)) )

proof end;

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 )

proof end;

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 P, R 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

proof end;

theorem Th25: :: TOPREAL4:25

for p being Point of (TOP-REAL 2)
for P, R 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

proof end;

theorem Th26: :: TOPREAL4:26

for p being Point of (TOP-REAL 2)
for P, R 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

proof end;

theorem Th27: :: TOPREAL4:27

for p being Point of (TOP-REAL 2)
for P, R 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

proof end;

theorem :: TOPREAL4:28

for p being Point of (TOP-REAL 2)
for P, R 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 by Th27, Th26;

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 )

proof end;