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

definition
let P be Subset of ();
let p, q be Point of ();
pred P is_S-P_arc_joining p,q means :: TOPREAL4:def 1
ex f being FinSequence of () 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 ()
for p, q being Point of () holds
( P is_S-P_arc_joining p,q iff ex f being FinSequence of () st
( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) );

definition
let P be Subset of ();
attr P is being_special_polygon means :: TOPREAL4:def 2
ex p1, p2 being Point of () ex P1, P2 being Subset of () 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 () holds
( P is being_special_polygon iff ex p1, p2 being Point of () ex P1, P2 being Subset of () 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 ()
for p, q being Point of () 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 ()
for p, q being Point of () 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 ()
for p, q being Point of () 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 ()
for p, q being Point of () st P is_S-P_arc_joining p,q holds
p <> q
proof end;

theorem :: TOPREAL4:5
for P being Subset of () 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 ()
for f being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for r being Real
for u being Point of () st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex P being Subset of () 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 ()
for f, h being FinSequence of () 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 ()
for f, h being FinSequence of () 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 ()
for f, h being FinSequence of ()
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 () 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 () 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 ()
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 ()
for f being FinSequence of ()
for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds
ex h being FinSequence of () 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 ()
for f being FinSequence of () st p <> f /. 1 & f is being_S-Seq & p in L~ f holds
ex h being FinSequence of () 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 ()
for f, h being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f, h being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f, h being FinSequence of ()
for r being Real
for u being Point of () 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 ()
for f being FinSequence of ()
for r being Real
for u being Point of () 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 () 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 ()
for p, p1, p2 being Point of ()
for P being Subset of ()
for r being Real
for u being Point of () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )
proof end;

Lm1: TopSpaceMetr () = TopStruct(# the carrier of (), the topology of () #)
by EUCLID:def 8;

theorem Th24: :: TOPREAL4:24
for P, R being Subset of ()
for p being Point of () st R is being_Region & P = { q where q is Point of () : ( q <> p & q in R & ( for P1 being Subset of () 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 ()
for P, R being Subset of () st R is being_Region & p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () 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 ()
for P, R being Subset of () st p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () 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 ()
for P, R being Subset of () st R is being_Region & p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () 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 ()
for P, R being Subset of () st R is being_Region & p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () st
( P1 is_S-P_arc_joining p,q & P1 c= R ) )
}
holds
R = P by ;

theorem :: TOPREAL4:29
for p, q being Point of ()
for R being Subset of () st R is being_Region & p in R & q in R & p <> q holds
ex P being Subset of () st
( P is_S-P_arc_joining p,q & P c= R )
proof end;