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