:: TOPREAL4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 :Def1: :: TOPREAL4:def 1
 ex f being FinSequence of (TOP-REAL 2) st
( f is_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_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 ) );

notation
let P be Subset of (TOP-REAL 2);
synonym P is_special_polygon for being_special_polygon P;
end;

definition
let T be TopStruct ;
let P be Subset of T;
attr P 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 ) );

notation
let T be TopStruct ;
let P be Subset of T;
synonym P is_Region for being_Region P;
end;

theorem :: TOPREAL4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: TOPREAL4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_S-P_arc
proof end;

theorem Th3: :: TOPREAL4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: TOPREAL4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st P is_special_polygon holds
P is_simple_closed_curve
proof end;

theorem Th7: :: TOPREAL4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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 Th11: :: TOPREAL4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th12: :: TOPREAL4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|,p*> holds
( h is_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|,p*> holds
( h is_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 Th14: :: TOPREAL4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for f, h being FinSequence of (TOP-REAL 2)
for i being Nat st p <> f /. 1 & f is_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg f,i & p <> f /. i & p <> f /. (i + 1) & h = (f | i) ^ <*p*> holds
( h is_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 Th15: :: TOPREAL4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is_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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is_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_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 Th17: :: TOPREAL4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, h being FinSequence of (TOP-REAL 2)
for i being Nat st f /. i <> f /. 1 & f is_S-Seq & i > 2 & i in dom f & h = f | i holds
( h is_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 Th18: :: TOPREAL4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_S-Seq & p in LSeg f,n holds
ex h being FinSequence of (TOP-REAL 2) st
( h is_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 Th19: :: TOPREAL4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is_S-Seq & p in L~ f holds
ex h being FinSequence of (TOP-REAL 2) st
( h is_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 Th20: :: TOPREAL4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) & not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & f is_S-Seq & (LSeg (f /. (len f)),p) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds
( h is_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
proof end;

theorem Th21: :: TOPREAL4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & f is_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 Th22: :: TOPREAL4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & |[((f /. (len f)) `1 ),(p `2 )]| in Ball u,r & f is_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 Th23: :: TOPREAL4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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 Th24: :: TOPREAL4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) = TOP-REAL 2
by EUCLID:def 8;

theorem Th25: :: TOPREAL4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, P being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st R is_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 Th26: :: TOPREAL4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for R, P being Subset of (TOP-REAL 2) st R is_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 Th27: :: TOPREAL4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th28: :: TOPREAL4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for R, P being Subset of (TOP-REAL 2) st R is_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:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for R, P being Subset of (TOP-REAL 2) st R is_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
proof end;

theorem :: TOPREAL4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2)
for R being Subset of (TOP-REAL 2) st R is_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;