:: Connectedness Conditions Using Polygonal Arcs
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, FINSEQ_1, REAL_1, TOPREAL1,
PARTFUN1, XBOOLE_0, RCOMP_1, RELAT_2, XXREAL_0, RELAT_1, FUNCT_1,
TOPREAL2, MCART_1, METRIC_1, ARYTM_3, TARSKI, RLTOPSP1, ORDINAL4, NAT_1,
CARD_1, ARYTM_1, PCOMPS_1, STRUCT_0, TOPREAL4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, STRUCT_0,
PRE_TOPC, CONNSP_1, METRIC_1, PCOMPS_1, RLTOPSP1, EUCLID, TOPREAL1,
TOPREAL2, XXREAL_0;
constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, FINSEQ_4, CONNSP_1, PCOMPS_1,
TOPREAL1, TOPREAL2, RELSET_1, FUNCSDOM, DOMAIN_1, COMPLEX1;
registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0,
PRE_TOPC, EUCLID, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, XBOOLE_0;
equalities TOPREAL1, STRUCT_0;
expansions TARSKI, TOPREAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, PRE_TOPC, CONNSP_1,
EUCLID, TOPMETR, TOPREAL1, TOPREAL2, TOPREAL3, FINSEQ_4, FINSEQ_3,
TBSP_1, PARTFUN2, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
PARTFUN1, ORDINAL1, RLTOPSP1;
schemes NAT_1;
begin
reserve P,P1,P2,R for Subset of TOP-REAL 2,
p,p1,p2,p3,p11,p22,q,q1,q2,q3,q4 for Point of TOP-REAL 2,
f,h for FinSequence of TOP-REAL 2,
r for Real,
u for Point of Euclid 2,
n,m,i,j,k for Nat,
x,y for set;
definition
let P,p,q;
pred P is_S-P_arc_joining p,q means
ex f st f is being_S-Seq & P = L~ f & p=f/.1 & q=f/.len f;
end;
definition
let P;
attr P is being_special_polygon means
ex p1,p2,P1,P2 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;
definition
let T be TopStruct, P be Subset of T;
attr P is being_Region means
P is open connected;
end;
theorem Th1:
P is_S-P_arc_joining p,q implies P is being_S-P_arc;
theorem Th2:
P is_S-P_arc_joining p,q implies P is_an_arc_of p,q
by TOPREAL1:25;
theorem Th3:
P is_S-P_arc_joining p,q implies p in P & q in P
proof
assume P is_S-P_arc_joining p,q;
then P is_an_arc_of p,q by Th2;
hence thesis by TOPREAL1:1;
end;
theorem
P is_S-P_arc_joining p,q implies p<>q
proof
assume that
A1: P is_S-P_arc_joining p,q and
A2: p=q;
consider f such that
A3: f is being_S-Seq and
P = L~f and
A4: p=f/.1 & q=f/.len f by A1;
len f >= 2 by A3;
then Seg len f = dom f & len f >= 1 by FINSEQ_1:def 3,XXREAL_0:2;
then
A5: len f in dom f & 1 in dom f by FINSEQ_1:1;
f is one-to-one & 1 <> len f by A3;
hence contradiction by A2,A4,A5,PARTFUN2:10;
end;
theorem
P is being_special_polygon implies P is being_simple_closed_curve
proof
given p1,p2,P1,P2 such that
A1: p1 <> p2 & p1 in P & p2 in P and
A2: P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 and
A3: P1 /\ P2 = {p1,p2} and
A4: P = P1 \/ P2;
reconsider P1, P2 as non empty Subset of TOP-REAL 2 by A3;
P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 by A2,Th2;
hence thesis by A1,A3,A4,TOPREAL2:6;
end;
theorem Th6:
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 *> implies 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
assume that
A1: p`1 = q`1 and
A2: p`2 <> q`2 and
A3: p in Ball(u,r) & q in Ball(u,r) and
A4: f =<* p,|[p`1,(p`2+q`2)/2]|,q *>;
thus
A5: f is being_S-Seq & f/.1 =p & f/.len f = q by A1,A2,A4,TOPREAL3:36;
p=|[p`1,p`2]| & q=|[q`1,q`2]| by EUCLID:53;
then |[p`1,(p`2+q`2)/2]| in Ball(u,r) by A1,A3,TOPREAL3:23;
then
A6: LSeg(p,|[p`1,(p`2+q`2)/2]|) c= Ball(u,r) & LSeg(|[p`1,(p`2+q`2)/2]|,q)
c= Ball(u,r) by A3,TOPREAL3:21;
thus L~f is_S-P_arc_joining p,q by A5;
L~f=LSeg(p,|[p`1,(p`2+q`2)/2]|) \/ LSeg(|[p`1,(p`2+q`2)/2]|,q) by A4,
TOPREAL3:16;
hence thesis by A6,XBOOLE_1:8;
end;
theorem Th7:
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 *> implies 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
assume that
A1: p`1 <> q`1 and
A2: p`2 = q`2 and
A3: p in Ball(u,r) & q in Ball(u,r) and
A4: f = <* p,|[(p`1+q`1)/2,p`2]|,q *>;
thus
A5: f is being_S-Seq & f/.1 =p & f/.len f = q by A1,A2,A4,TOPREAL3:37;
p=|[p`1,p`2]| & q=|[q`1,q`2]| by EUCLID:53;
then |[(p`1+q`1)/2,p`2]| in Ball(u,r) by A2,A3,TOPREAL3:24;
then
A6: LSeg(p,|[(p`1+q`1)/2,p`2]|) c= Ball(u,r) & LSeg(|[(p`1+q`1)/2,p`2]|,q)
c= Ball(u,r) by A3,TOPREAL3:21;
thus L~f is_S-P_arc_joining p,q by A5;
L~f=LSeg(p,|[(p`1+q`1)/2,p`2]|) \/ LSeg(|[(p`1+q`1)/2,p`2]|,q) by A4,
TOPREAL3:16;
hence thesis by A6,XBOOLE_1:8;
end;
theorem Th8:
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 *> implies 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
assume that
A1: p`1 <> q`1 & p`2 <> q`2 and
A2: p in Ball(u,r) and
A3: q in Ball(u,r) and
A4: |[p`1,q`2]| in Ball(u,r) and
A5: f =<* p,|[p`1,q`2]|,q *>;
thus
A6: f is being_S-Seq & f/.1 =p & f/.len f = q by A1,A5,TOPREAL3:34;
A7: LSeg(|[p`1,q`2]|,q) c= Ball(u,r) by A3,A4,TOPREAL3:21;
thus L~f is_S-P_arc_joining p,q by A6;
L~f=LSeg(p,|[p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,q) & LSeg(p,|[p`1,q`2]|) c=
Ball (u,r) by A2,A4,A5,TOPREAL3:16,21;
hence thesis by A7,XBOOLE_1:8;
end;
theorem Th9:
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 *> implies 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
assume that
A1: p`1 <> q`1 & p`2 <> q`2 and
A2: p in Ball(u,r) and
A3: q in Ball(u,r) and
A4: |[q`1,p`2]| in Ball(u,r) and
A5: f =<* p,|[q`1,p`2]|,q *>;
thus
A6: f is being_S-Seq & f/.1 =p & f/.len f = q by A1,A5,TOPREAL3:35;
A7: LSeg(|[q`1,p`2]|,q) c= Ball(u,r) by A3,A4,TOPREAL3:21;
thus L~f is_S-P_arc_joining p,q by A6;
L~f=LSeg(p,|[q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,q) & LSeg(p,|[q`1,p`2]|) c=
Ball (u,r) by A2,A4,A5,TOPREAL3:16,21;
hence thesis by A7,XBOOLE_1:8;
end;
theorem Th10:
p <> q & p in Ball(u,r) & q in Ball(u,r) implies ex P st P
is_S-P_arc_joining p,q & P c= Ball(u,r)
proof
assume that
A1: p<>q and
A2: p in Ball(u,r) & q in Ball(u,r);
now
per cases by A1,TOPREAL3:6;
suppose
A3: p`1 <> q`1;
now
per cases;
suppose
A4: p`2 = q`2;
reconsider P = L~<* p,|[(p`1+q`1)/2,p`2]|,q *> as Subset of TOP-REAL
2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A3,A4,Th7;
end;
suppose
A5: p`2 <> q`2;
A6: p = |[p`1,p`2]| & q=|[q`1,q`2]| by EUCLID:53;
now
per cases by A2,A6,TOPREAL3:25;
suppose
A7: |[p`1,q`2]| in Ball(u,r);
reconsider P = L~<* p,|[p`1,q`2]|,q *> as Subset of TOP-REAL 2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A3,A5,A7,Th8
;
end;
suppose
A8: |[q`1,p`2]| in Ball(u,r);
reconsider P = L~<* p,|[q`1,p`2]|,q *> as Subset of TOP-REAL 2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A3,A5,A8,Th9
;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A9: p`2 <> q`2;
now
per cases;
suppose
A10: p`1 = q`1;
reconsider P = L~<* p,|[p`1,(p`2+q`2)/2]|,q *> as Subset of TOP-REAL
2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A9,A10,Th6;
end;
suppose
A11: p`1 <> q`1;
A12: p = |[p`1,p`2]| & q=|[q`1,q`2]| by EUCLID:53;
now
per cases by A2,A12,TOPREAL3:25;
suppose
A13: |[p`1,q`2]| in Ball(u,r);
reconsider P = L~<* p,|[p`1,q`2]|,q *> as Subset of TOP-REAL 2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A9,A11,A13
,Th8;
end;
suppose
A14: |[q`1,p`2]| in Ball(u,r);
reconsider P = L~<* p,|[q`1,p`2]|,q *> as Subset of TOP-REAL 2;
take P;
thus P is_S-P_arc_joining p,q & P c= Ball(u,r) by A2,A9,A11,A14
,Th9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th11:
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 *> implies 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
assume that
A1: p<>f/.1 and
A2: (f/.1)`2 = p`2 and
A3: f is being_S-Seq and
A4: p in LSeg(f,1) and
A5: h = <* f/.1,|[((f/.1)`1+p`1)/2, (f/.1)`2]|,p *>;
set p1 = f/.1, q = f/.(1+1);
A6: L~h=LSeg(p1,|[(p1`1 + p`1)/2,p1`2]|) \/ LSeg(|[(p1`1 + p`1)/2,p1`2]|,p)
by A5,TOPREAL3:16;
A7: len f >= 2 by A3;
then
A8: LSeg(f,1) = LSeg(p1,q) by TOPREAL1:def 3;
A9: p1`1 <> p`1 by A1,A2,TOPREAL3:6;
hence
A10: h is being_S-Seq & h/.1 = p1 & h/.len h = p by A2,A5,TOPREAL3:37;
p1 in LSeg(p1,q) by RLTOPSP1:68;
then
A11: LSeg(p1,p) c= LSeg(p1,q) by A4,A8,TOPREAL1:6;
A12: Seg len f = dom f by FINSEQ_1:def 3;
thus L~h is_S-P_arc_joining p1,p by A10;
A13: LSeg(f,1) c= L~f by TOPREAL3:19;
LSeg(p1,|[(p1`1 + p`1)/2,p1`2]|) \/ LSeg(|[(p1`1 + p`1)/2,p1`2]|,p) =
LSeg(p1,p) by A2,A9,TOPREAL1:5,TOPREAL3:13;
hence L~h c= L~f by A8,A11,A6,A13;
len f >= 1 by A7,XXREAL_0:2;
then Seg 1 c= Seg len f by FINSEQ_1:5;
then f|1 = f|Seg 1 & dom f /\ Seg 1 = Seg 1 by A12,FINSEQ_1:def 16
,XBOOLE_1:28;
then dom(f|1) = Seg 1 by RELAT_1:61;
then len (f|1) = 1 by FINSEQ_1:def 3;
then L~(f|1)={} by TOPREAL1:22;
hence thesis by A2,A9,A6,TOPREAL1:5,TOPREAL3:13;
end;
theorem Th12:
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 *> implies 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
set p1 = f/.1;
assume that
A1: p<>p1 and
A2: p1`1 = p`1 and
A3: f is being_S-Seq and
A4: p in LSeg(f,1) and
A5: h = <* p1,|[p1`1,(p1`2+p`2)/2]|,p *>;
A6: L~h = LSeg(p1,|[p1`1,(p1`2+p`2)/2]|) \/ LSeg(|[p1`1,(p1`2+p`2)/2]|,p)
by A5,TOPREAL3:16;
set q = f/.(1+1);
A7: len f >= 2 by A3;
then
A8: LSeg(f,1) = LSeg(p1,q) by TOPREAL1:def 3;
A9: p1`2 <> p`2 by A1,A2,TOPREAL3:6;
hence
A10: h is being_S-Seq & h/.1 = p1 & h/.len h = p by A2,A5,TOPREAL3:36;
p1 in LSeg(p1,q) by RLTOPSP1:68;
then
A11: LSeg(p1,p) c= LSeg(p1,q) by A4,A8,TOPREAL1:6;
A12: Seg len f = dom f by FINSEQ_1:def 3;
thus L~h is_S-P_arc_joining p1,p by A10;
A13: LSeg(f,1) c= L~f by TOPREAL3:19;
LSeg(p1,|[p1`1,(p1`2+p`2)/2]|) \/ LSeg(|[p1`1,(p1`2+p`2)/2]|,p) = LSeg(
p1,p) by A2,A9,TOPREAL1:5,TOPREAL3:14;
hence L~h c= L~f by A8,A11,A6,A13;
len f >= 1 by A7,XXREAL_0:2;
then Seg 1 c= Seg len f by FINSEQ_1:5;
then f|1 = f|Seg 1 & dom f /\ Seg 1 = Seg 1 by A12,FINSEQ_1:def 16
,XBOOLE_1:28;
then dom(f|1) = Seg 1 by RELAT_1:61;
then len (f|1) = 1 by FINSEQ_1:def 3;
then L~(f|1)={} by TOPREAL1:22;
hence thesis by A2,A9,A6,TOPREAL1:5,TOPREAL3:14;
end;
theorem Th13:
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*> implies 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
set p1 = f/.1, q = f/.i;
assume that
A1: f is being_S-Seq and
A2: i in dom f and
A3: i+1 in dom f and
A4: i>1 and
A5: p in LSeg(f,i) and
A6: p<>f/.i and
A7: h = (f|i)^<*p*>;
A8: f is one-to-one by A1;
set v = f|i;
A9: v = f|Seg i by FINSEQ_1:def 16;
then
A10: dom v=dom f /\ Seg i by RELAT_1:61;
A11: Seg len h = dom h by FINSEQ_1:def 3;
A12: f is unfolded by A1;
A13: f is special by A1;
A14: f is s.n.c. by A1;
set q1 = f/.i, q2 = f/.(i+1);
A15: Seg len f = dom f by FINSEQ_1:def 3;
then
A16: i+1<=len f by A3,FINSEQ_1:1;
then
A17: p in LSeg(q1,q2) by A4,A5,TOPREAL1:def 3;
A18: LSeg(f,i) = LSeg(q1,q2) by A4,A16,TOPREAL1:def 3;
A19: LSeg(f,i) = LSeg(q2,q1) by A4,A16,TOPREAL1:def 3;
i<>i+1;
then
A20: q1 <> q2 by A2,A3,A8,PARTFUN2:10;
A21: q1 in LSeg(q1,q2) by RLTOPSP1:68;
A22: q1 = |[q1`1,q1`2]| & q2 = |[q2`1,q2`2]| by EUCLID:53;
A23: i in NAT by ORDINAL1:def 12;
A24: i<=len f by A2,A15,FINSEQ_1:1;
then Seg i c= dom f by A15,FINSEQ_1:5;
then
A25: dom v = Seg i by A10,XBOOLE_1:28;
then
A26: len v = i by FINSEQ_1:def 3,A23;
then
A27: len h = i + len <*p*> by A7,FINSEQ_1:22
.= i+1 by FINSEQ_1:39;
then
A28: h/.len h = p by A7,A26,FINSEQ_4:67;
A29: i in dom v by A4,A25,FINSEQ_1:1;
then
A30: h/.i=v/.i by A7,FINSEQ_4:68
.= q1 by A29,FINSEQ_4:70;
then
A31: LSeg(h,i) = LSeg(q1,p) by A4,A27,A28,TOPREAL1:def 3;
A32: 1+1<=i by A4,NAT_1:13;
thus
A33: h is being_S-Seq
proof
now
set Z = {m where m is Nat: 1<=m & m<=len h};
given x,y being object such that
A34: x in dom h and
A35: y in dom h and
A36: h.x = h.y and
A37: x<>y;
x in Z by A11,A34,FINSEQ_1:def 1;
then consider k1 be Nat such that
A38: k1=x and
A39: 1<=k1 and
A40: k1<=len h;
y in Z by A11,A35,FINSEQ_1:def 1;
then consider k2 be Nat such that
A41: k2=y and
A42: 1<=k2 and
A43: k2<=len h;
A44: h/.k1 = h.y by A34,A36,A38,PARTFUN1:def 6
.= h/.k2 by A35,A41,PARTFUN1:def 6;
k2<=len f by A27,A16,A43,XXREAL_0:2;
then
A45: k2 in dom f by A15,A42,FINSEQ_1:1;
k1<=len f by A27,A16,A40,XXREAL_0:2;
then
A46: k1 in dom f by A15,A39,FINSEQ_1:1;
A47: k1+(1+1) = k1+1+1;
A48: k2+(1+1) = k2+1+1;
now
per cases by A27,A40,A43,XXREAL_0:1;
suppose
k1=i+1 & k2=i+1;
hence contradiction by A37,A38,A41;
end;
suppose
A49: k1=i+1 & k2<i+1;
then
A50: k2+1<=k1 by NAT_1:13;
now
per cases by A50,XXREAL_0:1;
suppose
k2 + 1 = k1;
hence contradiction by A6,A7,A26,A30,A44,A49,FINSEQ_4:67;
end;
suppose
k2 + 1 < k1;
then
A51: k2+1<=i by A49,NAT_1:13;
now
per cases by A51,XXREAL_0:1;
suppose
A52: k2+1=i;
then k2<=i by NAT_1:11;
then
A53: k2 in dom v by A25,A42,FINSEQ_1:1;
then
A54: h/.k2 = v/.k2 by A7,FINSEQ_4:68
.= f/.k2 by A53,FINSEQ_4:70;
k2+1 <= len f by A2,A15,A52,FINSEQ_1:1;
then
A55: f/.k2 in LSeg(f,k2) by A42,TOPREAL1:21;
LSeg(f,k2) /\ LSeg(f,i) = {f/.i} by A12,A16,A42,A48,A52;
then f/.k2 in {f/.i} by A5,A27,A28,A44,A49,A55,A54,
XBOOLE_0:def 4;
then
A56: f/.k2 = f/.i by TARSKI:def 1;
k2<i by A52,NAT_1:13;
hence contradiction by A2,A8,A45,A56,PARTFUN2:10;
end;
suppose
A57: k2+1<i;
then
A58: k2+1<=len f by A24,XXREAL_0:2;
A59: LSeg(f,k2) misses LSeg(f,i) by A14,A57;
k2<=k2+1 by NAT_1:11;
then k2<=i by A57,XXREAL_0:2;
then
A60: k2 in dom v by A25,A42,FINSEQ_1:1;
then h/.k2 = v/.k2 by A7,FINSEQ_4:68
.= f/.k2 by A60,FINSEQ_4:70;
then p in LSeg(f,k2) by A27,A28,A42,A44,A49,A58,TOPREAL1:21;
hence contradiction by A5,A59,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A61: k1<i+1 & k2=i+1;
then
A62: k1+1<=k2 by NAT_1:13;
now
per cases by A62,XXREAL_0:1;
suppose
k1 + 1 = k2;
hence contradiction by A6,A7,A26,A30,A44,A61,FINSEQ_4:67;
end;
suppose
k1 + 1 < k2;
then
A63: k1+1<=i by A61,NAT_1:13;
now
per cases by A63,XXREAL_0:1;
suppose
A64: k1+1=i;
then k1<=i by NAT_1:11;
then
A65: k1 in dom v by A25,A39,FINSEQ_1:1;
then
A66: h/.k1 = v/.k1 by A7,FINSEQ_4:68
.= f/.k1 by A65,FINSEQ_4:70;
k1+1 <= len f by A2,A15,A64,FINSEQ_1:1;
then
A67: f/.k1 in LSeg(f,k1) by A39,TOPREAL1:21;
LSeg(f,k1) /\ LSeg(f,i) = {f/.i} by A12,A16,A39,A47,A64;
then f/.k1 in {f/.i} by A5,A27,A28,A44,A61,A67,A66,
XBOOLE_0:def 4;
then
A68: f/.k1 = f/.i by TARSKI:def 1;
k1<i by A64,NAT_1:13;
hence contradiction by A2,A8,A46,A68,PARTFUN2:10;
end;
suppose
A69: k1+1<i;
then
A70: k1+1<=len f by A24,XXREAL_0:2;
A71: LSeg(f,k1) misses LSeg(f,i) by A14,A69;
k1<=k1+1 by NAT_1:11;
then k1<=i by A69,XXREAL_0:2;
then
A72: k1 in dom v by A25,A39,FINSEQ_1:1;
then h/.k1 = v/.k1 by A7,FINSEQ_4:68
.= f/.k1 by A72,FINSEQ_4:70;
then p in LSeg(f,k1) by A27,A28,A39,A44,A61,A70,TOPREAL1:21;
hence contradiction by A5,A71,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A73: k1<i+1 & k2<i+1;
then k2<=i by NAT_1:13;
then
A74: k2 in dom v by A25,A42,FINSEQ_1:1;
k1<=i by A73,NAT_1:13;
then
A75: k1 in dom v by A25,A39,FINSEQ_1:1;
then f.k1 = v.k1 by A9,FUNCT_1:47
.= h.k1 by A7,A75,FINSEQ_1:def 7
.= v.k2 by A7,A36,A38,A41,A74,FINSEQ_1:def 7
.= f.k2 by A9,A74,FUNCT_1:47;
hence contradiction by A8,A37,A38,A41,A46,A45,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
hence h is one-to-one by FUNCT_1:def 4;
thus len h >= 2 by A4,A27,A32,XREAL_1:6;
thus h is unfolded
proof
let j be Nat such that
A76: 1 <= j and
A77: j + 2 <= len h;
A78: 1<=j+1 by NAT_1:11;
j+1+1 = j+(1+1);
then j+1<=i by A27,A77,XREAL_1:6;
then
A79: j+1 in dom v by A25,A78,FINSEQ_1:1;
then
A80: h/.(j+1) = v/.(j+1) by A7,FINSEQ_4:68
.= f/.(j+1) by A79,FINSEQ_4:70;
i+1+1 = i+(1+1);
then len h <= i+2 by A27,NAT_1:11;
then j+2 <= i+2 by A77,XXREAL_0:2;
then j<=i by XREAL_1:6;
then
A81: j in dom v by A25,A76,FINSEQ_1:1;
then
A82: LSeg(h,j) = LSeg(v,j) by A7,A79,TOPREAL3:18
.= LSeg(f,j) by A81,A79,TOPREAL3:17;
j<=j+2 by NAT_1:11;
then
A83: 1<=j+(1+1) by A76,XXREAL_0:2;
A84: j+(1+1) = j+1+1;
i+1 in Seg len f by A3,FINSEQ_1:def 3;
then len h <= len f by A27,FINSEQ_1:1;
then
A85: j+2 <= len f by A77,XXREAL_0:2;
then
A86: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A12,A76;
now
per cases by A77,XXREAL_0:1;
suppose
A87: j+2 = len h;
j +1 <= j+1+1 by NAT_1:11;
then j+1 <= len h by A77,XXREAL_0:2;
then
A88: h/.(j+1) in LSeg(h,j) by A76,TOPREAL1:21;
h/.(j+1) in LSeg(h,j+1) by A77,A78,A84,TOPREAL1:21;
then h/.(j+1) in LSeg(h,j) /\ LSeg(h,j+1) by A88,XBOOLE_0:def 4;
then
A89: {h/.(j+1)} c= LSeg(h,j) /\ LSeg(h,j+1) by ZFMISC_1:31;
LSeg(h,j) /\ LSeg(h,j+1) c= {h/.(j+1)} by A27,A18,A21,A17,A31,A86,A82
,A80,A87,TOPREAL1:6,XBOOLE_1:26;
hence thesis by A89;
end;
suppose
j+2 < len h;
then j+(1+1)<=i by A27,NAT_1:13;
then
A90: j+1+1 in dom v by A25,A83,FINSEQ_1:1;
then LSeg(h,j+1) = LSeg(v,j+1) by A7,A79,TOPREAL3:18
.= LSeg(f,j+1) by A79,A90,TOPREAL3:17;
hence thesis by A12,A76,A85,A82,A80;
end;
end;
hence thesis;
end;
thus h is s.n.c.
proof
let n,m be Nat;
assume
A91: m>n+1;
n<=n+1 by NAT_1:11;
then
A92: n<=m by A91,XXREAL_0:2;
A93: 1<=n+1 by NAT_1:11;
A94: LSeg(f,n) misses LSeg(f,m) by A14,A91;
now
per cases by XXREAL_0:1;
suppose
A95: m+1<len h;
A96: 1<m by A91,A93,XXREAL_0:2;
then
A97: 1<=m+1 by NAT_1:13;
m+1<=i by A27,A95,NAT_1:13;
then
A98: m+1 in dom v by A25,A97,FINSEQ_1:1;
A99: m<=i by A27,A95,XREAL_1:6;
then
A100: m in dom v by A25,A96,FINSEQ_1:1;
then
A101: LSeg(h,m)=LSeg(v,m) by A7,A98,TOPREAL3:18
.= LSeg(f,m) by A100,A98,TOPREAL3:17;
now
per cases;
suppose
0<n;
then
A102: 0+1<=n by NAT_1:13;
n+1<=i by A91,A99,XXREAL_0:2;
then
A103: n+1 in dom v by A25,A93,FINSEQ_1:1;
n<=i by A92,A99,XXREAL_0:2;
then
A104: n in dom v by A25,A102,FINSEQ_1:1;
then LSeg(h,n)=LSeg(v,n) by A7,A103,TOPREAL3:18
.= LSeg(f,n) by A104,A103,TOPREAL3:17;
then LSeg(h,n) misses LSeg(h,m) by A14,A91,A101;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
0=n;
then LSeg(h,n)={} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
A105: m+1=len h;
A106: LSeg(f,n) /\ LSeg(f,m) = {} by A94;
now
per cases;
suppose
0<n;
then 0+1<=n by NAT_1:13;
then
A107: n in dom v by A25,A27,A92,A105,FINSEQ_1:1;
A108: n+1 in dom v by A25,A27,A91,A93,A105,FINSEQ_1:1;
then LSeg(h,n)=LSeg(v,n) by A7,A107,TOPREAL3:18
.= LSeg(f,n) by A107,A108,TOPREAL3:17;
hence {} = LSeg(h,m) /\ (LSeg(f,m) /\ LSeg(h,n)) by A106
.= LSeg(h,m) /\ LSeg(f,m) /\ LSeg(h,n) by XBOOLE_1:16
.= LSeg(h,n) /\ LSeg(h,m) by A27,A18,A21,A17,A31,A105,
TOPREAL1:6,XBOOLE_1:28;
end;
suppose
0=n;
then LSeg(h,n)={} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
m+1>len h;
then LSeg(h,m) = {} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
let n be Nat such that
A109: 1 <= n and
A110: n + 1 <= len h;
set p3 = h/.n, p4 = h/.(n+1);
now
per cases by A110,XXREAL_0:1;
suppose
A111: n+1 = len h;
A112: i in dom v by A4,A25,FINSEQ_1:1;
then
A113: p3 = v/.i by A7,A27,A111,FINSEQ_4:68
.= q1 by A112,FINSEQ_4:70;
now
per cases by A4,A13,A16;
suppose
A114: q1`1 = q2`1;
then
A115: q1`2<> q2`2 by A20,TOPREAL3:6;
now
per cases by A115,XXREAL_0:1;
suppose
q1`2<q2`2;
then p in {p11: p11`1 = q1`1 & q1`2 <= p11`2 & p11`2<=q2`2}
by A5,A19,A22,A114,TOPREAL3:9;
then ex p11 st p=p11 & p11`1 = q1`1 & q1`2 <= p11`2 & p11`2<=
q2`2;
hence thesis by A7,A26,A27,A111,A113,FINSEQ_4:67;
end;
suppose
q2`2<q1`2;
then p in {p22: p22`1 = q1`1 & q2`2 <= p22`2 & p22`2<=q1`2}
by A5,A19,A22,A114,TOPREAL3:9;
then ex p11 st p=p11 & p11`1 = q1`1 & q2`2 <= p11`2 & p11`2<=
q1`2;
hence thesis by A7,A26,A27,A111,A113,FINSEQ_4:67;
end;
end;
hence thesis;
end;
suppose
A116: q1`2 = q2`2;
then
A117: q1`1<> q2`1 by A20,TOPREAL3:6;
now
per cases by A117,XXREAL_0:1;
suppose
q1`1<q2`1;
then p in {p11: p11`2 = q1`2 & q1`1 <= p11`1 & p11`1<=q2`1}
by A5,A19,A22,A116,TOPREAL3:10;
then ex p11 st p=p11 & p11`2 = q1`2 & q1`1 <= p11`1 & p11`1<=
q2`1;
hence thesis by A7,A26,A27,A111,A113,FINSEQ_4:67;
end;
suppose
q2`1<q1`1;
then p in {p22: p22`2 = q1`2 & q2`1 <= p22`1 & p22`1<=q1`1}
by A5,A19,A22,A116,TOPREAL3:10;
then ex p11 st p=p11 & p11`2 = q1`2 & q2`1 <= p11`1 & p11`1<=
q1`1;
hence thesis by A7,A26,A27,A111,A113,FINSEQ_4:67;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A118: n+1 < len h;
A119: 1<=n+1 by A109,NAT_1:13;
n+1<=i by A27,A118,NAT_1:13;
then
A120: n+1 in dom v by A25,A119,FINSEQ_1:1;
then h/.(n+1)=v/.(n+1) by A7,FINSEQ_4:68;
then
A121: p4=f/.(n+1) by A120,FINSEQ_4:70;
n<=i by A27,A118,XREAL_1:6;
then
A122: n in dom v by A25,A109,FINSEQ_1:1;
then h/.n=v/.n by A7,FINSEQ_4:68;
then
A123: p3=f/.n by A122,FINSEQ_4:70;
n+1 <= len f by A27,A16,A110,XXREAL_0:2;
hence thesis by A13,A109,A123,A121;
end;
end;
hence thesis;
end;
A124: 1 in dom v by A4,A25,FINSEQ_1:1;
then h/.1 = v/.1 by A7,FINSEQ_4:68
.= p1 by A124,FINSEQ_4:70;
hence
A125: h/.1=p1 & h/.len h=p by A7,A26,A27,FINSEQ_4:67;
set Mf = {LSeg(f,j): 1<=j & j+1<=len f}, Mv = {LSeg(v,n): 1<=n & n+1<=len v}
, Mh = {LSeg(h,m): 1<=m & m+1<=len h};
A126: Seg len v = dom v by FINSEQ_1:def 3;
thus L~h is_S-P_arc_joining p1,p by A33,A125;
A127: now
let x;
assume x in L~h;
then consider X be set such that
A128: x in X and
A129: X in Mh by TARSKI:def 4;
consider k such that
A130: X=LSeg(h,k) and
A131: 1<=k and
A132: k+1<=len h by A129;
A133: k+1<= len f by A27,A16,A132,XXREAL_0:2;
now
per cases by A132,XXREAL_0:1;
suppose
A134: k+1 = len h;
then
A135: LSeg(f,k) in Mf by A27,A16,A131;
LSeg(h,i) c= LSeg(f,i) by A5,A18,A21,A31,TOPREAL1:6;
hence x in L~f by A27,A128,A130,A134,A135,TARSKI:def 4;
thus x in L~v \/ LSeg(q1,p) by A27,A31,A128,A130,A134,XBOOLE_0:def 3;
end;
suppose
A136: k+1 < len h;
then
A137: k+1<=len v by A26,A27,NAT_1:13;
A138: k+1<=i by A27,A136,NAT_1:13;
k<=k+1 by NAT_1:11;
then k<=i by A138,XXREAL_0:2;
then
A139: k in dom v by A25,A131,FINSEQ_1:1;
1<=k+1 by A131,NAT_1:13;
then
A140: k+1 in dom v by A25,A138,FINSEQ_1:1;
then
A141: X=LSeg(v,k) by A7,A130,A139,TOPREAL3:18
.= LSeg(f,k) by A140,A139,TOPREAL3:17;
then X in Mf by A131,A133;
hence x in L~f by A128,TARSKI:def 4;
X=LSeg(v,k) by A140,A139,A141,TOPREAL3:17;
then X in Mv by A131,A137;
then x in union Mv by A128,TARSKI:def 4;
hence x in L~v \/ LSeg(q1,p) by XBOOLE_0:def 3;
end;
end;
hence x in L~f & x in L~v \/ LSeg(q1,p);
end;
thus L~h c= L~f
by A127;
A142: i<=i+1 by NAT_1:11;
thus L~h c= L~(f|i) \/ LSeg(q,p)
by A127;
let x be object such that
A143: x in L~v \/ LSeg(q,p);
now
per cases by A143,XBOOLE_0:def 3;
suppose
x in L~v;
then consider X be set such that
A144: x in X and
A145: X in Mv by TARSKI:def 4;
consider k such that
A146: X=LSeg(v,k) and
A147: 1<=k and
A148: k+1<=len v by A145;
A149: k+1<=len h by A26,A27,A142,A148,XXREAL_0:2;
k<=k+1 by NAT_1:11;
then k<=len v by A148,XXREAL_0:2;
then
A150: k in Seg len v by A147,FINSEQ_1:1;
1<=k+1 by NAT_1:11;
then k+1 in Seg len v by A148,FINSEQ_1:1;
then X=LSeg(h,k) by A7,A126,A146,A150,TOPREAL3:18;
then X in Mh by A147,A149;
hence thesis by A144,TARSKI:def 4;
end;
suppose
A151: x in LSeg(q,p);
LSeg(h,i) in Mh by A4,A27;
hence thesis by A31,A151,TARSKI:def 4;
end;
end;
hence thesis;
end;
theorem Th14:
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 *> implies 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
set p1 = f/.1, p = f/.2;
assume that
A1: p<>p1 and
A2: f is being_S-Seq and
A3: p`2 = p1`2 and
A4: h = <* p1,|[(p1`1+p`1)/2,p1`2]|,p *>;
A5: p1`1 <> p`1 by A1,A3,TOPREAL3:6;
hence
A6: h is being_S-Seq & h/.1 = p1 & h/.len h = p by A3,A4,TOPREAL3:37;
A7: LSeg(p1,|[(p1`1 + p`1)/2,p1`2]|) \/ LSeg(|[(p1`1 + p`1)/2,p1`2]|,p) =
LSeg(p1,p) by A3,A5,TOPREAL1:5,TOPREAL3:13;
set M = {LSeg(f|2,k): 1<=k & k+1<=len(f|2)};
A8: Seg len f = dom f by FINSEQ_1:def 3;
A9: L~h=LSeg(p1,|[(p1`1 + p`1)/2,p1`2]|) \/ LSeg(|[(p1`1 + p`1)/2,p1`2]|,p)
by A4,TOPREAL3:16;
A10: len f >= 2 by A2;
then
A11: 1+1 in Seg len f by FINSEQ_1:1;
then
A12: LSeg(f,1) = LSeg(p1,p) by A10,TOPREAL1:def 3;
Seg 2 c= Seg len f by A10,FINSEQ_1:5;
then f|2 = f|Seg 2 & dom f /\ Seg 2 = Seg 2 by A8,FINSEQ_1:def 16,XBOOLE_1:28
;
then
A13: dom(f|2) = Seg 2 by RELAT_1:61;
then
A14: 1 in dom(f|2) & 2 in dom(f|2) by FINSEQ_1:1;
thus
A15: L~h is_S-P_arc_joining p1,p by A6;
A16: L~(f|2) \/ LSeg(p,p) c= L~h
proof
let x be object such that
A17: x in L~(f|2) \/ LSeg(p,p);
now
per cases by A17,XBOOLE_0:def 3;
suppose
x in L~(f|2);
then consider X be set such that
A18: x in X and
A19: X in M by TARSKI:def 4;
consider m such that
A20: X=LSeg(f|2,m) and
A21: 1<=m and
A22: m+1<=len(f|2) by A19;
len(f|2) - 1 =1+1 - 1 by A13,FINSEQ_1:def 3
.= 1;
then m+1-1 <= 1 by A22,XREAL_1:9;
then m=1 by A21,XXREAL_0:1;
hence thesis by A11,A12,A9,A7,A14,A18,A20,TOPREAL3:17;
end;
suppose
x in LSeg(p,p);
then
A23: x in {p} by RLTOPSP1:70;
p in L~h by A15,Th3;
hence thesis by A23,TARSKI:def 1;
end;
end;
hence thesis;
end;
LSeg(f,1) c= L~f by TOPREAL3:19;
hence L~h c= L~f by A4,A12,A7,TOPREAL3:16;
len f >= 1 by A10,XXREAL_0:2;
then Seg 1 c= Seg len f by FINSEQ_1:5;
then f|1 = f|Seg 1 & dom f /\ Seg 1 = Seg 1 by A8,FINSEQ_1:def 16,XBOOLE_1:28
;
then dom(f|1) = Seg 1 by RELAT_1:61;
then len (f|1) = 1 by FINSEQ_1:def 3;
then L~(f|1)={} by TOPREAL1:22;
hence L~h = L~(f|1) \/ LSeg(p1,p) by A3,A5,A9,TOPREAL1:5,TOPREAL3:13;
A24: L~(f|2) c=L~(f|2) \/ LSeg(p,p) by XBOOLE_1:7;
A25: 1+1<=len(f|2) by A13,FINSEQ_1:def 3;
LSeg(f|2,1) = LSeg(p1,p) by A11,A12,A14,TOPREAL3:17;
then LSeg(p1,p) in M by A25;
then L~h c=L~(f|2) by A9,A7,ZFMISC_1:74;
then L~h c= L~(f|2) \/ LSeg(p,p) by A24;
hence thesis by A16;
end;
theorem Th15:
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 *> implies 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
set p1 = f/.1, p = f/.2;
assume that
A1: p<>p1 and
A2: f is being_S-Seq and
A3: p`1 = p1`1 and
A4: h = <* p1,|[p1`1,(p1`2+p`2)/2]|,p *>;
A5: p1`2 <> p`2 by A1,A3,TOPREAL3:6;
hence
A6: h is being_S-Seq & h/.1 = p1 & h/.len h = p by A3,A4,TOPREAL3:36;
A7: LSeg(p1,|[p1`1,(p1`2+p`2)/2]|) \/ LSeg(|[p1`1,(p1`2+p`2)/2]|,p) = LSeg(
p1,p) by A3,A5,TOPREAL1:5,TOPREAL3:14;
set M = {LSeg(f|2,k): 1<=k & k+1<=len(f|2)};
A8: Seg len f = dom f by FINSEQ_1:def 3;
A9: L~h = LSeg(p1,|[p1`1,(p1`2+p`2)/2]|) \/ LSeg(|[p1`1,(p1`2+p`2)/2]|,p)
by A4,TOPREAL3:16;
A10: len f >= 1+1 by A2;
then
A11: LSeg(f,1) = LSeg(p1,p) by TOPREAL1:def 3;
Seg 2 c= Seg len f by A10,FINSEQ_1:5;
then f|2 = f|Seg 2 & dom f /\ Seg 2 = Seg 2 by A8,FINSEQ_1:def 16,XBOOLE_1:28
;
then
A12: dom(f|2) = Seg 2 by RELAT_1:61;
then
A13: 1 in dom(f|2) & 2 in dom(f|2) by FINSEQ_1:1;
thus
A14: L~h is_S-P_arc_joining p1,p by A6;
A15: L~(f|2) \/ LSeg(p,p) c= L~h
proof
let x be object such that
A16: x in L~(f|2) \/ LSeg(p,p);
now
per cases by A16,XBOOLE_0:def 3;
suppose
x in L~(f|2);
then consider X be set such that
A17: x in X and
A18: X in M by TARSKI:def 4;
consider m such that
A19: X=LSeg(f|2,m) and
A20: 1<=m and
A21: m+1<=len(f|2) by A18;
len(f|2) - 1 =1+1 - 1 by A12,FINSEQ_1:def 3
.= 1;
then m+1-1 <= 1 by A21,XREAL_1:9;
then m=1 by A20,XXREAL_0:1;
hence thesis by A10,A11,A9,A7,A13,A17,A19,TOPREAL3:17;
end;
suppose
x in LSeg(p,p);
then
A22: x in {p} by RLTOPSP1:70;
p in L~h by A14,Th3;
hence thesis by A22,TARSKI:def 1;
end;
end;
hence thesis;
end;
LSeg(f,1) c= L~f by TOPREAL3:19;
hence L~h c= L~f by A4,A11,A7,TOPREAL3:16;
len f >= 1 by A10,XXREAL_0:2;
then Seg 1 c= Seg len f by FINSEQ_1:5;
then f|1 = f|Seg 1 & dom f /\ Seg 1 = Seg 1 by A8,FINSEQ_1:def 16,XBOOLE_1:28
;
then dom(f|1) = Seg 1 by RELAT_1:61;
then len (f|1) = 1 by FINSEQ_1:def 3;
then L~(f|1)={} by TOPREAL1:22;
hence L~h = L~(f|1) \/ LSeg(p1,p) by A3,A5,A9,TOPREAL1:5,TOPREAL3:14;
A23: L~(f|2) c=L~(f|2) \/ LSeg(p,p) by XBOOLE_1:7;
A24: 1+1<=len(f|2) by A12,FINSEQ_1:def 3;
LSeg(f|2,1) = LSeg(p1,p) by A10,A11,A13,TOPREAL3:17;
then LSeg(p1,p) in M by A24;
then L~h c=L~(f|2) by A9,A7,ZFMISC_1:74;
then L~h c= L~(f|2) \/ LSeg(p,p) by A23;
hence thesis by A15;
end;
theorem Th16:
f is being_S-Seq & i>2 & i in dom f & h = f|i implies 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
assume that
A1: f is being_S-Seq & i>2 and
A2: i in dom f and
A3: h = f|i;
A4: Seg len f = dom f by FINSEQ_1:def 3;
then i<=len f by A2,FINSEQ_1:1;
then
A5: Seg i c= Seg len f by FINSEQ_1:5;
h = f|Seg i by A3,FINSEQ_1:def 16;
then dom h=Seg(len f) /\ Seg i by A4,RELAT_1:61;
then
A6: dom h = Seg i by A5,XBOOLE_1:28;
1<=i by A2,A4,FINSEQ_1:1;
then
A7: 1 in dom h & i in dom h by A6,FINSEQ_1:1;
i in NAT by ORDINAL1:def 12;
then len h = i by A6,FINSEQ_1:def 3;
hence h is being_S-Seq & h/.1=f/.1 & h/.len h = f/.i by A1,A2,A3,A7,
FINSEQ_4:70,TOPREAL3:33;
hence L~h is_S-P_arc_joining f/.1,f/.i & L~h c= L~f by A3,TOPREAL3:20;
then f/.i in L~(f|i) by A3,Th3;
then LSeg(f/.i,f/.i) = {f/.i} & {f/.i} c= L~(f|i) by RLTOPSP1:70,ZFMISC_1:31;
hence thesis by A3,XBOOLE_1:12;
end;
theorem Th17:
p<>f/.1 & f is being_S-Seq & p in LSeg(f,n) implies ex h 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
set p1 = f/.1, q = f/.n;
assume that
A1: p<>p1 and
A2: f is being_S-Seq and
A3: p in LSeg(f,n);
A4: f is special by A2;
A5: n <= n+1 by NAT_1:11;
A6: now
assume
A7: not n in dom f or not n+1 in dom f;
now
per cases by A7;
suppose
not n in dom f;
then not(1 <= n & n <= len f) by FINSEQ_3:25;
then not(1 <= n & n+1 <= len f) by A5,XXREAL_0:2;
hence contradiction by A3,TOPREAL1:def 3;
end;
suppose
not n+1 in dom f;
then not(1 <= n+1 & n+1<= len f) by FINSEQ_3:25;
hence contradiction by A3,NAT_1:11,TOPREAL1:def 3;
end;
end;
hence contradiction;
end;
A8: f is one-to-one by A2;
A9: Seg len f=dom f by FINSEQ_1:def 3;
then
A10: 1<=n by A6,FINSEQ_1:1;
A11: n+1<=len f by A6,A9,FINSEQ_1:1;
A12: n<=len f by A6,A9,FINSEQ_1:1;
now
per cases;
case
f/.n = p & f/.(n+1) = p;
then n+1 = n by A6,A8,PARTFUN2:10;
hence contradiction;
end;
case
A13: f/.n = p & f/.(n+1) <> p;
then 1<n by A1,A10,XXREAL_0:1;
then
A14: 1+1<=n by NAT_1:13;
now
per cases by A14,XXREAL_0:1;
suppose
A15: n=1+1;
now
per cases by A4,A12,A13,A15;
suppose
A16: p1`1=p`1;
take h = <* p1,|[p1`1,(p1`2+p`2)/2]|,p *>;
thus h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A1,A2,A13
,A15,A16,Th15;
end;
suppose
A17: p1`2=p`2;
take h = <* p1,|[(p1`1+p`1)/2,p1`2]|,p *>;
thus h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A1,A2,A13
,A15,A17,Th14;
end;
end;
hence thesis;
end;
suppose
A18: n>2;
take h=f|n;
thus h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A2,A6,A13
,A18,Th16;
end;
end;
hence thesis;
end;
case
A19: f/.n <> p & f/.(n+1) = p;
now
per cases by A10,XXREAL_0:1;
suppose
A20: n=1;
now
per cases by A4,A11,A19,A20;
suppose
A21: p1`1= p`1;
take h=<* p1,|[p1`1,(p1`2+p`2)/2]|,p *>;
thus h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A2,A19,A20
,A21,Th15;
end;
suppose
A22: p1`2=p`2;
take h=<* p1,|[(p1`1+p`1)/2,p1`2]|,p *>;
thus h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A2,A19,A20
,A22,Th14;
end;
end;
hence thesis;
end;
suppose
A23: 1<n;
take h=f|(n+1);
1+1<n+1 by A23,XREAL_1:6;
hence h is being_S-Seq & h/.1=p1 & h/.len h=p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A2,A6,A19
,Th16,TOPREAL3:38;
end;
end;
hence thesis;
end;
case
A24: f/.n <> p & f/.(n+1) <> p;
now
per cases by A10,XXREAL_0:1;
suppose
A25: n=1;
set q1 = f/.(1+1);
A26: len f >= 1+1 by A2;
then
A27: LSeg(f,n) = LSeg(p1,q1) by A25,TOPREAL1:def 3;
now
per cases by A4,A26;
suppose
A28: p1`1=q1`1;
take h = <* p1,|[p1`1,(p1`2+p`2)/2]|,p *>;
p1`1 <= p`1 & p`1 <= q1`1 by A3,A27,A28,TOPREAL1:3;
then p1`1 = p`1 by A28,XXREAL_0:1;
hence h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A1,A2,A3
,A25,Th12;
end;
suppose
A29: p1`2=q1`2;
take h = <* p1,|[(p1`1+p`1)/2,p1`2]|,p *>;
p1`2 <= p`2 & p`2 <= q1`2 by A3,A27,A29,TOPREAL1:4;
then p1`2 = p`2 by A29,XXREAL_0:1;
hence h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h = L~(f|n) \/ LSeg(q,p) by A1,A2,A3
,A25,Th11;
end;
end;
hence thesis;
end;
suppose
A30: 1<n;
take h = (f|n)^<*p*>;
thus h is being_S-Seq & h/.1 = p1 & h/.len h = p & L~h
is_S-P_arc_joining p1,p & L~h c= L~f & L~h =L~(f|n) \/ LSeg(q,p) by A2,A3,A6
,A24,A30,Th13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th18:
p<>f/.1 & f is being_S-Seq & p in L~f implies ex h 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
set M = {LSeg(f,i): 1<=i & i+1<=len f}, p1 = f/.1;
assume that
A1: p<>p1 & f is being_S-Seq and
A2: p in L~f;
consider X be set such that
A3: p in X and
A4: X in M by A2,TARSKI:def 4;
consider n such that
A5: X=LSeg(f,n) and
1<=n and
n+1<=len f by A4;
consider h such that
A6: h is being_S-Seq & h/.1=p1 & h/.len h = p & L~h is_S-P_arc_joining
p1,p & L~h c= L~f and
L~h = L~(f|n) \/ LSeg(f/.n,p) by A1,A3,A5,Th17;
take h;
thus thesis by A6;
end;
theorem Th19:
( 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*> implies h is being_S-Seq & L~h
is_S-P_arc_joining f/.1,p & L~h c= L~f \/ Ball(u,r)
proof
set p1 = f/.1, p2 = f/.len f;
assume
A1: p`1=p2`1 & p`2<>p2`2 or p`1<>p2`1 & p`2=p2`2;
assume that
A2: p2 in Ball(u,r) & p in Ball(u,r) and
A3: f is being_S-Seq and
A4: LSeg(p2,p) /\ L~f = {p2} and
A5: h=f^<*p*>;
A6: not p in L~f by A1,A4,TOPREAL3:40;
A7: f is one-to-one by A3;
A8: f is unfolded by A3;
A9: f is one-to-one by A3;
A10: f is s.n.c. by A3;
A11: Seg len h = dom h by FINSEQ_1:def 3;
set Mf = {LSeg(f,i): 1<=i & i+1<=len f}, Mh = {LSeg(h,m): 1<=m & m+1<=len h};
A12: Seg len f = dom f by FINSEQ_1:def 3;
A13: 2<=len f by A3;
then
A14: 1<=len f by XXREAL_0:2;
then
A15: len f in dom f by A12,FINSEQ_1:1;
then
A16: h/.len f = p2 by A5,FINSEQ_4:68;
A17: len h = len f + len <*p*> by A5,FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
then
A18: h/.len h = p by A5,FINSEQ_4:67;
then
A19: LSeg(h,len f) = LSeg(p2,p) by A17,A14,A16,TOPREAL1:def 3;
A20: f is special by A3;
thus
A21: h is being_S-Seq
proof
now
set Z = {m where m is Nat: 1<=m & m<=len h};
given x,y being object such that
A22: x in dom h and
A23: y in dom h and
A24: h.x = h.y and
A25: x<>y;
y in Z by A11,A23,FINSEQ_1:def 1;
then consider k2 be Nat such that
A26: k2=y and
A27: 1<=k2 and
A28: k2<=len h;
x in Z by A11,A22,FINSEQ_1:def 1;
then consider k1 be Nat such that
A29: k1=x and
A30: 1<=k1 and
A31: k1<=len h;
A32: h/.k1 = h.y by A22,A24,A29,PARTFUN1:def 6
.= h/.k2 by A23,A26,PARTFUN1:def 6;
now
per cases by A17,A31,A28,XXREAL_0:1;
suppose
k1=len f+1 & k2=len f+1;
hence contradiction by A25,A29,A26;
end;
suppose
A33: k1=len f+1 & k2<len f+1;
then
A34: k2+1<=k1 by NAT_1:13;
now
per cases by A34,XXREAL_0:1;
suppose
k2 + 1 = k1;
hence contradiction by A1,A5,A16,A32,A33,FINSEQ_4:67;
end;
suppose
k2 + 1 < k1;
then
A35: k2<len f+1-1 by A33,XREAL_1:20;
reconsider k2 as Element of NAT by ORDINAL1:def 12;
k2 in dom f by A12,A27,A35,FINSEQ_1:1;
then h/.k2 = f/.k2 by A5,FINSEQ_4:68;
hence contradiction by A5,A13,A6,A27,A32,A33,A35,FINSEQ_4:67
,TOPREAL3:39;
end;
end;
hence contradiction;
end;
suppose
A36: k1<len f+1 & k2=len f+1;
then
A37: k1+1<=k2 by NAT_1:13;
now
per cases by A37,XXREAL_0:1;
suppose
k1 + 1 = k2;
hence contradiction by A1,A5,A16,A32,A36,FINSEQ_4:67;
end;
suppose
k1 + 1 < k2;
then
A38: k1<len f+1-1 by A36,XREAL_1:20;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
k1 in dom f by A12,A30,A38,FINSEQ_1:1;
then h/.k1 = f/.k1 by A5,FINSEQ_4:68;
hence contradiction by A5,A13,A6,A30,A32,A36,A38,FINSEQ_4:67
,TOPREAL3:39;
end;
end;
hence contradiction;
end;
suppose
A39: k1<len f+1 & k2<len f+1;
then k2<=len f by NAT_1:13;
then
A40: k2 in dom f by A12,A27,FINSEQ_1:1;
k1<=len f by A39,NAT_1:13;
then
A41: k1 in dom f by A12,A30,FINSEQ_1:1;
then f.k1 = h.k1 by A5,FINSEQ_1:def 7
.= f.k2 by A5,A24,A29,A26,A40,FINSEQ_1:def 7;
hence contradiction by A9,A25,A29,A26,A41,A40,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
hence h is one-to-one by FUNCT_1:def 4;
2+1<=len f +1 by A13,XREAL_1:6;
hence len h >= 2 by A17,XXREAL_0:2;
thus h is unfolded
proof
let j be Nat such that
A42: 1 <= j and
A43: j + 2 <= len h;
A44: j+(1+1) = j+1+1;
j+1 <= j+2 by XREAL_1:6;
then
A45: j+1 <= len h by A43,XXREAL_0:2;
now
per cases by A43,XXREAL_0:1;
suppose
A46: j+2 = len h;
then
A47: j+(1+1 - 1)= len f by A17;
then j<=len f by NAT_1:13;
then j in dom f by A12,A42,FINSEQ_1:1;
then
A48: LSeg(h,j) = LSeg(f,j) by A5,A15,A47,TOPREAL3:18;
LSeg(h,j) in Mf by A42,A47,A48;
then
A49: LSeg(h,j) = LSeg(h,j) /\ L~f by XBOOLE_1:28,ZFMISC_1:74;
h/.(j+1) in LSeg(h,j) by A42,A45,TOPREAL1:21;
then
A50: {h/.(j+1)} c= LSeg(h,j) by ZFMISC_1:31;
LSeg(h,j+1) = LSeg(p2,p) by A17,A14,A18,A16,A46,TOPREAL1:def 3;
hence
LSeg(h,j) /\ LSeg(h,j+1) = LSeg(h,j) /\ {h/.(j+1)} by A4,A17,A16,A46
,A49,XBOOLE_1:16
.= {h/.(j+1)} by A50,XBOOLE_1:28;
end;
suppose
j+2 < len h;
then
A51: j+(2+1)-1<=len f by A17,NAT_1:13;
then
A52: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A8,A42,A43;
1<=j+2 by A44,NAT_1:11;
then
A53: j+1+1 in dom f by A12,A51,FINSEQ_1:1;
j+1<=j+2 by A44,NAT_1:11;
then
A54: j+1<=len f by A51,XXREAL_0:2;
1<=j+1 by NAT_1:11;
then
A55: j+1 in dom f by A12,A54,FINSEQ_1:1;
then
A56: h/.(j+1) = f/.(j+1) by A5,FINSEQ_4:68;
j<=j+1 by NAT_1:11;
then j<=len f by A54,XXREAL_0:2;
then j in dom f by A12,A42,FINSEQ_1:1;
then LSeg(h,j) = LSeg(f,j) by A5,A55,TOPREAL3:18;
hence thesis by A5,A52,A55,A53,A56,TOPREAL3:18;
end;
end;
hence thesis;
end;
thus h is s.n.c.
proof
let n,m be Nat such that
A57: m>n+1;
n<=n+1 by NAT_1:11;
then
A58: n<=m by A57,XXREAL_0:2;
A59: n+1+1=n+(1+1);
A60: 1<=n+1 by NAT_1:11;
LSeg(f,n) misses LSeg(f,m) by A10,A57;
then
A61: LSeg(f,n) /\ LSeg(f,m) = {};
now
per cases by XXREAL_0:1;
suppose
A62: m+1<len h;
then
A63: m+1<=len f by A17,NAT_1:13;
A64: 1<m by A57,A60,XXREAL_0:2;
then 1<=m+1 by NAT_1:13;
then
A65: m+1 in dom f by A12,A63,FINSEQ_1:1;
A66: m<=len f by A17,A62,XREAL_1:6;
then m in dom f by A12,A64,FINSEQ_1:1;
then
A67: LSeg(h,m)=LSeg(f,m) by A5,A65,TOPREAL3:18;
now
per cases;
suppose
0<n;
then
A68: 0+1<=n by NAT_1:13;
n+1<=len f by A57,A66,XXREAL_0:2;
then
A69: n+1 in dom f by A12,A60,FINSEQ_1:1;
n<=len f by A58,A66,XXREAL_0:2;
then n in dom f by A12,A68,FINSEQ_1:1;
hence LSeg(h,n) /\ LSeg(h,m) = {} by A5,A61,A67,A69,TOPREAL3:18;
end;
suppose
0=n;
then LSeg(h,n)={} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
A70: m+1=len h;
now
per cases;
suppose
A71: 0<n;
A72: n+1 in dom f by A17,A12,A57,A60,A70,FINSEQ_1:1;
A73: 0+1<=n by A71,NAT_1:13;
then n in dom f by A17,A12,A58,A70,FINSEQ_1:1;
then
A74: LSeg(h,n)=LSeg(f,n) by A5,A72,TOPREAL3:18;
now
set L = LSeg(f,n);
set x = the Element of LSeg(h,n) /\ LSeg(h,m);
assume
A75: LSeg(h,n) /\ LSeg(h,m) <> {};
then
A76: x in L by A74,XBOOLE_0:def 4;
A77: x in LSeg(p2,p) by A17,A19,A70,A75,XBOOLE_0:def 4;
L in Mf by A17,A57,A70,A73;
then x in L~f by A76,TARSKI:def 4;
then x in {p2} by A4,A77,XBOOLE_0:def 4;
then
A78: x=p2 by TARSKI:def 1;
A79: n+1+1<=len f by A17,A57,A70,NAT_1:13;
now
per cases by A79,XXREAL_0:1;
suppose
A80: n+1+1 = len f;
1 <= n+1 by NAT_1:11;
then
A81: p2 in LSeg(f,n+1) by A80,TOPREAL1:21;
LSeg(f,n) /\ LSeg(f,n+1) = {f/.(n+ 1)} by A8,A59,A73,A80;
then p2 in {f/.(n+1)} by A76,A78,A81,XBOOLE_0:def 4;
then f/.len f=f/.(n+1) by TARSKI:def 1;
then len f + 1 = len f by A15,A7,A72,A80,PARTFUN2:10;
hence contradiction;
end;
suppose
A82: n+1+1<len f;
reconsider j=len f - 1 as Element of NAT by A13,INT_1:5
,XXREAL_0:2;
n+2+1<=len f by A82,NAT_1:13;
then n+2<=len f - 1 by XREAL_1:19;
then n+1<j by A59,NAT_1:13;
then LSeg(f,n) misses LSeg(f,j) by A10;
then
A83: LSeg(f,n) /\ LSeg(f,j) = {};
(1+1)-1 = 1;
then j+1 = len f & 1<=j by A13,XREAL_1:13;
then p2 in LSeg(f,j) by TOPREAL1:21;
hence contradiction by A76,A78,A83,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
0=n;
then LSeg(h,n)={} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
suppose
m+1>len h;
then LSeg(h,m) = {} by TOPREAL1:def 3;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
end;
hence LSeg(h,n) /\ LSeg(h,m) = {};
end;
hereby
let n be Nat such that
A84: 1 <= n and
A85: n + 1 <= len h;
set p3 = h/.n, p4 = h/.(n+1);
now
per cases by A85,XXREAL_0:1;
suppose
n+1 = len h;
hence p3`1=p4`1 or p3`2=p4`2 by A1,A5,A17,A16,FINSEQ_4:67;
end;
suppose
A86: n+1 < len h;
A87: 1<=n+1 by A84,NAT_1:13;
n+1<=len f by A17,A86,NAT_1:13;
then n+1 in dom f by A12,A87,FINSEQ_1:1;
then
A88: p4=f/.(n+1) by A5,FINSEQ_4:68;
n<=len f by A17,A86,XREAL_1:6;
then n in dom f by A12,A84,FINSEQ_1:1;
then
A89: p3=f/.n by A5,FINSEQ_4:68;
n+1<= len f by A17,A86,NAT_1:13;
hence p3`1 = p4`1 or p3`2 = p4`2 by A20,A84,A89,A88;
end;
end;
hence p3`1 = p4`1 or p3`2 = p4`2;
end;
end;
1 in dom f by A12,A14,FINSEQ_1:1;
then h/.1 = p1 by A5,FINSEQ_4:68;
hence L~h is_S-P_arc_joining p1,p by A18,A21;
let x be object;
assume x in L~h;
then consider X be set such that
A90: x in X and
A91: X in Mh by TARSKI:def 4;
consider k such that
A92: X=LSeg(h,k) and
A93: 1<=k and
A94: k+1<=len h by A91;
per cases by A94,XXREAL_0:1;
suppose
A95: k+1 = len h;
A96: Ball(u,r) c= L~f \/ Ball(u,r) by XBOOLE_1:7;
X c= Ball(u,r) by A2,A17,A19,A92,A95,TOPREAL3:21;
hence thesis by A90,A96;
end;
suppose
k+1 < len h;
then
A97: k+1<=len f by A17,NAT_1:13;
k<=k+1 by NAT_1:11;
then k<=len f by A97,XXREAL_0:2;
then
A98: k in dom f by A12,A93,FINSEQ_1:1;
1<=k+1 by A93,NAT_1:13;
then k+1 in dom f by A12,A97,FINSEQ_1:1;
then X=LSeg(f,k) by A5,A92,A98,TOPREAL3:18;
then X in Mf by A93,A97;
then x in union Mf by A90,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th20:
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} implies L~h is_S-P_arc_joining f/.1,p & L~
h c= L~f \/ Ball(u,r)
proof
set p1 = f/.1, p2 = f/.len f;
assume that
A1: p2 in Ball(u,r) and
A2: p in Ball(u,r) and
A3: |[p`1,p2`2]| in Ball(u,r) and
A4: f is being_S-Seq and
A5: p`1<>p2`1 and
A6: p`2<>p2`2 and
A7: h=f^<*|[p`1,p2`2]|,p*> and
A8: (LSeg(p2,|[p`1,p2`2]|) \/ LSeg(|[p`1,p2`2]|,p)) /\ L~f = {p2};
set p3 = |[p`1,p2`2]|, f1 = f^<* p3 *>, h1 = f1^<* p *>;
reconsider Lf = L~f as non empty Subset of TOP-REAL 2 by A8;
A9: p2 in LSeg(p2,p3) by RLTOPSP1:68;
L~f is_S-P_arc_joining p1,p2 by A4;
then Lf is_an_arc_of p1,p2 by Th2;
then p2 in L~f by TOPREAL1:1;
then p2 in LSeg(p2,p3) /\ L~f by A9,XBOOLE_0:def 4;
then
A10: LSeg(p2,p3) /\ L~f c= (LSeg(p2,p3) /\ L~f) \/ (LSeg(p3,p) /\ L~f) & {p2
} c= LSeg(p2,p3) /\ L~f by XBOOLE_1:7,ZFMISC_1:31;
{p2} = (LSeg(p2,p3) /\ L~f) \/ (LSeg(p3,p) /\ L~f) by A8,XBOOLE_1:23;
then
A11: LSeg(p2,p3) /\ L~f = {p2} by A10;
A12: len f1 = len f + len <*p3*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
then
A13: f1/.len f1 = p3 by FINSEQ_4:67;
A14: p=|[p`1,p`2]| by EUCLID:53;
A15: Seg len f = dom f by FINSEQ_1:def 3;
len f>=2 by A4;
then
A16: 1<=len f by XXREAL_0:2;
then len f in dom f by A15,FINSEQ_1:1;
then
A17: f1/.len f = p2 by FINSEQ_4:68;
A18: LSeg(p3,p) /\ L~f1 c= {p3}
proof
set M1 = {LSeg(f1,i): 1<=i & i+1<=len f1}, Mf = {LSeg(f,j): 1<=j & j+1<=
len f};
assume not thesis;
then consider x being object such that
A19: x in LSeg(p3,p) /\ L~f1 and
A20: not x in {p3};
x in L~f1 by A19,XBOOLE_0:def 4;
then consider X be set such that
A21: x in X and
A22: X in M1 by TARSKI:def 4;
consider k such that
A23: X=LSeg(f1,k) and
A24: 1<=k and
A25: k+1<=len f1 by A22;
A26: x in LSeg(p3,p) by A19,XBOOLE_0:def 4;
now
per cases by A25,XXREAL_0:1;
suppose
k+1 = len f1;
then LSeg(f1,k) = LSeg(p2,p3) by A12,A13,A17,A24,TOPREAL1:def 3;
then x in LSeg(p2,p3) /\ LSeg(p3,p) by A26,A21,A23,XBOOLE_0:def 4;
hence contradiction by A20,TOPREAL3:30;
end;
suppose
k+1 < len f1;
then
A27: k+1<=len f by A12,NAT_1:13;
k<=k+1 by NAT_1:11;
then k<=len f by A27,XXREAL_0:2;
then
A28: k in dom f by A15,A24,FINSEQ_1:1;
1<=k+1 by A24,NAT_1:13;
then k+1 in dom f by A15,A27,FINSEQ_1:1;
then X=LSeg(f,k) by A23,A28,TOPREAL3:18;
then X in Mf by A24,A27;
then
A29: x in L~f by A21,TARSKI:def 4;
x in LSeg(p2,p3) \/ LSeg(p3,p) by A26,XBOOLE_0:def 3;
then x in {p2} by A8,A29,XBOOLE_0:def 4;
then x = p2 by TARSKI:def 1;
hence contradiction by A5,A14,A26,TOPREAL3:11;
end;
end;
hence contradiction;
end;
A30: h1 = f^(<*p3*>^<*p*>) by FINSEQ_1:32
.= h by A7,FINSEQ_1:def 9;
A31: p3`2 = p2`2 & p3`1 = p`1 by EUCLID:52;
then
A32: f1 is being_S-Seq by A1,A3,A4,A5,A11,Th19;
A33: L~f1 is_S-P_arc_joining p1,p3 by A1,A3,A4,A5,A31,A11,Th19;
then reconsider Lf1 = L~f1 as non empty Subset of TOP-REAL 2 by Th1,
TOPREAL1:26;
A34: p3 in LSeg(p3,p) by RLTOPSP1:68;
A35: f1/.len f1=p3 by A12,FINSEQ_4:67;
L~f1 c= L~f \/ Ball(u,r) by A1,A3,A4,A5,A31,A11,Th19;
then L~f1 \/ Ball(u,r) c= L~f \/ Ball(u,r) \/ Ball(u,r) by XBOOLE_1:9;
then
A36: L~f1 \/ Ball(u,r) c= L~f \/ (Ball(u,r) \/ Ball(u,r)) by XBOOLE_1:4;
A37: p`1=p3`1 & p`2<>p3`2 or p`1<>p3`1 & p`2=p3`2 by A6,EUCLID:52;
Lf1 is_an_arc_of p1,p3 by A33,Th2;
then p3 in L~f1 by TOPREAL1:1;
then p3 in LSeg(p3,p) /\ L~f1 by A34,XBOOLE_0:def 4;
then {p3} c= LSeg(p3,p) /\ L~f1 by ZFMISC_1:31;
then
A38: LSeg(p3,p) /\ L~f1 = {p3} by A18;
1 in dom f by A15,A16,FINSEQ_1:1;
then f1/.1=p1 by FINSEQ_4:68;
hence L~h is_S-P_arc_joining p1,p by A2,A3,A37,A32,A35,A38,A30,Th19;
L~h1 c= L~f1 \/ Ball(u,r) by A2,A3,A37,A32,A35,A38,Th19;
hence thesis by A30,A36;
end;
theorem Th21:
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} implies L~h is_S-P_arc_joining f/.1,p & L~h
c= L~f \/ Ball(u,r)
proof
set p1 = f/.1, p2 = f/.len f;
assume that
A1: p2 in Ball(u,r) and
A2: p in Ball(u,r) and
A3: |[p2`1,p`2]| in Ball(u,r) and
A4: f is being_S-Seq and
A5: p`1<>p2`1 and
A6: p`2<>p2`2 and
A7: h=f^<*|[p2`1,p`2]|,p*> and
A8: (LSeg(p2,|[p2`1,p`2]|) \/ LSeg(|[p2`1,p`2]|,p)) /\ L~f = {p2};
set p3 = |[p2`1,p`2]|, f1 = f^<* p3 *>, h1 = f1^<* p *>;
reconsider Lf = L~f as non empty Subset of TOP-REAL 2 by A8;
A9: p2 in LSeg(p2,p3) by RLTOPSP1:68;
L~f is_S-P_arc_joining p1,p2 by A4;
then Lf is_an_arc_of p1,p2 by Th2;
then p2 in L~f by TOPREAL1:1;
then p2 in LSeg(p2,p3) /\ L~f by A9,XBOOLE_0:def 4;
then
A10: LSeg(p2,p3) /\ L~f c= (LSeg(p2,p3) /\ L~f) \/ (LSeg(p3,p) /\ L~f) & {p2
} c= LSeg(p2,p3) /\ L~f by XBOOLE_1:7,ZFMISC_1:31;
{p2} = (LSeg(p2,p3) /\ L~f) \/ (LSeg(p3,p) /\ L~f) by A8,XBOOLE_1:23;
then
A11: LSeg(p2,p3) /\ L~f = {p2} by A10;
A12: len f1 = len f + len <*p3*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
then
A13: f1/.len f1 = p3 by FINSEQ_4:67;
A14: p=|[p`1,p`2]| by EUCLID:53;
A15: Seg len f = dom f by FINSEQ_1:def 3;
len f>=2 by A4;
then
A16: 1<=len f by XXREAL_0:2;
then len f in dom f by A15,FINSEQ_1:1;
then
A17: f1/.len f = p2 by FINSEQ_4:68;
A18: LSeg(p3,p) /\ L~f1 c= {p3}
proof
set M1 = {LSeg(f1,i): 1<=i & i+1<=len f1}, Mf = {LSeg(f,j): 1<=j & j+1<=
len f};
assume not thesis;
then consider x being object such that
A19: x in LSeg(p3,p) /\ L~f1 and
A20: not x in {p3};
x in L~f1 by A19,XBOOLE_0:def 4;
then consider X be set such that
A21: x in X and
A22: X in M1 by TARSKI:def 4;
consider k such that
A23: X=LSeg(f1,k) and
A24: 1<=k and
A25: k+1<=len f1 by A22;
A26: x in LSeg(p3,p) by A19,XBOOLE_0:def 4;
now
per cases by A25,XXREAL_0:1;
suppose
k+1 = len f1;
then LSeg(f1,k) = LSeg(p2,p3) by A12,A13,A17,A24,TOPREAL1:def 3;
then x in LSeg(p2,p3) /\ LSeg(p3,p) by A26,A21,A23,XBOOLE_0:def 4;
hence contradiction by A20,TOPREAL3:29;
end;
suppose
k+1 < len f1;
then
A27: k+1<=len f by A12,NAT_1:13;
k<=k+1 by NAT_1:11;
then k<=len f by A27,XXREAL_0:2;
then
A28: k in dom f by A15,A24,FINSEQ_1:1;
1<=k+1 by A24,NAT_1:13;
then k+1 in dom f by A15,A27,FINSEQ_1:1;
then X=LSeg(f,k) by A23,A28,TOPREAL3:18;
then X in Mf by A24,A27;
then
A29: x in L~f by A21,TARSKI:def 4;
x in LSeg(p2,p3) \/ LSeg(p3,p) by A26,XBOOLE_0:def 3;
then x in {p2} by A8,A29,XBOOLE_0:def 4;
then x = p2 by TARSKI:def 1;
hence contradiction by A6,A14,A26,TOPREAL3:12;
end;
end;
hence contradiction;
end;
A30: h1 = f^(<*p3*>^<*p*>) by FINSEQ_1:32
.= h by A7,FINSEQ_1:def 9;
A31: p3`2 = p`2 & p3`1 = p2`1 by EUCLID:52;
then
A32: f1 is being_S-Seq by A1,A3,A4,A6,A11,Th19;
A33: L~f1 is_S-P_arc_joining p1,p3 by A1,A3,A4,A6,A31,A11,Th19;
then reconsider Lf1 = L~f1 as non empty Subset of TOP-REAL 2 by Th1,
TOPREAL1:26;
A34: p3 in LSeg(p3,p) by RLTOPSP1:68;
A35: f1/.len f1=p3 by A12,FINSEQ_4:67;
L~f1 c= L~f \/ Ball(u,r) by A1,A3,A4,A6,A31,A11,Th19;
then L~f1 \/ Ball(u,r) c= L~f \/ Ball(u,r) \/ Ball(u,r) by XBOOLE_1:9;
then
A36: L~f1 \/ Ball(u,r) c= L~f \/ (Ball(u,r) \/ Ball(u,r)) by XBOOLE_1:4;
A37: p`1=p3`1 & p`2<>p3`2 or p`1<>p3`1 & p`2=p3`2 by A5,EUCLID:52;
Lf1 is_an_arc_of p1,p3 by A33,Th2;
then p3 in L~f1 by TOPREAL1:1;
then p3 in LSeg(p3,p) /\ L~f1 by A34,XBOOLE_0:def 4;
then {p3} c= LSeg(p3,p) /\ L~f1 by ZFMISC_1:31;
then
A38: LSeg(p3,p) /\ L~f1 = {p3} by A18;
1 in dom f by A15,A16,FINSEQ_1:1;
then f1/.1=p1 by FINSEQ_4:68;
hence L~h is_S-P_arc_joining p1,p by A2,A3,A37,A32,A35,A38,A30,Th19;
L~h1 c= L~f1 \/ Ball(u,r) by A2,A3,A37,A32,A35,A38,Th19;
hence thesis by A30,A36;
end;
theorem Th22:
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 implies ex h st L~h is_S-P_arc_joining f/.1,p &
L~h c= L~f \/ Ball(u,r)
proof
set p1 = f/.1;
set Mf= {LSeg(f,k):1<=k & k+1<=len f};
assume that
A1: not p1 in Ball(u,r) and
A2: f/.len f in Ball(u,r) and
A3: p in Ball(u,r) and
A4: f is being_S-Seq and
A5: not p in L~f;
A6: f is special by A4;
defpred X[Nat] means 1<=$1 & $1<=len f - 1 & LSeg(f,$1) meets Ball(u,r);
A7: len f>= 2 by A4;
then reconsider n=len f - 1 as Element of NAT by INT_1:5,XXREAL_0:2;
2=1+1;
then
A8: 1<=len f - 1 by A7,XREAL_1:19;
n+1=len f;
then f/.len f in LSeg(f,n) by A8,TOPREAL1:21;
then LSeg(f,n) meets Ball(u,r) by A2,XBOOLE_0:3;
then
A9: ex n be Nat st X[n] by A8;
consider m be Nat such that
A10: X[m] and
A11: for i be Nat st X[i] holds m<=i from NAT_1:sch 5(A9);
reconsider m as Element of NAT by ORDINAL1:def 12;
consider q1,q2 such that
A12: f/.m = q1 and
A13: f/.(m+1) = q2;
A14: LSeg(f,m) /\ Ball(u,r) <> {} by A10,XBOOLE_0:def 7;
A15: m+1<=len f by A10,XREAL_1:19;
then
A16: LSeg(f,m) = LSeg(q1,q2) by A10,A12,A13,TOPREAL1:def 3;
m<=m+1 by NAT_1:11;
then
A17: m<=len f by A15,XXREAL_0:2;
A18: Seg len f=dom f by FINSEQ_1:def 3;
A19: now
set x = the Element of Ball(u,r) /\ L~(f|m);
set M = {LSeg(f|m,i):1<=i & i+1<=len(f|m)};
A20: Seg len(f|m) = dom(f |m ) by FINSEQ_1:def 3;
assume
A21: Ball(u,r) /\ L~(f|m) <> {};
then
A22: x in Ball(u,r) by XBOOLE_0:def 4;
x in L~(f|m) by A21,XBOOLE_0:def 4;
then consider X be set such that
A23: x in X and
A24: X in M by TARSKI:def 4;
consider k such that
A25: X=LSeg(f|m,k) and
A26: 1<=k and
A27: k+1<=len(f|m) by A24;
k<=k+1 by NAT_1:11;
then k<=len(f|m) by A27,XXREAL_0:2;
then
A28: k in Seg len(f|m) by A26,FINSEQ_1:1;
1<=k+1 by NAT_1:11;
then k+1 in Seg len(f|m) by A27,FINSEQ_1:1;
then x in LSeg(f,k) by A23,A25,A28,A20,TOPREAL3:17;
then
A29: LSeg(f,k) meets Ball(u,r) by A22,XBOOLE_0:3;
Seg m c= Seg len f by A17,FINSEQ_1:5;
then
A30: Seg m = dom f /\ (Seg m) by A18,XBOOLE_1:28
.= dom(f|(Seg m)) by RELAT_1:61
.= Seg len(f|m) by A20,FINSEQ_1:def 16;
A31: k+1-1 <= len(f|m)-1 by A27,XREAL_1:9;
then
A32: k<=m-1 by A30,FINSEQ_1:6;
m = len(f|m) by A30,FINSEQ_1:6;
then len(f|m) -1<=len f - 1 by A17,XREAL_1:9;
then k<=len f - 1 by A31,XXREAL_0:2;
then m<=k by A11,A26,A29;
then m<=m-1 by A32,XXREAL_0:2;
then 0<=m+-1-m by XREAL_1:48;
hence contradiction;
end;
for i st 1<=i<=len f - 1 & LSeg(f,i) /\ Ball(u,r) <> {}
holds m<=i by A11,XBOOLE_0:def 7;
then
A33: not q1 in Ball(u,r) by A1,A10,A12,TOPREAL3:26;
set A=LSeg(f,m) /\ Ball(u,r);
A34: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
m+1 <= n+1 by A10,XREAL_1:6;
then LSeg(f,m) in Mf by A10;
then
A35: LSeg(f,m) c= union Mf by ZFMISC_1:74;
now
per cases;
suppose
ex q st q in A & (p`1=q`1 or p`2=q`2);
then consider q such that
A36: q in A and
A37: p`1=q`1 or p`2=q`2;
A38: q in Ball(u,r) by A36,XBOOLE_0:def 4;
A39: q in LSeg(q,p) by RLTOPSP1:68;
A40: q in LSeg(f,m) by A36,XBOOLE_0:def 4;
then consider h such that
A41: h is being_S-Seq and
A42: h/.1=p1 and
A43: h/.len h=q and
A44: L~h is_S-P_arc_joining p1,q and
A45: L~h c= L~f and
A46: L~h = L~(f|m) \/ LSeg(q1,q) by A1,A4,A12,A38,Th17;
take g = h^<* p *>;
A47: L~h \/ Ball(u,r) c= L~f \/ Ball(u,r) by A45,XBOOLE_1:9;
A48: q in L~f by A35,A40;
A49: now
per cases by A37;
suppose
p`1=q`1;
hence p`1=q`1 & p`2<>q`2 or p`1<>q`1 & p`2=q`2 by A5,A48,TOPREAL3:6;
end;
suppose
p`2=q`2;
hence p`1=q`1 & p`2<>q`2 or p`1<>q`1 & p`2=q`2 by A5,A48,TOPREAL3:6;
end;
end;
A50: LSeg(q,p) /\ L~h c= {q}
proof
A51: now
per cases by A6,A10,A15,A12,A13;
suppose
q1`1=q2`1;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A40,TOPREAL3:11;
end;
suppose
q1`2=q2`2;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A40,TOPREAL3:12;
end;
end;
LSeg(q,p) = LSeg(q,p) /\ Ball(u,r) by A3,A38,TOPREAL3:21,XBOOLE_1:28;
then
A52: LSeg(q,p) /\ (L~(f|m) \/ LSeg(q1,q)) = LSeg(q,p) /\ Ball(u,r) /\
L~(f|m) \/ LSeg(q,p) /\ LSeg(q1,q) by XBOOLE_1:23
.= LSeg(q,p) /\(Ball(u,r) /\ L~(f|m))\/ LSeg(q,p) /\ LSeg(q1,q) by
XBOOLE_1:16
.= LSeg(q1,q) /\ LSeg(q,p) by A19;
A53: now
q1 in LSeg(q1,q2) by RLTOPSP1:68;
then
A54: LSeg(q1,q) c= LSeg(f,m) by A16,A40,TOPREAL1:6;
assume p in LSeg(q1,q);
hence contradiction by A5,A35,A54;
end;
let x be object;
assume x in LSeg(q,p) /\ L~h;
hence thesis by A3,A33,A38,A49,A46,A52,A53,A51,TOPREAL3:42;
end;
q in L~h by A44,Th3;
then q in LSeg(q,p) /\ L~h by A39,XBOOLE_0:def 4;
then {q} c= LSeg(q,p) /\ L~h by ZFMISC_1:31;
then
A55: LSeg(q,p) /\ L~h = {q} by A50;
then L~g c=L~h \/ Ball(u,r) by A3,A38,A49,A41,A43,Th19;
hence L~g is_S-P_arc_joining p1,p & L~g c=L~f \/ Ball(u,r) by A3,A38,A49
,A41,A42,A43,A55,A47,Th19;
end;
suppose
A56: for q st q in A holds p`1<>q`1 & p`2<>q`2;
set x = the Element of A;
A57: x in LSeg(f,m) by A14,XBOOLE_0:def 4;
then reconsider q=x as Point of TOP-REAL 2;
A58: q`1<>p`1 & q`2<>p`2 by A14,A56;
q <> p1 by A1,A14,XBOOLE_0:def 4;
then consider h such that
A59: h is being_S-Seq and
A60: h/.1=p1 and
A61: h/.len h=q and
A62: L~h is_S-P_arc_joining p1,q and
A63: L~h c= L~f and
A64: L~h = L~(f|m) \/ LSeg(q1,q) by A4,A12,A57,Th17;
A65: q in Ball(u,r) by A14,XBOOLE_0:def 4;
A66: q=|[q`1,q`2]| & p=|[p`1,p`2]| by EUCLID:53;
now
per cases by A3,A65,A66,TOPREAL3:25;
suppose
A67: |[q`1,p`2]| in Ball(u,r);
set v = |[q`1,p`2]|;
A68: (LSeg(q,v) \/ LSeg(v,p)) /\ L~h c= {q}
proof
let x be object;
set L = LSeg(q,v) \/ LSeg(v,p);
assume
A69: x in L /\ L~h;
LSeg(q,v) c=Ball(u,r) & LSeg(v,p) c=Ball(u,r) by A3,A65,A67,
TOPREAL3:21;
then L = L /\ Ball(u,r) by XBOOLE_1:8,28;
then
A70: L /\ (L~(f|m) \/ LSeg(q1,q)) = L /\ Ball(u,r) /\ L~(f|m) \/
L /\ LSeg( q1,q) by XBOOLE_1:23
.= L /\ (Ball(u,r) /\ L~(f|m)) \/ L /\ LSeg(q1,q) by XBOOLE_1:16
.= {} \/ L /\ LSeg(q1,q) by A19;
A71: now
per cases by A6,A10,A15,A12,A13;
suppose
q1`1=q2`1;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A57,TOPREAL3:11;
end;
suppose
q1`2=q2`2;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A57,TOPREAL3:12;
end;
end;
now
per cases by A71;
suppose
A72: q1`1 = q`1;
now
q1 in LSeg(q1,q2) by RLTOPSP1:68;
then
A73: LSeg(q1,q) c= LSeg(f,m) by A16,A57,TOPREAL1:6;
A74: v`2=p`2 by EUCLID:52;
assume v in LSeg(q1,q);
then v in LSeg(f,m) /\ Ball(u,r) by A67,A73,XBOOLE_0:def 4;
hence contradiction by A56,A74;
end;
hence thesis by A33,A65,A58,A64,A67,A70,A69,A72,TOPREAL3:43;
end;
suppose
q1`2 = q`2;
hence thesis by A14,A56,A64,A70,A69,TOPREAL3:27;
end;
end;
hence thesis;
end;
take g = h^<* |[q`1,p`2]|,p *>;
q in LSeg(q,v) by RLTOPSP1:68;
then
A75: q in (LSeg(q,v) \/ LSeg(v,p)) by XBOOLE_0:def 3;
A76: L~h \/ Ball(u,r) c= L~f \/ Ball(u,r) by A63,XBOOLE_1:9;
q in L~h by A62,Th3;
then q in (LSeg(q,v) \/ LSeg(v,p)) /\ L~h by A75,XBOOLE_0:def 4;
then {q} c= (LSeg(q,v) \/ LSeg(v,p)) /\ L~h by ZFMISC_1:31;
then
A77: (LSeg(q,|[q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,p)) /\ L~h={q} by A68;
then L~g c= L~h \/ Ball(u,r) by A3,A65,A58,A59,A61,A67,Th21;
hence
L~g is_S-P_arc_joining p1,p & L~g c=L~f \/ Ball(u,r) by A3,A65,A58
,A59,A60,A61,A67,A77,A76,Th21;
end;
suppose
A78: |[p`1,q`2]| in Ball(u,r);
set v = |[p`1,q`2]|;
A79: (LSeg(q,v) \/ LSeg(v,p)) /\ L~h c= {q}
proof
let x be object;
set L = LSeg(q,v) \/ LSeg(v,p);
assume
A80: x in L /\ L~h;
LSeg(q,v) c=Ball(u,r) & LSeg(v,p) c= Ball(u,r) by A3,A65,A78,
TOPREAL3:21;
then L = L /\ Ball(u,r) by XBOOLE_1:8,28;
then
A81: L /\ (L~(f|m) \/ LSeg(q1,q)) = L /\ Ball(u,r) /\ L~(f|m) \/
L /\ LSeg(q1,q) by XBOOLE_1:23
.= L /\ (Ball(u,r) /\ L~(f|m)) \/ L /\ LSeg(q1,q) by XBOOLE_1:16
.= {} \/ L /\ LSeg(q1,q) by A19;
A82: now
per cases by A6,A10,A15,A12,A13;
suppose
q1`1=q2`1;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A57,TOPREAL3:11;
end;
suppose
q1`2=q2`2;
hence q1`1 = q`1 or q1`2=q`2 by A34,A16,A57,TOPREAL3:12;
end;
end;
now
per cases by A82;
suppose
q1`1 = q`1;
hence thesis by A14,A56,A64,A81,A80,TOPREAL3:28;
end;
suppose
A83: q1`2 = q`2;
now
q1 in LSeg(q1,q2) by RLTOPSP1:68;
then
A84: LSeg(q1,q) c= LSeg(f,m) by A16,A57,TOPREAL1:6;
A85: v`1=p`1 by EUCLID:52;
assume v in LSeg(q1,q);
then v in LSeg(f,m) /\ Ball(u,r) by A78,A84,XBOOLE_0:def 4;
hence contradiction by A56,A85;
end;
hence thesis by A33,A65,A58,A64,A78,A81,A80,A83,TOPREAL3:44;
end;
end;
hence thesis;
end;
take g = h^<* |[p`1,q`2]|,p *>;
q in LSeg(q,v) by RLTOPSP1:68;
then
A86: q in (LSeg(q,v) \/ LSeg(v,p)) by XBOOLE_0:def 3;
A87: L~h \/ Ball(u,r) c= L~f \/ Ball(u,r) by A63,XBOOLE_1:9;
q in L~h by A62,Th3;
then q in (LSeg(q,v) \/ LSeg(v,p)) /\ L~h by A86,XBOOLE_0:def 4;
then {q} c= (LSeg(q,v) \/ LSeg(v,p)) /\ L~h by ZFMISC_1:31;
then
A88: (LSeg(q,|[p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,p)) /\ L~h={q} by A79;
then L~g c= L~h \/ Ball(u,r) by A3,A65,A58,A59,A61,A78,Th20;
hence
L~g is_S-P_arc_joining p1,p & L~g c=L~f \/ Ball(u,r) by A3,A65,A58
,A59,A60,A61,A78,A88,A87,Th20;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th23:
for R,p,p1,p2,P,r,u 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 ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p1,p & P1 c= R
proof
let R,p,p1,p2,P,r,u;
assume that
A1: p<>p1 and
A2: P is_S-P_arc_joining p1,p2 and
A3: P c= R and
A4: p in Ball(u,r) and
A5: p2 in Ball(u,r) and
A6: Ball(u,r) c= R;
consider f such that
A7: f is being_S-Seq and
A8: P = L~f and
A9: p1=f/.1 and
A10: p2=f/.len f by A2;
now
per cases;
suppose
p1 in Ball(u,r);
then consider P1 such that
A11: P1 is_S-P_arc_joining p1,p & P1 c= Ball(u,r) by A1,A4,Th10;
reconsider P1 as Subset of TOP-REAL 2;
take P1;
thus P1 is_S-P_arc_joining p1,p & P1 c= R by A6,A11;
end;
suppose
A12: not p1 in Ball(u,r);
now
per cases;
suppose
p in P;
then consider h such that
h is being_S-Seq and
h/.1=p1 and
h/.len h=p and
A13: L~h is_S-P_arc_joining p1,p & L~h c= L~f by A1,A7,A8,A9,Th18;
reconsider P1=L~h as Subset of TOP-REAL 2;
take P1;
thus P1 is_S-P_arc_joining p1,p & P1 c= R by A3,A8,A13;
end;
suppose
not p in P;
then consider h such that
A14: L~h is_S-P_arc_joining p1,p and
A15: L~h c= L~f \/ Ball(u,r) by A4,A5,A7,A8,A9,A10,A12,Th22;
reconsider P1=L~h as Subset of TOP-REAL 2;
take P1;
thus P1 is_S-P_arc_joining p1,p by A14;
L~f \/ Ball(u,r) c= R by A3,A6,A8,XBOOLE_1:8;
hence P1 c= R by A15;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm1: TopSpaceMetr(Euclid 2)=the TopStruct of TOP-REAL 2 by EUCLID:def 8;
reserve P, R for Subset of TOP-REAL 2;
theorem Th24:
for p st R is being_Region & P = {q: q<>p & q in R & not 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
let p;
assume that
A1: R is being_Region and
A2: P = {q: q<>p & q in R & not ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R};
reconsider RR = R, PP=P as Subset of the TopStruct of TOP-REAL 2;
R is open by A1;
then
A3: RR is open by PRE_TOPC:30;
now
let u;
reconsider p2=u as Point of TOP-REAL 2 by TOPREAL3:8;
assume
A4: u in P;
then
ex q1 st q1 = u & q1<>p & q1 in R & not ex P1 being Subset of TOP-REAL
2 st P1 is_S-P_arc_joining p,q1 & P1 c=R by A2;
then consider r being Real such that
A5: r>0 and
A6: Ball(u,r) c= RR by A3,Lm1,TOPMETR:15;
take r;
thus r>0 by A5;
reconsider r9 = r as Real;
A7: p2 in Ball(u,r9) by A5,TBSP_1:11;
thus Ball(u,r) c= P
proof
assume not thesis;
then consider x being object such that
A8: x in Ball(u,r) and
A9: not x in P;
x in R by A6,A8;
then reconsider q=x as Point of TOP-REAL 2;
now
per cases by A2,A6,A8,A9;
suppose
A10: q=p;
A11: now
assume
A12: q=p2;
ex p3 st p3=p2 & p3<>p & p3 in R & not ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,p3 & P1 c=R by A2,A4;
hence contradiction by A10,A12;
end;
u in Ball(u,r9) by A5,TBSP_1:11;
then
A13: ex P2 being Subset of TOP-REAL 2 st P2 is_S-P_arc_joining q,p2 &
P2 c= Ball(u,r9) by A8,A11,Th10;
not p2 in P
proof
assume p2 in P;
then ex q4 st q4=p2 & q4<>p & q4 in R & not ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q4 & P1 c=R by A2;
hence contradiction by A6,A10,A13,XBOOLE_1:1;
end;
hence contradiction by A4;
end;
suppose
A14: ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p
,q & P1 c=R;
not p2 in P
proof
assume p2 in P;
then ex q4 st q4=p2 & q4<>p & q4 in R & not ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q4 & P1 c=R by A2;
hence contradiction by A6,A7,A8,A14,Th23;
end;
hence contradiction by A4;
end;
end;
hence contradiction;
end;
end;
then PP is open by Lm1,TOPMETR:15;
hence thesis by PRE_TOPC:30;
end;
theorem Th25:
R is being_Region & p in R & P = {q: q=p or ex P1 being Subset
of TOP-REAL 2 st P1 is_S-P_arc_joining p,q & P1 c=R} implies P is open
proof
assume that
A1: R is being_Region and
A2: p in R and
A3: P = {q: q=p or ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R};
reconsider RR = R, PP=P as Subset of the TopStruct of TOP-REAL 2;
R is open by A1;
then
A4: RR is open by PRE_TOPC:30;
now
let u;
reconsider p2=u as Point of TOP-REAL 2 by TOPREAL3:8;
assume u in P;
then consider q1 such that
A5: q1=u and
A6: q1=p or ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining
p,q1 & P1 c=R by A3;
now
per cases by A6;
suppose
q1=p;
hence p2 in R by A2,A5;
end;
suppose
ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p,
q1 & P1 c=R;
then consider P2 being Subset of TOP-REAL 2 such that
A7: P2 is_S-P_arc_joining p,q1 and
A8: P2 c=R;
p2 in P2 by A5,A7,Th3;
hence p2 in R by A8;
end;
end;
then consider r being Real such that
A9: r>0 and
A10: Ball(u,r) c= RR by A4,Lm1,TOPMETR:15;
take r;
thus r>0 by A9;
reconsider r9= r as Real;
A11: p2 in Ball(u,r9) by A9,TBSP_1:11;
thus Ball(u,r) c= P
proof
let x be object;
assume
A12: x in Ball(u,r);
then reconsider q=x as Point of TOP-REAL 2 by A10,TARSKI:def 3;
now
per cases;
suppose
q=p;
hence thesis by A3;
end;
suppose
A13: q<>p;
A14: now
assume q1=p;
then p in Ball(u,r9) by A5,A9,TBSP_1:11;
then consider P2 being Subset of TOP-REAL 2 such that
A15: P2 is_S-P_arc_joining p,q and
A16: P2 c= Ball(u,r9) by A12,A13,Th10;
reconsider P2 as Subset of TOP-REAL 2;
P2 c= R by A10,A16;
hence thesis by A3,A15;
end;
now
assume q1<>p;
then
ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p,q
& P1 c=R by A5,A6,A10,A11,A12,A13,Th23;
hence thesis by A3;
end;
hence thesis by A14;
end;
end;
hence thesis;
end;
end;
then PP is open by Lm1,TOPMETR:15;
hence thesis by PRE_TOPC:30;
end;
theorem Th26:
p in R & P={q: q=p or ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R} implies P c= R
proof
assume that
A1: p in R and
A2: P = {q: q=p or ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R};
let x be object;
assume x in P;
then consider q such that
A3: q=x and
A4: q=p or ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p,q
& P1 c=R by A2;
now
per cases by A4;
suppose
q=p;
hence thesis by A1,A3;
end;
suppose
ex P1 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p,q & P1 c=R;
then consider P1 being Subset of TOP-REAL 2 such that
A5: P1 is_S-P_arc_joining p,q and
A6: P1 c=R;
q in P1 by A5,Th3;
hence thesis by A3,A6;
end;
end;
hence thesis;
end;
theorem Th27:
R is being_Region & p in R & P={q: q=p or ex P1 be Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q & P1 c=R} implies R c= P
proof
assume that
A1: R is being_Region and
A2: p in R and
A3: P = {q: q=p or ex P1 be Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R};
A4: p in P by A3;
set P2 = R \ P;
reconsider P22=P2 as Subset of TOP-REAL 2;
A5: [#]((TOP-REAL 2)|R) = R by PRE_TOPC:def 5;
then reconsider P11 = P, P12 = P22 as Subset of (TOP-REAL 2)|R by A2,A3,Th26,
XBOOLE_1:36;
P \/ (R \ P) = P \/ R by XBOOLE_1:39;
then
A6: [#]((TOP-REAL 2)|R) = P11 \/ P12 by A5,XBOOLE_1:12;
now
let x be object;
A7: now
assume
A8: x in P2;
then reconsider q2=x as Point of TOP-REAL 2;
not x in P by A8,XBOOLE_0:def 5;
then
A9: q2<>p & not ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q2 & P1 c=R by A3;
q2 in R by A8,XBOOLE_0:def 5;
hence
x in {q: q<>p & q in R & not ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c= R} by A9;
end;
now
assume x in {q: q<>p & q in R & not ex P1 being Subset of TOP-REAL 2
st P1 is_S-P_arc_joining p,q & P1 c=R};
then
A10: ex q3 st q3=x & q3<>p & q3 in R & not ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q3 & P1 c=R;
then not ex q st q=x & (q=p or ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R);
then not x in P by A3;
hence x in P2 by A10,XBOOLE_0:def 5;
end;
hence x in P2 iff x in {q: q<>p & q in R & not ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q & P1 c=R} by A7;
end;
then P2={q: q<>p & q in R & not ex P1 being Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q & P1 c=R} by TARSKI:2;
then P22 is open by A1,Th24;
then
A11: P22 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
reconsider R9 = R as non empty Subset of TOP-REAL 2 by A2;
R is connected by A1;
then
A12: (TOP-REAL 2)|R9 is connected by CONNSP_1:def 3;
P is open by A1,A2,A3,Th25;
then
A13: P in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
P11 = P /\ [#]((TOP-REAL 2)|R) by XBOOLE_1:28;
then P11 in the topology of (TOP-REAL 2)|R by A13,PRE_TOPC:def 4;
then
A14: P11 is open by PRE_TOPC:def 2;
P12 = P22 /\ [#]((TOP-REAL 2)|R) by XBOOLE_1:28;
then P12 in the topology of ( TOP-REAL 2)|R by A11,PRE_TOPC:def 4;
then
A15: P12 is open by PRE_TOPC:def 2;
A16: P11 misses P12 by XBOOLE_1:79;
then P11 /\ P12 = {}((TOP-REAL 2)|R);
then P2 = {} by A4,A12,A16,A6,A14,A15,CONNSP_1:11;
hence thesis by XBOOLE_1:37;
end;
theorem
R is being_Region & p in R & P={q: q=p or ex P1 being Subset of
TOP-REAL 2 st P1 is_S-P_arc_joining p,q & P1 c=R} implies R = P
by Th27,Th26;
theorem
R is being_Region & p in R & q in R & p<>q implies ex P st P
is_S-P_arc_joining p,q & P c=R
proof
set RR={q2: q2=p or ex P1 be Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p
,q2 & P1 c=R};
RR c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in RR;
then ex q2 st q2=x & (q2=p or ex P1 be Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q2 & P1 c=R);
hence thesis;
end;
then reconsider RR as Subset of TOP-REAL 2;
assume that
A1: R is being_Region & p in R and
A2: q in R and
A3: p<>q;
R c= RR by A1,Th27;
then q in RR by A2;
then ex q1 st q1=q & (q1=p or ex P1 be Subset of TOP-REAL 2 st P1
is_S-P_arc_joining p,q1 & P1 c=R);
hence thesis by A3;
end;