:: Graph Theoretical Properties of Arcs in the Plane and Fashoda
:: Meet Theorem
:: by Yatsuka Nakamura
::
:: Received August 21, 1998
:: Copyright (c) 1998-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, GRAPH_1, FINSEQ_1, STRUCT_0, TREES_2, SUBSET_1, REAL_1,
GRAPH_4, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0, CARD_1, ZFMISC_1, MCART_1,
ARYTM_1, NAT_1, RELAT_1, TARSKI, PARTFUN1, GLIB_000, FINSET_1, EUCLID,
RLTOPSP1, TOPREAL1, GOBOARD5, PRE_TOPC, SUPINF_2, GOBOARD1, GOBOARD4,
COMPLEX1, METRIC_1, SQUARE_1, RVSUM_1, CARD_3, PCOMPS_1, RCOMP_1,
WEIERSTR, INT_1, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, MEASURE5,
PSCOMP_1, XXREAL_2, JGRAPH_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, FINSET_1, NAT_1, NAT_D, SEQM_3,
GRAPH_1, STRUCT_0, GRAPH_2, GRAPH_4, TOPREAL1, GOBOARD5, PRE_TOPC,
GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, TOPS_2,
METRIC_1, TBSP_1, RCOMP_1, SQUARE_1, PSCOMP_1, RVSUM_1, RLVECT_1,
RLTOPSP1, EUCLID, FUNCT_3;
constructors FUNCT_3, REAL_1, SQUARE_1, NAT_D, RCOMP_1, BINARITH, TOPS_2,
COMPTS_1, TBSP_1, MONOID_0, GOBOARD1, GOBOARD4, GOBOARD5, PSCOMP_1,
GRAPH_2, WEIERSTR, GRAPH_4, XXREAL_2, FUNCSDOM, FINSEQ_6;
registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1,
STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, GRAPH_2, GRAPH_4,
FINSET_1, VALUED_0, FUNCT_2, CARD_1, XXREAL_2, TOPREAL1, RELSET_1,
SQUARE_1, ORDINAL1, FINSEQ_6;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, EUCLID, SQUARE_1, BINOP_1, STRUCT_0, ALGSTR_0, RLTOPSP1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, FUNCT_1, FINSEQ_1, NAT_1, ZFMISC_1, SPPOL_1, FINSEQ_4,
GRAPH_1, FUNCT_3, RELAT_1, GRAPH_4, FINSEQ_3, TOPREAL1, GOBOARD1,
GOBOARD5, GOBOARD4, TOPREAL3, SQUARE_1, EUCLID, JORDAN7, UNIFORM1,
WEIERSTR, JORDAN5A, TOPS_2, PRE_TOPC, TBSP_1, HEINE, COMPTS_1, TOPMETR,
PSCOMP_1, BORSUK_1, ABSVALUE, METRIC_1, RVSUM_1, FUNCT_2, JORDAN6,
XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_0, COMPLEX1, XREAL_1, XXREAL_0,
ORDINAL1, NAT_D, PARTFUN1, XXREAL_1, XXREAL_2, SEQM_3, XREAL_0, VALUED_1,
RLTOPSP1, CARD_1, XTUPLE_0, RLVECT_4, RLVECT_1;
schemes FINSEQ_1;
begin :: GRAPHS BY CARTESIAN PRODUCT
reserve x,y for set;
reserve G for Graph;
reserve vs,vs9 for FinSequence of the carrier of G;
reserve IT for oriented Chain of G;
reserve N for Nat;
reserve n,m,k,i,j for Nat;
reserve r,r1,r2 for Real;
theorem Th1:
for vs st IT is Simple & vs is_oriented_vertex_seq_of IT holds
for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
proof
let vs;
assume that
A1: IT is Simple and
A2: vs is_oriented_vertex_seq_of IT;
A3: len vs = len IT + 1 by A2,GRAPH_4:def 5;
consider vs9 such that
A4: vs9 is_oriented_vertex_seq_of IT and
A5: for n,m being Nat
st 1<=n & n<m & m<=len vs9 & vs9.n=vs9.m holds n=1 & m=len vs9
by A1,GRAPH_4:def 7;
A6: for n,m being Nat
st 1<=n & n<m & m<=len vs9 & vs9.n=vs9.m holds n=1 & m=len vs9
by A5;
per cases;
suppose
IT<> {};
then vs=vs9 by A2,A4,GRAPH_4:10;
hence thesis by A6;
end;
suppose
IT= {};
then len IT=0;
hence thesis by A3,XXREAL_0:2;
end;
end;
definition
let X be set;
func PGraph(X) -> MultiGraphStruct equals
MultiGraphStruct(#X,[:X,X:],pr1(X,
X),pr2(X,X)#);
coherence;
end;
theorem
for X being set holds the carrier of PGraph(X)=X;
definition
let f be FinSequence;
func PairF(f) -> FinSequence means
:Def2:
len it=len f-'1 & for i being Nat st 1<=i & i<len f holds it.i=[f.i,f.(i+1)];
existence
proof
deffunc F(Nat)=[f.$1,f.($1+1)];
ex p being FinSequence st len p = len f-'1 & for k being Nat st k in
dom p holds p.k=F(k) from FINSEQ_1:sch 2;
then consider p being FinSequence such that
A1: len p = len f-'1 and
A2: for k being Nat st k in dom p holds p.k=[f.k,f.(k+1)];
for i being Nat st 1<=i & i<len f holds p.i=[f.i,f.(i+1)]
proof
let i be Nat;
assume that
A3: 1<=i and
A4: i<len f;
i+1<=len f by A4,NAT_1:13;
then
A5: i+1-1<=len f-1 by XREAL_1:9;
len f-1=len f-'1 by A3,A4,XREAL_1:233,XXREAL_0:2;
then i in dom p by A1,A3,A5,FINSEQ_3:25;
hence thesis by A2;
end;
hence thesis by A1;
end;
uniqueness
proof
let g1,g2 be FinSequence;
assume that
A6: len g1=len f-'1 and
A7: for i being Nat st 1<=i & i<len f holds g1.i=[f.i,f.(i +1 )] and
A8: len g2=len f-'1 and
A9: for i being Nat st 1<=i & i<len f holds g2.i=[f.i,f.(i +1 )];
per cases;
suppose
A10: len f>=1;
for j being Nat st 1<=j & j<=len g1 holds g1.j=g2.j
proof
let j be Nat;
assume that
A11: 1<=j and
A12: j<=len g1;
len f<len f+1 by NAT_1:13;
then len f-1<len f by XREAL_1:19;
then len g1<len f by A6,A10,XREAL_1:233;
then
A13: j in NAT & j<len f by A12,ORDINAL1:def 12,XXREAL_0:2;
then g1.j=[f.j,f.(j+1)] by A7,A11;
hence thesis by A9,A11,A13;
end;
hence thesis by A6,A8,FINSEQ_1:14;
end;
suppose
len f<1;
then len f+1<=1 by NAT_1:13;
then len f+1-1<=1-1 by XREAL_1:9;
then
A14: len f=0;
0 qua Nat-1<0;
then g1= {} by A6,A14,XREAL_0:def 2;
hence thesis by A6,A8;
end;
end;
end;
reserve X for non empty set;
registration
let X be non empty set;
cluster PGraph(X) -> non empty;
coherence;
end;
theorem
for f being FinSequence of X holds f is FinSequence of the carrier of
PGraph(X);
theorem Th4:
for f being FinSequence of X holds PairF(f) is FinSequence of the
carrier' of PGraph(X)
proof
let f be FinSequence of X;
rng PairF(f) c= [:X,X:]
proof
let y be object;
A1: len f-'1<len f-'1+1 by NAT_1:13;
assume y in rng PairF(f);
then consider x being object such that
A2: x in dom PairF(f) and
A3: y=(PairF(f)).x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A2;
A4: x in Seg len PairF(f) by A2,FINSEQ_1:def 3;
then
A5: 1<=n by FINSEQ_1:1;
A6: len PairF(f)=len f-'1 by Def2;
A7: n<=len PairF(f) by A4,FINSEQ_1:1;
then 1<=len f-'1 by A5,A6,XXREAL_0:2;
then len f-'1=len f-1 by NAT_D:39;
then
A8: n<len f by A7,A6,A1,XXREAL_0:2;
then
A9: n+1<=len f by NAT_1:13;
1<n+1 by A5,NAT_1:13;
then n+1 in dom f by A9,FINSEQ_3:25;
then
A10: f.(n+1) in rng f by FUNCT_1:def 3;
n in dom f by A5,A8,FINSEQ_3:25;
then
A11: f.n in rng f by FUNCT_1:def 3;
(PairF(f)).n =[f.n,f.(n+1)] by A5,A8,Def2;
hence thesis by A3,A11,A10,ZFMISC_1:def 2;
end;
hence thesis by FINSEQ_1:def 4;
end;
definition
let X be non empty set,f be FinSequence of X;
redefine func PairF(f) -> FinSequence of the carrier' of PGraph(X); :: redefines PairF (JGRAPH_1, definition)
coherence by Th4;
end;
theorem Th5:
for n being Nat,f being FinSequence of X st 1 <= n & n
<= len PairF(f) holds (PairF(f)).n in the carrier' of PGraph(X)
proof
let n be Nat,f be FinSequence of X;
assume that
A1: 1 <= n and
A2: n <= len PairF(f);
A3: len f-'1<len f-'1+1 by NAT_1:13;
A4: len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A1,A2,XXREAL_0:2;
then len f-'1=len f-1 by NAT_D:39;
then
A5: n<len f by A2,A4,A3,XXREAL_0:2;
then
A6: n+1<=len f by NAT_1:13;
1<n+1 by A1,NAT_1:13;
then n+1 in dom f by A6,FINSEQ_3:25;
then
A7: f.(n+1) in rng f by FUNCT_1:def 3;
n in dom f by A1,A5,FINSEQ_3:25;
then
A8: f.n in rng f by FUNCT_1:def 3;
(PairF(f)).n =[f.n,f.(n+1)] by A1,A5,Def2;
hence thesis by A8,A7,ZFMISC_1:def 2;
end;
theorem Th6:
for f being FinSequence of X holds PairF(f) is oriented Chain of PGraph(X)
proof
let f be FinSequence of X;
A1: now
per cases;
case
len f>=1;
then len f-1+1=len f-'1+1 by XREAL_1:233;
then
A2: len f = len PairF(f) + 1 by Def2;
A3: for n being Nat
st 1 <= n & n <= len f holds f.n in the carrier of PGraph(X)
proof
let n be Nat;
assume 1 <= n & n <= len f;
then n in dom f by FINSEQ_3:25;
then f.n in rng f by FUNCT_1:def 3;
hence thesis;
end;
A4: for n being Nat
st 1 <= n & n <= len PairF(f) ex x9, y9 being Element
of PGraph(X) st x9 = f.n & y9 = f.(n+1) & (PairF(f)).n joins x9, y9
proof
A5: len f-'1<len f-'1+1 by NAT_1:13;
let n be Nat;
assume that
A6: 1 <= n and
A7: n <= len PairF(f);
A8: 1<n+1 by A6,NAT_1:13;
A9: len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A6,A7,XXREAL_0:2;
then len f-'1=len f-1 by NAT_D:39;
then
A10: n<len f by A7,A9,A5,XXREAL_0:2;
then n+1<=len f by NAT_1:13;
then n+1 in dom f by A8,FINSEQ_3:25;
then
A11: f.(n+1) in rng f by FUNCT_1:def 3;
n in dom f by A6,A10,FINSEQ_3:25;
then
A12: f.n in rng f by FUNCT_1:def 3;
then reconsider
a=f.n,b=f.(n+1) as Element of PGraph(X ) by A11;
(pr2(X,X)).(f.n,f.(n+1))=f.(n+1) by A12,A11,FUNCT_3:def 5;
then
A13: (the Target of PGraph(X)).((PairF(f)).n) = b by A6,A10,Def2;
(pr1(X,X)).(f.n,f.(n+1))=f.n by A12,A11,FUNCT_3:def 4;
then (the Source of PGraph(X)).((PairF(f)).n) = a by A6,A10,Def2;
then (PairF(f)).n joins a, b by A13,GRAPH_1:def 12;
hence thesis;
end;
for n being Nat
st 1 <= n & n <= len PairF(f) holds (PairF(f)).n in the
carrier' of PGraph(X) by Th5;
hence PairF(f) is Chain of PGraph(X) by A2,A3,A4,GRAPH_1:def 14;
end;
case
len f<1;
then len f+1<=1 by NAT_1:13;
then len f+1-1<=1-1 by XREAL_1:9;
then
A14: len f=0;
0 qua Nat-1<0;
then len f-'1=0 by A14,XREAL_0:def 2;
then len PairF(f)=0 by Def2;
then PairF(f)= {};
hence thesis by GRAPH_1:14;
end;
end;
for n being Nat
st 1 <= n & n < len PairF(f) holds (the Source of PGraph(X)).((
PairF(f)).(n+1)) = (the Target of PGraph(X)).((PairF(f)).n)
proof
A15: len f-'1<len f-'1+1 by NAT_1:13;
let n be Nat;
assume that
A16: 1 <= n and
A17: n < len PairF(f);
A18: len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A16,A17,XXREAL_0:2;
then
A19: len f-'1=len f-1 by NAT_D:39;
then
A20: n<len f by A17,A18,A15,XXREAL_0:2;
then n in dom f by A16,FINSEQ_3:25;
then
A21: f.n in rng f by FUNCT_1:def 3;
n+1<=len PairF(f) by A17,NAT_1:13;
then
A22: n+1<len f by A18,A19,A15,XXREAL_0:2;
then
A23: n+1+1<=len f by NAT_1:13;
A24: 1<n+1 by A16,NAT_1:13;
then 1<n+1+1 by NAT_1:13;
then n+1+1 in dom f by A23,FINSEQ_3:25;
then
A25: f.(n+1+1) in rng f by FUNCT_1:def 3;
n+1<=len f by A20,NAT_1:13;
then n+1 in dom f by A24,FINSEQ_3:25;
then
A26: f.(n+1) in rng f by FUNCT_1:def 3;
then reconsider
b=f.(n+1) as Element of PGraph(X);
(pr2(X,X)).(f.n,f.(n+1))=f.(n+1) by A21,A26,FUNCT_3:def 5;
then
A27: (the Target of PGraph(X)).((PairF(f)).n) = b by A16,A20,Def2;
n+1 in dom f by A22,A24,FINSEQ_3:25;
then f.(n+1) in rng f by FUNCT_1:def 3;
then (pr1(X,X)).(f.(n+1),f.((n+1)+1))=f.(n+1) by A25,FUNCT_3:def 4;
hence thesis by A22,A24,A27,Def2;
end;
hence thesis by A1,GRAPH_1:def 15;
end;
definition
let X be non empty set,f be FinSequence of X;
redefine func PairF(f) -> oriented Chain of PGraph(X); :: redefines PairF (JGRAPH_1, definition)
coherence by Th6;
end;
theorem Th7:
for f being FinSequence of X, f1 being FinSequence of the
carrier of PGraph(X) st len f>=1 & f=f1 holds f1 is_oriented_vertex_seq_of
PairF(f)
proof
let f be FinSequence of X, f1 be FinSequence of the carrier of PGraph(X);
assume that
A1: len f>=1 and
A2: f=f1;
A3: for n st 1<=n & n<=len PairF(f) holds ((PairF(f)).n) orientedly_joins f1
/.n, f1/.(n+1)
proof
A4: len f-'1<len f-'1+1 by NAT_1:13;
let n;
assume that
A5: 1<=n and
A6: n<=len PairF(f);
A7: 1<n+1 by A5,NAT_1:13;
A8: len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A5,A6,XXREAL_0:2;
then len f-'1=len f-1 by NAT_D:39;
then
A9: n<len f by A6,A8,A4,XXREAL_0:2;
then n+1<=len f by NAT_1:13;
then
A10: n+1 in dom f by A7,FINSEQ_3:25;
then
A11: f.(n+1) in rng f by FUNCT_1:def 3;
A12: n in dom f by A5,A9,FINSEQ_3:25;
then
A13: f.n in rng f by FUNCT_1:def 3;
then
A14: (pr1(X,X)).(f.n,f.(n+1))=f.n by A11,FUNCT_3:def 4;
A15: (pr2(X,X)).(f.n,f.(n+1))=f.(n+1) by A13,A11,FUNCT_3:def 5;
f1/.(n+1)=f1.(n+1) by A2,A10,PARTFUN1:def 6;
then
A16: (the Target of PGraph(X)).((PairF(f)).n) = f1/.(n+1) by A2,A5,A9,A15,Def2;
f1/.n=f1.n by A2,A12,PARTFUN1:def 6;
then (the Source of PGraph(X)).((PairF(f)).n) = f1/.n by A2,A5,A9,A14,Def2;
hence thesis by A16,GRAPH_4:def 1;
end;
A17:for n being Nat
st 1<=n & n<=len PairF(f) holds ((PairF(f)).n) orientedly_joins f1
/.n, f1/.(n+1) by A3;
len f-'1=len f-1 by A1,XREAL_1:233;
then len f-1+1=len PairF(f)+1 by Def2;
hence thesis by A2,A17,GRAPH_4:def 5;
end;
begin :: SHORTCUTS OF FINITE SEQUENCES IN PLANE
definition
let X be non empty set,f,g be FinSequence of X;
pred g is_Shortcut_of f means
f.1=g.1 & f.len f=g.len g & ex fc being
Subset of PairF(f),fvs being Subset of f, sc being oriented simple Chain of
PGraph(X), g1 being FinSequence of the carrier of PGraph(X) st Seq fc = sc &
Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc;
end;
theorem Th8:
for f,g being FinSequence of X st g is_Shortcut_of f holds 1<=
len g & len g <= len f
proof
let f,g be FinSequence of X;
reconsider df=dom f as finite set;
A1: card df=card (Seg len f) by FINSEQ_1:def 3
.=len f by FINSEQ_1:57;
assume g is_Shortcut_of f;
then consider fc being Subset of PairF(f),fvs being Subset of f, sc being
oriented simple Chain of PGraph(X), g1 being FinSequence of the carrier of
PGraph(X) such that
Seq fc = sc and
A2: Seq fvs = g and
A3: g1=g and
A4: g1 is_oriented_vertex_seq_of sc;
A5: len g1 = len sc + 1 by A4,GRAPH_4:def 5;
reconsider dfvs=dom fvs as finite set;
A6: rng Sgm(dom fvs) c= dom fvs by FINSEQ_1:50;
A7: dom fvs c= dom f by RELAT_1:11;
g=fvs*Sgm(dom fvs) by A2,FINSEQ_1:def 15;
then dom g=dom (Sgm(dom fvs)) by A6,RELAT_1:27;
then len g=len Sgm(dom fvs) by FINSEQ_3:29
.=card dfvs by FINSEQ_3:39;
hence thesis by A3,A5,A7,A1,NAT_1:12,43;
end;
theorem Th9:
for f being FinSequence of X st len f>=1 holds ex g being
FinSequence of X st g is_Shortcut_of f
proof
let f be FinSequence of X;
reconsider f1=f as FinSequence of the carrier of PGraph(X);
assume len f>=1;
then consider fc being Subset of PairF(f), fvs being Subset of f1, sc being
oriented simple Chain of PGraph(X), vs1 being FinSequence of the carrier of
PGraph(X) such that
A1: Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & f1.
1 = vs1.1 & f1.len f1 = vs1.len vs1 by Th7,GRAPH_4:21;
reconsider g1=vs1 as FinSequence of X;
g1 is_Shortcut_of f by A1;
hence thesis;
end;
theorem Th10:
for f,g being FinSequence of X holds
g is_Shortcut_of f implies rng PairF(g) c= rng PairF(f)
proof
let f,g be FinSequence of X;
A1: len PairF(g)=len g-'1 by Def2;
len g<len g+1 by NAT_1:13;
then
A2: len g-1<len g by XREAL_1:19;
assume g is_Shortcut_of f;
then consider fc being Subset of PairF(f), fvs being Subset of f, sc being
oriented simple Chain of PGraph(X), g1 being FinSequence of the carrier of
PGraph(X) such that
A3: Seq fc = sc and
Seq fvs = g and
A4: g1=g and
A5: g1 is_oriented_vertex_seq_of sc;
A6: rng Sgm(dom fc) = dom fc by FINSEQ_1:50;
fc* Sgm(dom fc)=sc by A3,FINSEQ_1:def 15;
then rng fc = rng sc by A6,RELAT_1:28;
then
A7: rng sc c= rng PairF(f) by RELAT_1:11;
len f<len f+1 by NAT_1:13;
then
A8: len f-1<len f by XREAL_1:19;
let y be object;
assume y in rng PairF(g);
then consider x being object such that
A9: x in dom PairF(g) and
A10: y=(PairF(g)).x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A9;
A11: x in Seg len PairF(g) by A9,FINSEQ_1:def 3;
then
A12: 1<=n by FINSEQ_1:1;
then
A13: 1<=n+1 by NAT_1:13;
A14: n<=len PairF(g) by A11,FINSEQ_1:1;
then 1<=len PairF(g) by A12,XXREAL_0:2;
then len g-'1=len g-1 by A1,NAT_D:39;
then
A15: n<len g by A14,A1,A2,XXREAL_0:2;
then n+1<=len g by NAT_1:13;
then n+1<=len sc+1 by A4,A5,GRAPH_4:def 5;
then
A16: n<=len sc by XREAL_1:6;
then
A17: (sc.n) orientedly_joins g1/.n, g1/.(n+1) by A5,A12,GRAPH_4:def 5;
n in dom sc by A12,A16,FINSEQ_3:25;
then sc.n in rng sc by FUNCT_1:def 3;
then consider z being object such that
A18: z in dom PairF(f) and
A19: (PairF(f)).z=sc.n by A7,FUNCT_1:def 3;
reconsider m=z as Element of NAT by A18;
A20: z in Seg len PairF(f) by A18,FINSEQ_1:def 3;
then
A21: 1<=m by FINSEQ_1:1;
m<=len PairF(f) by A20,FINSEQ_1:1;
then
A22: m<=len f -'1 by Def2;
then 1<=len f-'1 by A21,XXREAL_0:2;
then len f-'1=len f-1 by NAT_D:39;
then
A23: m<len f by A22,A8,XXREAL_0:2;
then
A24: m+1<=len f by NAT_1:13;
A25: 1<=m by A20,FINSEQ_1:1;
then
A26: [f.m,f.(m+1)]=sc.n by A19,A23,Def2;
1<m+1 by A21,NAT_1:13;
then m+1 in dom f by A24,FINSEQ_3:25;
then
A27: f.(m+1) in rng f by FUNCT_1:def 3;
m in dom f by A25,A23,FINSEQ_3:25;
then
A28: f.m in rng f by FUNCT_1:def 3;
then (the Source of PGraph(X)).(f.m,f.(m+1))= f.m by A27,FUNCT_3:def 4;
then g1/.n=f.m by A17,A26,GRAPH_4:def 1;
then
A29: g.n=f.m by A4,A12,A15,FINSEQ_4:15;
A30: (PairF(g)).x=[g.n,g.(n+1)] by A12,A15,Def2;
(the Target of PGraph(X)).(f.m,f.(m+1))= f.(m+1) by A28,A27,FUNCT_3:def 5;
then
A31: g1/.(n+1)=f.(m+1) by A17,A26,GRAPH_4:def 1;
n+1<=len g1 by A4,A15,NAT_1:13;
then g.(n+1)=f.(m+1) by A4,A31,A13,FINSEQ_4:15;
hence thesis by A10,A30,A18,A19,A26,A29,FUNCT_1:def 3;
end;
theorem Th11:
for f,g being FinSequence of X st f.1<>f.len f & g
is_Shortcut_of f holds g is one-to-one
proof
let f,g be FinSequence of X;
assume that
A1: f.1<>f.len f and
A2: g is_Shortcut_of f;
A3: f.1=g.1 & f.len f=g.len g by A2;
consider fc being Subset of PairF(f), fvs being Subset of f, sc being
oriented simple Chain of PGraph(X), g1 being FinSequence of the carrier of
PGraph(X) such that
Seq fc = sc and
Seq fvs = g and
A4: g1=g and
A5: g1 is_oriented_vertex_seq_of sc by A2;
sc is Simple by GRAPH_4:18;
then consider vs being FinSequence of the carrier of PGraph(X) such that
A6: vs is_oriented_vertex_seq_of sc and
A7: for n,m being Nat st 1<=n & n<m & m<=len vs & vs.n=vs.m
holds n=1 & m=len vs by GRAPH_4:def 7;
A8: len g1 = len sc + 1 by A5,GRAPH_4:def 5;
then 1<=len g1 by NAT_1:11;
then 1<len g1 by A1,A3,A4,XXREAL_0:1;
then sc<> {} by A8;
then
A9: g1=vs by A5,A6,GRAPH_4:10;
let x,y be object;
assume that
A10: x in dom g and
A11: y in dom g and
A12: g.x=g.y;
assume
A13: x<>y;
reconsider i1=x as Element of NAT by A10;
A14: x in Seg len g by A10,FINSEQ_1:def 3;
then
A15: 1<=i1 by FINSEQ_1:1;
A16: i1<=len g by A14,FINSEQ_1:1;
reconsider i2=y as Element of NAT by A11;
A17: y in Seg len g by A11,FINSEQ_1:def 3;
then
A18: 1<=i2 by FINSEQ_1:1;
A19: i2<=len g by A17,FINSEQ_1:1;
per cases;
suppose
i1<=i2;
then
A20: i1<i2 by A13,XXREAL_0:1;
then i1=1 by A4,A7,A9,A12,A15,A19;
hence contradiction by A1,A3,A4,A7,A9,A12,A19,A20;
end;
suppose
A21: i1>i2;
then i2=1 by A4,A7,A9,A12,A16,A18;
hence contradiction by A1,A3,A4,A7,A9,A12,A16,A21;
end;
end;
definition
let n;
let IT be FinSequence of TOP-REAL n;
attr IT is nodic means
for i,j st LSeg(IT,i) meets LSeg(IT,j) holds
LSeg(IT,i) /\ LSeg(IT,j)={IT.i} &(IT.i=IT.j or IT.i=IT.(j+1)) or LSeg(IT,i) /\
LSeg(IT,j)={IT.(i+1)} &(IT.(i+1)=IT.j or IT.(i+1)=IT.(j+1)) or LSeg(IT,i)=LSeg(
IT,j);
end;
theorem
for f being FinSequence of TOP-REAL 2 st f is s.n.c. holds f is s.c.c.
proof
let f be FinSequence of TOP-REAL 2;
assume f is s.n.c.;
then
for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f) holds LSeg(f,i)
misses LSeg(f,j) by TOPREAL1:def 7;
hence thesis by GOBOARD5:def 4;
end;
theorem Th13:
for f being FinSequence of TOP-REAL 2 st f is s.c.c. & LSeg(f,1)
misses LSeg(f,len f -'1) holds f is s.n.c.
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is s.c.c. and
A2: LSeg(f,1) misses LSeg(f,len f -'1);
for i,j be Nat st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
proof
let i,j be Nat;
assume
A3: i+1 < j;
per cases;
suppose
len f<>0;
then
A4: len f>=0 qua Nat+1 by NAT_1:13;
now
per cases;
case
A5: 1<=i & j+1<=len f;
then
A6: j<len f by NAT_1:13;
now
per cases;
case
A7: i=1 & j+1=len f;
then j=len f-1;
then LSeg(f,i) misses LSeg(f,j) by A2,A4,A7,XREAL_1:233;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
case
not(i=1 & j+1=len f);
then i>1 or j+1<len f by A5,XXREAL_0:1;
then LSeg(f,i) misses LSeg(f,j) by A1,A3,A6,GOBOARD5:def 4;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
case
A8: not (1<=i & j+1<=len f);
now
per cases by A8;
case
1>i;
then LSeg(f,i)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
case
j+1>len f;
then LSeg(f,j)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
hence thesis;
end;
suppose
A9: len f=0;
now
per cases;
case
i>=1;
i+1>len f by A9;
then LSeg(f,i)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
case
i<1;
then LSeg(f,i)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
hence thesis;
end;
end;
hence thesis by TOPREAL1:def 7;
end;
theorem Th14:
for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f)
is Simple holds f is s.c.c.
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is nodic and
A2: PairF(f) is Simple;
reconsider f1=f as FinSequence of the carrier of PGraph(the carrier of
TOP-REAL 2);
per cases;
suppose
len f>=1;
then
A3: f1 is_oriented_vertex_seq_of PairF(f) by Th7;
for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f) holds LSeg(f,i
) misses LSeg(f,j)
proof
let i,j;
assume that
A4: i+1 < j and
A5: i > 1 & j < len f or j+1 < len f;
per cases;
suppose
A6: i>=1;
A7: i<j by A4,NAT_1:13;
then
A8: 1<=j by A6,XXREAL_0:2;
then
A9: 1<j+1 by NAT_1:13;
A10: i+1<j+1 by A4,NAT_1:13;
A11: 1<i+1 by A6,NAT_1:13;
A12: j<len f by A5,NAT_1:13;
then
A13: i+1<len f by A4,XXREAL_0:2;
A14: j+1<=len f by A5,NAT_1:13;
A15: i<j+1 by A7,NAT_1:13;
then
A16: i<len f by A14,XXREAL_0:2;
now
assume
A17: LSeg(f,i) meets LSeg(f,j);
now
per cases by A1,A17;
case
A18: LSeg(f,i) /\ LSeg(f,j)={f.i} &(f.i=f.j or f.i=f.(j+1))&
LSeg(f,i)<>LSeg(f,j);
now
per cases by A18;
case
f.i=f.j;
hence contradiction by A2,A3,A6,A7,A12,Th1;
end;
case
f.i=f.(j+1);
hence contradiction by A2,A3,A5,A6,A15,A14,Th1;
end;
end;
hence contradiction;
end;
case
A19: LSeg(f,i) /\ LSeg(f,j)={f.(i+1)} &(f.(i+1)=f.j or f.(i+
1)=f.(j+1))&LSeg(f,i)<>LSeg(f,j);
now
per cases by A19;
case
f.(i+1)=f.j;
hence contradiction by A2,A3,A4,A12,A11,Th1;
end;
case
f.(i+1)=f.(j+1);
hence contradiction by A2,A3,A10,A14,A11,Th1;
end;
end;
hence contradiction;
end;
case
LSeg(f,i)=LSeg(f,j);
then LSeg(f/.i,f/.(i+1))=LSeg(f,j) by A6,A13,TOPREAL1:def 3;
then
A20: LSeg(f/.i,f/.(i+1))=LSeg(f/.j,f/.(j+1)) by A8,A14,TOPREAL1:def 3;
A21: f/.j=f.j & f/.(j+1)=f.(j+1) by A8,A12,A14,A9,FINSEQ_4:15;
A22: f/.i=f.i & f/.(i+1)=f.(i+1) by A6,A13,A16,A11,FINSEQ_4:15;
now
per cases by A20,A22,A21,SPPOL_1:8;
case
f.i=f.j & f.(i+1)=f.(j+1);
hence contradiction by A2,A3,A10,A14,A11,Th1;
end;
case
f.i=f.(j+1) & f.(i+1)=f.j;
hence contradiction by A2,A3,A4,A12,A11,Th1;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence thesis;
end;
suppose
i<1;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis by GOBOARD5:def 4;
end;
suppose
A23: len f<1;
for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f) holds LSeg(f,
i) misses LSeg(f,j)
proof
let i,j;
assume that
i+1 < j and
i > 1 & j < len f or j+1 < len f;
per cases;
suppose
i>=1;
then i>len f by A23,XXREAL_0:2;
then i+1>len f by NAT_1:13;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
suppose
i<1;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis by GOBOARD5:def 4;
end;
end;
theorem Th15:
for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f)
is Simple & f.1<>f.len f holds f is s.n.c.
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is nodic and
A2: PairF(f) is Simple and
A3: f.1<>f.len f;
reconsider f1=f as FinSequence of the carrier of PGraph(the carrier of
TOP-REAL 2);
A4: len f-'1<=len f by NAT_D:44;
per cases;
suppose
A5: len f-'1>2;
then
A6: len f-'1>1 by XXREAL_0:2;
then
A7: 1<len f by NAT_D:44;
len f>=1 by A6,NAT_D:44;
then
A8: f1 is_oriented_vertex_seq_of PairF(f) by Th7;
A9: 1+1<len f by A5,NAT_D:44;
A10: len f-'1=len f-1 by A6,NAT_D:39;
then
A11: (len f-'1)+1=len f;
now
assume
A12: LSeg(f,1) meets LSeg(f,len f-'1);
now
per cases by A1,A12;
case
LSeg(f,1) /\ LSeg(f,(len f-'1))={f.1} &(f.1=f.(len f-'1) or
f.1=f.((len f-'1)+1));
hence contradiction by A2,A3,A4,A6,A8,A10,Th1;
end;
case
A13: LSeg(f,1) /\ LSeg(f,(len f-'1))={f.(1+1)} &(f.(1+1)=f.(len
f-'1) or f.(1+1)=f.((len f-'1)+1));
now
per cases by A13;
case
f.(1+1)=f.(len f-'1);
hence contradiction by A2,A4,A5,A8,Th1;
end;
case
f.(1+1)=f.((len f-'1)+1);
hence contradiction by A2,A8,A9,A10,Th1;
end;
end;
hence contradiction;
end;
case
LSeg(f,1)=LSeg(f,(len f-'1));
then LSeg(f/.1,f/.(1+1))=LSeg(f,(len f-'1)) by A9,TOPREAL1:def 3;
then
A14: LSeg(f/.1,f/.(1+1))=LSeg(f/.(len f-'1),f/.((len f-'1)+ 1)) by A6,A10,
TOPREAL1:def 3;
A15: 1+1<(len f-'1)+1 by A6,XREAL_1:6;
(len f-'1)<len f by A11,NAT_1:13;
then
A16: f/.(len f-'1)=f.(len f-'1) by A6,FINSEQ_4:15;
1<len f by A6,NAT_D:44;
then
A17: f/.1=f.1 by FINSEQ_4:15;
A18: f/.(1+1)=f.(1+1) & f/.((len f-'1)+1)=f.((len f-'1)+1) by A7,A9,A10,
FINSEQ_4:15;
now
per cases by A14,A17,A16,A18,SPPOL_1:8;
case
f.1=f.(len f-'1) & f.(1+1)=f.((len f-'1)+1);
hence contradiction by A2,A8,A10,A15,Th1;
end;
case
f.1=f.((len f-'1)+1) & f.(1+1)=f.(len f-'1);
hence contradiction by A3,A10;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence thesis by A1,A2,Th13,Th14;
end;
suppose
A19: len f-'1<=2;
for i,j be Nat st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
proof
let i,j be Nat;
assume
A20: i+1 < j;
per cases;
suppose
A21: 1<=i & j+1<=len f;
then 1<i+1 by NAT_1:13;
then 1+1<i+1+1 by XREAL_1:8;
then
A22: 1+1+1<=i+1+1 by NAT_1:13;
i+1+1<j+1 by A20,XREAL_1:6;
then i+1+1<len f by A21,XXREAL_0:2;
then 1+1+1<len f by A22,XXREAL_0:2;
then
A23: 1+1+1-1<len f-1 by XREAL_1:9;
then 1<len f-1 by XXREAL_0:2;
hence thesis by A19,A23,NAT_D:39;
end;
suppose
A24: 1>i or j+1>len f;
now
per cases by A24;
case
1>i;
then LSeg(f,i)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
case
j+1>len f;
then LSeg(f,j)={} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
hence thesis;
end;
end;
hence thesis by TOPREAL1:def 7;
end;
end;
theorem Th16:
for p1,p2,p3 being Point of TOP-REAL n st (ex x being set st x<>
p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3)) holds p1 in LSeg(p2,p3) or p3 in LSeg(p1,
p2)
proof
let p1,p2,p3 be Point of TOP-REAL n;
given x being set such that
A1: x<>p2 and
A2: x in LSeg(p1,p2)/\ LSeg(p2,p3);
reconsider p=x as Point of TOP-REAL n by A2;
A3: p in { (1-r1)*p1 + r1*p2 : 0 <= r1 & r1 <= 1 } by A2,XBOOLE_0:def 4;
A4: p in { (1-r2)*p2 + r2*p3 : 0 <= r2 & r2 <= 1 } by A2,XBOOLE_0:def 4;
consider r1 such that
A5: p=(1-r1)*p1 + r1*p2 and
0 <= r1 and
A6: r1 <= 1 by A3;
consider r2 such that
A7: p=(1-r2)*p2 + r2*p3 and
A8: 0 <= r2 and
r2 <= 1 by A4;
per cases;
suppose
A9: r1>=1-r2;
now
per cases;
case
A10: r2<>0;
r2*p3=(1-r1)*p1 + r1*p2-(1-r2)*p2 by A5,A7,RLVECT_4:1;
then r2*p3=(1-r1)*p1 + (r1*p2-(1-r2)*p2) by RLVECT_1:def 3;
then r2"*(r2*p3)=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by RLVECT_1:35;
then (r2"*r2)*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by RLVECT_1:def 7;
then 1*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by A10,XCMPLX_0:def 7;
then
A11: p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by RLVECT_1:def 8
.=r2"*((1-r1)*p1) +r2"*((r1-(1-r2))*p2) by RLVECT_1:def 5
.=(r2"*(1-r1))*p1 +r2"*((r1-(1-r2))*p2) by RLVECT_1:def 7
.=(r2"*(1-r1))*p1 +(r2"*(r1-(1-r2)))*p2 by RLVECT_1:def 7;
r1<=1+(0 qua Nat) by A6;
then r1-1<=0 by XREAL_1:20;
then r1-1+r2<=0 qua Nat+r2 by XREAL_1:6;
then
A12: r2"*(r1-(1-r2))<=r2"*r2 by A8,XREAL_1:64;
r2"*(1-r1) +r2"*(r1-(1-r2))=r2"*(1-1+r2) .=1 by A10,XCMPLX_0:def 7;
then
A13: r2"*(1-r1)=1-r2"*(r1-(1-r2));
(r1-(1-r2))>=0 by A9,XREAL_1:48;
hence thesis by A8,A11,A13,A12;
end;
case
r2=0;
then p=1*p2+0.TOP-REAL n by A7,RLVECT_1:10;
then p=p2+0.TOP-REAL n by RLVECT_1:def 8;
hence thesis by A1,RLVECT_1:4;
end;
end;
hence thesis;
end;
suppose
A14: r1<1-r2;
set s2=1-r1;
set s1=1-r2;
1-s2+s2<=1+s2 by A6,XREAL_1:6;
then
A15: 1-1<=s2 by XREAL_1:20;
A16: 0 qua Nat+s1<=1-s1+s1 by A8,XREAL_1:6;
now
per cases;
case
A17: s2<>0;
s2*p1=(1-s1)*p3 + s1*p2-(1-s2)*p2 by A5,A7,RLVECT_4:1
.=(1-s1)*p3 + (s1*p2-(1-s2)*p2) by RLVECT_1:def 3
.=(1-s1)*p3 + (s1-(1-s2))*p2 by RLVECT_1:35;
then (s2"*s2)*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by RLVECT_1:def 7;
then 1*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by A17,XCMPLX_0:def 7;
then p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by RLVECT_1:def 8
.=s2"*((1-s1)*p3) +s2"*((s1-(1-s2))*p2) by RLVECT_1:def 5
.=(s2"*(1-s1))*p3 +s2"*((s1-(1-s2))*p2) by RLVECT_1:def 7;
then
A18: p1=(s2"*(1-s1))*p3 +(s2"*(s1-(1-s2)))*p2 by RLVECT_1:def 7;
s1<=1+(0 qua Nat) by A16;
then s1-1<=0 by XREAL_1:20;
then s1-1+s2<=0 qua Nat+s2 by XREAL_1:6;
then
A19: s2"*(s1-(1-s2))<=s2"*s2 by A15,XREAL_1:64;
s2"*(1-s1) +s2"*(s1-(1-s2))=s2"*(1-1+s2) .=1 by A17,XCMPLX_0:def 7;
then
A20: s2"*(1-s1)=1-s2"*(s1-(1-s2));
(s1-(1-s2))>=0 by A14,XREAL_1:48;
then p1 in {(1-r)*p3+r*p2:0<=r & r<=1} by A15,A18,A20,A19;
hence thesis by RLTOPSP1:def 2;
end;
case
s2=0;
then p=1*p2+0.TOP-REAL n by A5,RLVECT_1:10;
then p=p2+0.TOP-REAL n by RLVECT_1:def 8;
hence thesis by A1,RLVECT_1:4;
end;
end;
hence thesis;
end;
end;
theorem Th17:
for f being FinSequence of TOP-REAL 2 st f is s.n.c. & LSeg(f,1)
/\ LSeg(f,1+1) c= {f/.(1+1)} & LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len
f-'1)} holds f is unfolded
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is s.n.c. and
A2: LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} and
A3: LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)};
for i be Nat st 1 <= i & i + 2 <= len f holds LSeg(f,i) /\ LSeg(f,i+1) =
{f/.(i+1)}
proof
let i be Nat;
assume that
A4: 1 <= i and
A5: i + 2 <= len f;
A6: 1<i+1 by A4,NAT_1:13;
then
A7: LSeg(f,i+1)=LSeg(f/.(i+1),f/.(i+1+1)) by A5,TOPREAL1:def 3;
A8: 1<i+1+1 by A6,NAT_1:13;
i+1+1=i+2;
then
A9: i+1<len f by A5,NAT_1:13;
then
A10: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A4,TOPREAL1:def 3;
f/.(i+1) in LSeg(f/.i,f/.(i+1)) & f/.(i+1) in LSeg(f/.(i+1),f/.(i+1+1
)) by RLTOPSP1:68;
then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by A10,A7,XBOOLE_0:def 4;
then
A11: {f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:31;
A12: i<len f by A9,NAT_1:13;
per cases;
suppose
i=1;
hence thesis by A2,A11;
end;
suppose
A13: i<>1;
now
per cases;
case
A14: i+2=len f;
then len f-2=len f-'2 & len f-1=len f-'1 by A4,A6,NAT_D:39;
hence thesis by A3,A11,A14;
end;
case
A15: i+2<>len f;
1<i by A4,A13,XXREAL_0:1;
then 1+1<=i by NAT_1:13;
then
A16: 1+1-1<=i-1 by XREAL_1:9;
i+2<len f by A5,A15,XXREAL_0:1;
then
A17: i+1+1+1<=len f by NAT_1:13;
now
f/.(i+1) in LSeg(f,i+1) & f/.(i+1) in LSeg(f,i) by A10,A7,
RLTOPSP1:68;
then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by XBOOLE_0:def 4;
then
A18: {f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:31;
assume LSeg(f,i) /\ LSeg(f,i+1)<>{f/.(i+1)};
then not LSeg(f,i) /\ LSeg(f,i+1) c= {f/.(i+1)} by A18;
then consider x being object such that
A19: x in LSeg(f,i) /\ LSeg(f,i+1) and
A20: not x in {f/.(i+1)};
A21: LSeg(f,i+1+1)=LSeg(f/.(i+1+1),f/.(i+1+1+1)) by A8,A17,
TOPREAL1:def 3;
A22: x<>f/.(i+1) by A20,TARSKI:def 1;
now
per cases by A10,A7,A19,A22,Th16;
case
A23: f/.i in LSeg(f/.(i+1),f/.(i+1+1));
A24: i-'1=i-1 by A4,XREAL_1:233;
then i-'1+1<i+1 by NAT_1:13;
then LSeg(f,i-'1) misses LSeg(f,i+1) by A1,TOPREAL1:def 7;
then
A25: LSeg(f,i-'1)/\ LSeg(f,i+1)={};
LSeg(f,i-'1)=LSeg(f/.(i-'1),f/.(i-'1+1)) by A12,A16,A24,
TOPREAL1:def 3;
then f/.i in LSeg(f,i-'1) by A24,RLTOPSP1:68;
hence contradiction by A7,A23,A25,XBOOLE_0:def 4;
end;
case
A26: f/.(i+1+1) in LSeg(f/.i,f/.(i+1));
i+1<i+1+1 by NAT_1:13;
then LSeg(f,i) misses LSeg(f,i+1+1) by A1,TOPREAL1:def 7;
then
A27: LSeg(f,i)/\ LSeg(f,i+1+1)={};
f/.(i+1+1) in LSeg(f,i+1+1) by A21,RLTOPSP1:68;
hence contradiction by A10,A26,A27,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis by TOPREAL1:def 6;
end;
theorem Th18:
for f being FinSequence of X holds PairF(f) is Simple & f.1<>f.
len f implies f is one-to-one & len f<>1
proof
let f be FinSequence of X;
thus PairF(f) is Simple & f.1<>f.len f implies f is one-to-one & len f<>1
proof
reconsider f1=f as FinSequence of the carrier of PGraph(X);
assume that
A1: PairF(f) is Simple and
A2: f.1<>f.len f;
consider vs being FinSequence of the carrier of PGraph(X) such that
A3: vs is_oriented_vertex_seq_of PairF(f) and
A4: for n,m being Nat
st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
by A1,GRAPH_4:def 7;
now
per cases;
case
A5: len f>=1;
now
per cases by A5,XXREAL_0:1;
case
A6: len f>1;
A7: f1 is_oriented_vertex_seq_of PairF(f) by A5,Th7;
then len f1=len PairF(f)+1 by GRAPH_4:def 5;
then 1-1<len PairF(f)+1-1 by A6,XREAL_1:9;
then PairF(f) <> {};
then
A8: vs = f1 by A3,A7,GRAPH_4:10;
for x,y being object st x in dom f & y in dom f & f.x=f.y holds x=y
proof
let x,y be object;
assume that
A9: x in dom f and
A10: y in dom f and
A11: f.x=f.y;
reconsider i=x,j=y as Element of NAT by A9,A10;
A12: dom f=Seg len f by FINSEQ_1:def 3;
then
A13: i<=len f by A9,FINSEQ_1:1;
A14: j<=len f by A10,A12,FINSEQ_1:1;
A15: 1<=j by A10,A12,FINSEQ_1:1;
A16: 1<=i by A9,A12,FINSEQ_1:1;
now
assume
A17: i<>j;
now
per cases by A17,XXREAL_0:1;
case
A18: i<j;
then i=1 by A4,A8,A11,A16,A14;
hence contradiction by A2,A4,A8,A11,A14,A18;
end;
case
A19: j<i;
then j=1 by A4,A8,A11,A13,A15;
hence contradiction by A2,A4,A8,A11,A13,A19;
end;
end;
hence contradiction;
end;
hence thesis;
end;
hence f is one-to-one;
end;
case
len f=1;
hence f is one-to-one by A2;
end;
end;
hence f is one-to-one;
end;
case
len f<1;
then len f+1<=1 by NAT_1:13;
then len f+1-1<=1-1 by XREAL_1:9;
then len f=0;
then Seg len f={};
then for x,y being object st x in dom f & y in dom f & f.x=f.y
holds x=y by
FINSEQ_1:def 3;
hence f is one-to-one;
end;
end;
hence thesis by A2;
end;
end;
theorem
for f being FinSequence of X holds f is one-to-one & len f>1 implies
PairF(f) is Simple & f.1<>f.len f
proof
let f be FinSequence of X;
assume that
A1: f is one-to-one and
A2: len f>1;
A3: 1 in dom f & len f in dom f by A2,FINSEQ_3:25;
reconsider f1=f as FinSequence of the carrier of PGraph(X);
A4: for i,j being Nat
st 1<=i & i<j & j<=len f1 & f1.i=f1.j holds i=1 & j=len f1
proof
let i,j be Nat;
assume that
A5: 1<=i and
A6: i<j and
A7: j<=len f1 and
A8: f1.i=f1.j;
1<j by A5,A6,XXREAL_0:2;
then j in Seg len f by A7,FINSEQ_1:1;
then
A9: j in dom f by FINSEQ_1:def 3;
i<len f by A6,A7,XXREAL_0:2;
then i in Seg len f by A5,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
hence thesis by A1,A6,A8,A9;
end;
f1 is_oriented_vertex_seq_of PairF(f) by A2,Th7;
hence thesis by A1,A2,A3,A4,GRAPH_4:def 7;
end;
theorem
for f being FinSequence of TOP-REAL 2 st f is nodic & PairF(f) is
Simple & f.1<>f.len f holds f is unfolded
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is nodic and
A2: PairF(f) is Simple & f.1<>f.len f;
per cases;
suppose
A3: 2<len f;
then
A4: 2+1<=len f by NAT_1:13;
then
A5: 2+1 in dom f by FINSEQ_3:25;
A6: f.2=f/.2 by A3,FINSEQ_4:15;
then
A7: f.2 in LSeg(f,2) by A4,TOPREAL1:21;
1+1<=len f by A3;
then f.2 in LSeg(f,1) by A6,TOPREAL1:21;
then LSeg(f,1)/\ LSeg(f,2)<>{} by A7,XBOOLE_0:def 4;
then
A8: LSeg(f,1) meets LSeg(f,2);
A9: len f<len f+1 by NAT_1:13;
then
A10: len f-1<len f by XREAL_1:19;
A11: 2 in dom f by A3,FINSEQ_3:25;
A12: LSeg(f,1)=LSeg(f/.1,f/.(1+1)) by A3,TOPREAL1:def 3;
A13: f is one-to-one by A2,Th18;
A14: 1<len f by A3,XXREAL_0:2;
then
A15: 1 in dom f by FINSEQ_3:25;
A16: f.1=f/.1 by A14,FINSEQ_4:15;
A17: len f-'2=len f-2 by A3,XREAL_1:233;
A18: LSeg(f,2)=LSeg(f/.2,f/.(2+1)) by A4,TOPREAL1:def 3;
now
assume
A19: LSeg(f,1)=LSeg(f,2);
now
per cases by A12,A18,A19,SPPOL_1:8;
case
A20: f/.1=f/.2 & f/.(1+1)=f/.(2+1);
f.1=f/.1 & f.2=f/.2 by A3,A14,FINSEQ_4:15;
hence contradiction by A13,A15,A11,A20;
end;
case
A21: f/.1=f/.(2+1) & f/.(1+1)=f/.2;
f.(2+1)=f/.(2+1) by A4,FINSEQ_4:15;
hence contradiction by A13,A15,A16,A5,A21;
end;
end;
hence contradiction;
end;
then LSeg(f,1) /\ LSeg(f,2)={f.1} &(f.1=f.2 or f.1=f.(2+1)) or LSeg(f,1)
/\ LSeg(f,2)={f.(1+1)} &(f.(1+1)=f.2 or f.(1+1)=f.(2+1)) by A1,A8;
then
A22: LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} by A3,A13,A15,A5,FINSEQ_4:15;
A23: len f-1=len f-'1 by A3,XREAL_1:233,XXREAL_0:2;
then
A24: len f-'1+1 in dom f by A14,FINSEQ_3:25;
A25: 1+1-1<=len f-1 by A3,XREAL_1:9;
then
A26: f.(len f-'1)=f/.(len f-'1) by A23,A10,FINSEQ_4:15;
A27: 2+1-2<=len f-2 by A4,XREAL_1:9;
then
A28: LSeg(f,(len f-'2))=LSeg(f/.(len f-'2),f/.((len f-'2)+1)) by A17,A10,
TOPREAL1:def 3;
A29: len f-1-1<len f-1 by A10,XREAL_1:9;
then len f-2<len f by A10,XXREAL_0:2;
then
A30: f.(len f-'2)=f/.(len f-'2) by A27,A17,FINSEQ_4:15;
A31: len f-'2<len f by A17,A10,A29,XXREAL_0:2;
then
A32: len f-'2 in dom f by A27,A17,FINSEQ_3:25;
A33: LSeg(f,(len f-'1))=LSeg(f/.(len f-'1),f/.((len f-'1)+1)) by A25,A23,
TOPREAL1:def 3;
A34: f.(len f-'2)=f/.(len f-'2) by A27,A17,A31,FINSEQ_4:15;
A35: now
assume
A36: LSeg(f,(len f-'2))=LSeg(f,(len f-'1));
A37: (len f-'2) in dom f by A27,A17,A31,FINSEQ_3:25;
A38: (len f-'1) in dom f by A25,A23,A10,FINSEQ_3:25;
now
per cases by A28,A33,A36,SPPOL_1:8;
case
A39: f/.(len f-'2)=f/.(len f-'1) & f/.((len f-'2)+1)=f/.((len f -'1)+1);
f.(len f-'1)=f/.(len f-'1) by A25,A23,A10,FINSEQ_4:15;
hence contradiction by A13,A23,A17,A9,A34,A37,A38,A39;
end;
case
A40: f/.(len f-'2)=f/.((len f-'1)+1) & f/.((len f-'2)+1)=f/.(len f-'1);
(len f-'1)+1 in Seg len f by A14,A23,FINSEQ_1:1;
then
A41: (len f-'1)+1 in dom f by FINSEQ_1:def 3;
f.((len f-'1)+1)=f/.((len f-'1)+1) by A14,A23,FINSEQ_4:15;
hence contradiction by A13,A23,A17,A10,A29,A30,A37,A40,A41;
end;
end;
hence contradiction;
end;
len f-'1+1=len f by A23;
then
A42: f.(len f-'1) in LSeg(f,(len f-'1)) by A25,A26,TOPREAL1:21;
len f-'2+1=len f-(1+1-1) by A17;
then f.(len f-'1) in LSeg(f,(len f-'2)) by A27,A23,A10,A26,TOPREAL1:21;
then LSeg(f,(len f-'2))/\ LSeg(f,(len f-'1))<>{} by A42,XBOOLE_0:def 4;
then LSeg(f,(len f-'2)) meets LSeg(f,(len f-'1));
then
LSeg(f,(len f-'2)) /\ LSeg(f,(len f-'1))={f.(len f-'2)} &(f.(len f-'2
)=f.(len f-'1) or f.(len f-'2)=f.((len f-'1)+1)) or LSeg(f,(len f-'2)) /\ LSeg(
f,(len f-'1))={f.((len f-'2)+1)} &(f.((len f-'2)+1)=f.(len f-'1) or f.((len f-'
2)+1)=f.((len f-'1)+1)) by A1,A35;
then
LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)} by A13,A25,A23,A17
,A10,A29,A32,A24,FINSEQ_4:15;
hence thesis by A1,A2,A22,Th15,Th17;
end;
suppose
A43: len f<=2;
for i be Nat st 1 <= i & i + 2 <= len f holds LSeg(f,i) /\ LSeg(f,i+1
) = {f/.(i+1)}
proof
let i be Nat;
assume that
A44: 1 <= i and
A45: i + 2 <= len f;
i+2<=2 by A43,A45,XXREAL_0:2;
then i<=2-2 by XREAL_1:19;
hence thesis by A44,XXREAL_0:2;
end;
hence thesis by TOPREAL1:def 6;
end;
end;
theorem Th21:
for f,g being FinSequence of TOP-REAL 2,i st g is_Shortcut_of f
& 1 <= i & i+1 <= len g holds ex k1 being Element of NAT st 1<=k1 & k1+1<=len f
& f/.k1=g/.i & f/.(k1+1)=g/.(i+1) & f.k1=g.i & f.(k1+1)=g.(i+1)
proof
let f,g be FinSequence of TOP-REAL 2,i;
assume that
A1: g is_Shortcut_of f and
A2: 1 <= i and
A3: i+1 <= len g;
A4: len PairF(g)=len g -'1 by Def2;
A5: i<len g by A3,NAT_1:13;
then
A6: (PairF(g)).i=[g.i,g.(i+1)] by A2,Def2;
1<=i+1 by A2,NAT_1:13;
then
A7: g/.(i+1)=g.(i+1) by A3,FINSEQ_4:15;
i<=len g by A3,NAT_1:13;
then
A8: g/.i=g.i by A2,FINSEQ_4:15;
A9: len g<=len f by A1,Th8;
1<len g by A2,A5,XXREAL_0:2;
then
A10: len f-'1=len f-1 by A9,XREAL_1:233,XXREAL_0:2;
A11: len PairF(f)=len f-'1 by Def2;
A12: i<=len g-1 by A3,XREAL_1:19;
then 1<=len g-1 by A2,XXREAL_0:2;
then len g-'1=len g-1 by NAT_D:39;
then i in dom (PairF(g)) by A2,A4,A12,FINSEQ_3:25;
then
A13: [ g.i,g.(i+1) ] in rng PairF(g) by A6,FUNCT_1:def 3;
rng PairF(g) c= rng PairF(f) by A1,Th10;
then consider x being object such that
A14: x in dom PairF(f) and
A15: (PairF(f)).x=[g.i,g.(i+1)] by A13,FUNCT_1:def 3;
reconsider k=x as Element of NAT by A14;
A16: x in Seg len PairF(f) by A14,FINSEQ_1:def 3;
then
A17: 1<=k by FINSEQ_1:1;
k<=len PairF(f) by A16,FINSEQ_1:1;
then
A18: k+1<=len f-1+1 by A11,A10,XREAL_1:6;
then
A19: k<len f by NAT_1:13;
then [ g.i,g.(i+1)]=[ f.k,f.(k+1) ] by A15,A17,Def2;
then
A20: g.i=f.k & g.(i+1)=f.(k+1) by XTUPLE_0:1;
1<k+1 by A17,NAT_1:13;
then
A21: f/.(k+1)=f.(k+1) by A18,FINSEQ_4:15;
f/.k=f.k by A17,A19,FINSEQ_4:15;
hence thesis by A17,A18,A20,A8,A7,A21;
end;
theorem Th22:
for f,g being FinSequence of TOP-REAL 2 st g is_Shortcut_of f
holds rng g c= rng f
proof
let f,g be FinSequence of TOP-REAL 2;
assume
A1: g is_Shortcut_of f;
let x be object;
assume x in rng g;
then consider z being object such that
A2: z in dom g and
A3: x=g.z by FUNCT_1:def 3;
reconsider i=z as Element of NAT by A2;
A4: z in Seg len g by A2,FINSEQ_1:def 3;
then
A5: 1<=i by FINSEQ_1:1;
A6: i<=len g by A4,FINSEQ_1:1;
per cases;
suppose
i<len g;
then i+1<=len g by NAT_1:13;
then consider k1 being Element of NAT such that
A7: 1<=k1 and
A8: k1+1<=len f and
f/.k1=g/.i and
f/.(k1+1)=g/.(i+1) and
A9: f.k1=g.i and
f.(k1+1)=g.(i+1) by A1,A5,Th21;
k1<len f by A8,NAT_1:13;
then k1 in dom f by A7,FINSEQ_3:25;
hence thesis by A3,A9,FUNCT_1:def 3;
end;
suppose
i>=len g;
then
A10: i=len g by A6,XXREAL_0:1;
now
per cases;
case
A11: 1<i;
then
A12: i-'1=i-1 by XREAL_1:233;
1-1<i-1 by A11,XREAL_1:9;
then 0<i-'1 by A11,XREAL_1:233;
then 0 qua Nat+1<=i-'1 by NAT_1:13;
then consider k1 being Element of NAT such that
A13: 1<=k1 and
A14: k1+1<=len f and
f/.k1=g/.(i-'1) and
f/.(k1+1)=g/.(i-'1+1) and
f.k1=g.(i-'1) and
A15: f.(k1+1)=g.(i-'1+1) by A1,A6,A12,Th21;
1<k1+1 by A13,NAT_1:13;
then k1+1 in dom f by A14,FINSEQ_3:25;
hence thesis by A3,A12,A15,FUNCT_1:def 3;
end;
case
1>=i;
then
A16: i=1 by A5,XXREAL_0:1;
A17: f.1=g.1 by A1;
len g<=len f by A1,Th8;
then 1 in dom f by A10,A16,FINSEQ_3:25;
hence thesis by A3,A16,A17,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
end;
theorem Th23:
for f,g being FinSequence of TOP-REAL 2 st g is_Shortcut_of f
holds L~g c= L~f
proof
let f,g be FinSequence of TOP-REAL 2;
assume
A1: g is_Shortcut_of f;
let x be object;
assume x in L~g;
then x in union { LSeg(g,i) : 1 <= i & i+1 <= len g } by TOPREAL1:def 4;
then consider y such that
A2: x in y & y in { LSeg(g,i) : 1 <= i & i+1 <= len g } by TARSKI:def 4;
consider i such that
A3: y=LSeg(g,i) and
A4: 1<=i & i+1<=len g by A2;
consider k1 being Element of NAT such that
A5: 1<=k1 & k1+1<=len f and
A6: f/.k1=g/.i & f/.(k1+1)=g/.(i+1) and
f.k1=g.i and
f.(k1+1)=g.(i+1) by A1,A4,Th21;
A7: LSeg(f,k1) in {LSeg(f,k):1<=k & k+1<=len f} by A5;
x in LSeg(g/.i,g/.(i+1)) by A2,A3,A4,TOPREAL1:def 3;
then x in LSeg(f,k1) by A5,A6,TOPREAL1:def 3;
then x in union { LSeg(f,k) : 1 <= k & k+1 <= len f } by A7,TARSKI:def 4;
hence thesis by TOPREAL1:def 4;
end;
theorem Th24:
for f,g being FinSequence of TOP-REAL 2 st f is special & g
is_Shortcut_of f holds g is special
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f is special and
A2: g is_Shortcut_of f;
for i be Nat st 1 <= i & i+1 <= len g holds (g/.i)`1 = (g/.(i+1))`1 or (
g/.i)`2 = (g/.(i+1))`2
proof
A3: len g<=len f by A2,Th8;
A4: len PairF(g)=len g -'1 by Def2;
let i be Nat;
assume that
A5: 1 <= i and
A6: i+1 <= len g;
i<=len g by A6,NAT_1:13;
then
A7: g/.i=g.i by A5,FINSEQ_4:15;
A8: i<len g by A6,NAT_1:13;
then 1<len g by A5,XXREAL_0:2;
then
A9: len f-'1=len f-1 by A3,XREAL_1:233,XXREAL_0:2;
A10: i<=len g-1 by A6,XREAL_1:19;
then 1<=len g-1 by A5,XXREAL_0:2;
then len g-'1=len g-1 by NAT_D:39;
then
A11: i in dom PairF(g) by A5,A4,A10,FINSEQ_3:25;
(PairF(g)).i=[g.i,g.(i+1)] by A5,A8,Def2;
then
A12: [ (g.i),(g.(i+1)) ] in rng PairF(g) by A11,FUNCT_1:def 3;
rng PairF(g) c= rng PairF(f) by A2,Th10;
then consider x being object such that
A13: x in dom PairF(f) and
A14: (PairF(f)).x=[g.i,g.(i+1)] by A12,FUNCT_1:def 3;
reconsider k=x as Element of NAT by A13;
A15: x in Seg len PairF(f) by A13,FINSEQ_1:def 3;
then
A16: 1<=k by FINSEQ_1:1;
1<=i+1 by A5,NAT_1:13;
then
A17: g/.(i+1)=g.(i+1) by A6,FINSEQ_4:15;
A18: len PairF(f)=len f-'1 by Def2;
k<=len PairF(f) by A15,FINSEQ_1:1;
then
A19: k+1<=len f-1+1 by A18,A9,XREAL_1:6;
then
A20: k<len f by NAT_1:13;
then (PairF(f)).k=[f.k,f.(k+1)] by A16,Def2;
then
A21: g.i=f.k & g.(i+1)=f.(k+1) by A14,XTUPLE_0:1;
1<k+1 by A16,NAT_1:13;
then
A22: f/.(k+1)=f.(k+1) by A19,FINSEQ_4:15;
f/.k=f.k by A16,A20,FINSEQ_4:15;
hence thesis by A1,A16,A19,A21,A7,A17,A22,TOPREAL1:def 5;
end;
hence thesis by TOPREAL1:def 5;
end;
theorem Th25:
for f being FinSequence of TOP-REAL 2 st f is special & 2<=len f
& f.1 <> f.len f holds ex g being FinSequence of TOP-REAL 2 st 2<=len g & g is
special & g is one-to-one & L~g c= L~f & f.1=g.1 & f.len f=g.len g & rng g c=
rng f
proof
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is special and
A2: 2<=len f and
A3: f.1 <> f.len f;
consider g being FinSequence of TOP-REAL 2 such that
A4: g is_Shortcut_of f by A2,Th9,XXREAL_0:2;
A5: g.1=f.1 & g.len g=f.len f by A4;
1<=len g by A4,Th8;
then 1<len g by A3,A5,XXREAL_0:1;
then
A6: 1+1<=len g by NAT_1:13;
A7: L~g c= L~f & rng g c= rng f by A4,Th22,Th23;
g is one-to-one by A3,A4,Th11;
hence thesis by A1,A4,A7,A6,Th24;
end;
:: Goboard Theorem for general special sequences
theorem Th26:
for f1,f2 being FinSequence of TOP-REAL 2 st f1 is special & f2
is special & 2<=len f1 & 2<=len f2 & f1.1<>f1.len f1 & f2.1<>f2.len f2 & X_axis
(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & X_axis(f2)
lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1) lies_between (
Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2) lies_between (Y_axis(f2)).1,
(Y_axis(f2)).(len f2) holds L~f1 meets L~f2
proof
let f1,f2 be FinSequence of TOP-REAL 2;
assume that
A1: f1 is special and
A2: f2 is special and
A3: 2<=len f1 and
A4: 2<=len f2 and
A5: f1.1<>f1.len f1 and
A6: f2.1<>f2.len f2 and
A7: X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) and
A8: X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) and
A9: Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) and
A10: Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2);
consider g1 being FinSequence of TOP-REAL 2 such that
A11: 2<=len g1 and
A12: g1 is special and
A13: g1 is one-to-one and
A14: L~g1 c= L~f1 and
A15: f1.1=g1.1 and
A16: f1.len f1=g1.len g1 and
A17: rng g1 c= rng f1 by A1,A3,A5,Th25;
consider g2 being FinSequence of TOP-REAL 2 such that
A18: 2<=len g2 and
A19: g2 is special and
A20: g2 is one-to-one and
A21: L~g2 c= L~f2 and
A22: f2.1=g2.1 and
A23: f2.len f2=g2.len g2 and
A24: rng g2 c= rng f2 by A2,A4,A6,Th25;
A25: for k being Nat st k in dom g2 & k+1 in dom g2 holds g2/.k
<> g2/.(k+1)
proof
let k be Nat;
assume that
A26: k in dom g2 and
A27: k+1 in dom g2;
A28: g2.k=g2/.k by A26,PARTFUN1:def 6;
k<k+1 by NAT_1:13;
then g2.k<>g2.(k+1) by A20,A26,A27;
hence thesis by A27,A28,PARTFUN1:def 6;
end;
for i st i in dom Y_axis(g1) holds (Y_axis(g2)).1 <= Y_axis(g1).i &
Y_axis(g1).i <= (Y_axis(g2)).(len g2)
proof
let i;
A29: len (Y_axis(f2)) = len f2 by GOBOARD1:def 2;
A30: 1<=len f2 by A4,XXREAL_0:2;
then 1 in Seg len f2 by FINSEQ_1:1;
then
A31: 1 in dom (Y_axis(f2)) by A29,FINSEQ_1:def 3;
len f2 in Seg len f2 by A30,FINSEQ_1:1;
then
A32: len f2 in dom (Y_axis(f2)) by A29,FINSEQ_1:def 3;
A33: len (Y_axis(g2)) = len g2 by GOBOARD1:def 2;
A34: 1<=len g2 by A18,XXREAL_0:2;
then 1 in Seg len g2 by FINSEQ_1:1;
then
A35: 1 in dom (Y_axis(g2)) by A33,FINSEQ_1:def 3;
g2/.1=g2.1 by A34,FINSEQ_4:15;
then
A36: g2/.1=f2/.1 by A22,A30,FINSEQ_4:15;
len g2 in Seg len g2 by A34,FINSEQ_1:1;
then
A37: len g2 in dom (Y_axis(g2)) by A33,FINSEQ_1:def 3;
g2/.len g2=g2.(len g2) by A34,FINSEQ_4:15;
then
A38: g2/.len g2=f2/.len f2 by A23,A30,FINSEQ_4:15;
assume
A39: i in dom Y_axis(g1);
then
A40: Y_axis(g1).i = (g1/.i)`2 by GOBOARD1:def 2;
len (Y_axis(g1)) = len g1 by GOBOARD1:def 2;
then i in Seg len g1 by A39,FINSEQ_1:def 3;
then
A41: i in dom g1 by FINSEQ_1:def 3;
then g1.i in rng g1 by FUNCT_1:def 3;
then consider y being object such that
A42: y in dom f1 and
A43: g1.i=f1.y by A17,FUNCT_1:def 3;
reconsider j=y as Element of NAT by A42;
f1.j=f1/.j by A42,PARTFUN1:def 6;
then
A44: g1/.i=f1/.j by A41,A43,PARTFUN1:def 6;
len (Y_axis(f1)) = len f1 & j in Seg len f1 by A42,FINSEQ_1:def 3
,GOBOARD1:def 2;
then
A45: j in dom (Y_axis(f1)) by FINSEQ_1:def 3;
then
A46: Y_axis(f1).j =(f1/.j)`2 by GOBOARD1:def 2;
Y_axis(f1).j <= (Y_axis(f2)).(len f2) by A9,A45,GOBOARD4:def 2;
then
A47: (g1/.i)`2<=(g2/.len g2)`2 by A38,A44,A46,A32,GOBOARD1:def 2;
(Y_axis(f2)).1 <= Y_axis(f1).j by A9,A45,GOBOARD4:def 2;
then (g2/.1)`2<=(g1/.i)`2 by A36,A31,A44,A46,GOBOARD1:def 2;
hence thesis by A35,A47,A40,A37,GOBOARD1:def 2;
end;
then
A48: Y_axis(g1) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2) by
GOBOARD4:def 2;
for i st i in dom X_axis(g2) holds (X_axis(g1)).1 <= X_axis(g2).i &
X_axis(g2).i <= (X_axis(g1)).(len g1)
proof
let i;
A49: len (X_axis(f1)) = len f1 by GOBOARD1:def 1;
A50: 1<=len f1 by A3,XXREAL_0:2;
then 1 in Seg len f1 by FINSEQ_1:1;
then
A51: 1 in dom (X_axis(f1)) by A49,FINSEQ_1:def 3;
len f1 in Seg len f1 by A50,FINSEQ_1:1;
then
A52: len f1 in dom (X_axis(f1)) by A49,FINSEQ_1:def 3;
A53: len (X_axis(g1)) = len g1 by GOBOARD1:def 1;
A54: 1<=len g1 by A11,XXREAL_0:2;
then 1 in Seg len g1 by FINSEQ_1:1;
then
A55: 1 in dom (X_axis(g1)) by A53,FINSEQ_1:def 3;
g1/.1=g1.1 by A54,FINSEQ_4:15;
then
A56: g1/.1=f1/.1 by A15,A50,FINSEQ_4:15;
len g1 in Seg len g1 by A54,FINSEQ_1:1;
then
A57: len g1 in dom (X_axis(g1)) by A53,FINSEQ_1:def 3;
g1/.len g1=g1.(len g1) by A54,FINSEQ_4:15;
then
A58: g1/.len g1=f1/.len f1 by A16,A50,FINSEQ_4:15;
assume
A59: i in dom X_axis(g2);
then
A60: X_axis(g2).i =(g2/.i)`1 by GOBOARD1:def 1;
len (X_axis(g2)) = len g2 by GOBOARD1:def 1;
then i in Seg len g2 by A59,FINSEQ_1:def 3;
then
A61: i in dom g2 by FINSEQ_1:def 3;
then g2.i in rng g2 by FUNCT_1:def 3;
then consider y being object such that
A62: y in dom f2 and
A63: g2.i=f2.y by A24,FUNCT_1:def 3;
reconsider j=y as Element of NAT by A62;
f2.j=f2/.j by A62,PARTFUN1:def 6;
then
A64: g2/.i=f2/.j by A61,A63,PARTFUN1:def 6;
len (X_axis(f2)) = len f2 & j in Seg len f2 by A62,FINSEQ_1:def 3
,GOBOARD1:def 1;
then
A65: j in dom (X_axis(f2)) by FINSEQ_1:def 3;
then
A66: X_axis(f2).j =(f2/.j)`1 by GOBOARD1:def 1;
X_axis(f2).j <= (X_axis(f1)).(len f1) by A8,A65,GOBOARD4:def 2;
then
A67: (g2/.i)`1<=(g1/.len g1)`1 by A58,A64,A66,A52,GOBOARD1:def 1;
(X_axis(f1)).1 <= X_axis(f2).j by A8,A65,GOBOARD4:def 2;
then (g1/.1)`1<=(g2/.i)`1 by A56,A51,A64,A66,GOBOARD1:def 1;
hence thesis by A55,A67,A60,A57,GOBOARD1:def 1;
end;
then
A68: X_axis(g2) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1) by
GOBOARD4:def 2;
for i st i in dom Y_axis(g2) holds (Y_axis(g2)).1 <= Y_axis(g2).i &
Y_axis(g2).i <= (Y_axis(g2)).(len g2)
proof
let i;
A69: len (Y_axis(f2)) = len f2 by GOBOARD1:def 2;
A70: 1<=len f2 by A4,XXREAL_0:2;
then 1 in Seg len f2 by FINSEQ_1:1;
then
A71: 1 in dom (Y_axis(f2)) by A69,FINSEQ_1:def 3;
A72: 1<=len g2 by A18,XXREAL_0:2;
then g2/.1=g2.1 by FINSEQ_4:15;
then
A73: g2/.1=f2/.1 by A22,A70,FINSEQ_4:15;
A74: len (Y_axis(g2)) = len g2 by GOBOARD1:def 2;
then len g2 in Seg len (Y_axis(g2)) by A72,FINSEQ_1:1;
then
A75: len g2 in dom (Y_axis(g2)) by FINSEQ_1:def 3;
g2/.len g2=g2.(len g2) by A72,FINSEQ_4:15;
then
A76: g2/.len g2=f2/.len f2 by A23,A70,FINSEQ_4:15;
1 in Seg len g2 by A72,FINSEQ_1:1;
then
A77: 1 in dom (Y_axis(g2)) by A74,FINSEQ_1:def 3;
len f2 in Seg len f2 by A70,FINSEQ_1:1;
then
A78: len f2 in dom (Y_axis(f2)) by A69,FINSEQ_1:def 3;
assume
A79: i in dom Y_axis(g2);
then
A80: Y_axis(g2).i =(g2/.i)`2 by GOBOARD1:def 2;
i in Seg len g2 by A79,A74,FINSEQ_1:def 3;
then
A81: i in dom g2 by FINSEQ_1:def 3;
then g2.i in rng g2 by FUNCT_1:def 3;
then consider y being object such that
A82: y in dom f2 and
A83: g2.i=f2.y by A24,FUNCT_1:def 3;
reconsider j=y as Element of NAT by A82;
f2.j=f2/.j by A82,PARTFUN1:def 6;
then
A84: g2/.i=f2/.j by A81,A83,PARTFUN1:def 6;
j in Seg len f2 by A82,FINSEQ_1:def 3;
then
A85: j in dom (Y_axis(f2)) by A69,FINSEQ_1:def 3;
then
A86: Y_axis(f2).j =(f2/.j)`2 by GOBOARD1:def 2;
Y_axis(f2).j <= (Y_axis(f2)).(len f2) by A10,A85,GOBOARD4:def 2;
then
A87: (g2/.i)`2<=(g2/.len g2)`2 by A76,A84,A86,A78,GOBOARD1:def 2;
(Y_axis(f2)).1 <= Y_axis(f2).j by A10,A85,GOBOARD4:def 2;
then (g2/.1)`2<=(g2/.i)`2 by A73,A71,A84,A86,GOBOARD1:def 2;
hence thesis by A77,A87,A80,A75,GOBOARD1:def 2;
end;
then
A88: Y_axis(g2) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2) by
GOBOARD4:def 2;
for i st i in dom X_axis(g1) holds (X_axis(g1)).1 <= X_axis(g1).i &
X_axis(g1).i <= (X_axis(g1)).(len g1)
proof
let i;
A89: len (X_axis(f1)) = len f1 by GOBOARD1:def 1;
assume
A90: i in dom X_axis(g1);
then
A91: X_axis(g1).i = (g1/.i)`1 by GOBOARD1:def 1;
A92: 1<=len f1 by A3,XXREAL_0:2;
then len f1 in Seg len f1 by FINSEQ_1:1;
then
A93: len f1 in dom (X_axis(f1)) by A89,FINSEQ_1:def 3;
A94: 1<=len g1 by A11,XXREAL_0:2;
then g1/.1=g1.1 by FINSEQ_4:15;
then
A95: g1/.1=f1/.1 by A15,A92,FINSEQ_4:15;
g1/.len g1=g1.(len g1) by A94,FINSEQ_4:15;
then
A96: g1/.len g1=f1/.len f1 by A16,A92,FINSEQ_4:15;
A97: len (X_axis(g1)) = len g1 by GOBOARD1:def 1;
then
A98: 1 in dom X_axis(g1) by A94,FINSEQ_3:25;
i in Seg len g1 by A90,A97,FINSEQ_1:def 3;
then
A99: i in dom g1 by FINSEQ_1:def 3;
then g1.i in rng g1 by FUNCT_1:def 3;
then consider y being object such that
A100: y in dom f1 and
A101: g1.i=f1.y by A17,FUNCT_1:def 3;
reconsider j=y as Element of NAT by A100;
f1.j=f1/.j by A100,PARTFUN1:def 6;
then
A102: g1/.i=f1/.j by A99,A101,PARTFUN1:def 6;
len g1 in Seg len g1 by A94,FINSEQ_1:1;
then
A103: len g1 in dom (X_axis(g1)) by A97,FINSEQ_1:def 3;
j in Seg len f1 by A100,FINSEQ_1:def 3;
then
A104: j in dom (X_axis(f1)) by A89,FINSEQ_1:def 3;
then
A105: X_axis(f1).j =(f1/.j)`1 by GOBOARD1:def 1;
X_axis(f1).j <= (X_axis(f1)).(len f1) by A7,A104,GOBOARD4:def 2;
then
A106: (g1/.i)`1<=(g1/.len g1)`1 by A96,A102,A105,A93,GOBOARD1:def 1;
A107: (X_axis(f1)).1 <= X_axis(f1).j by A7,A104,GOBOARD4:def 2;
1 in dom X_axis(f1) by A89,A92,FINSEQ_3:25;
then (g1/.1)`1<=(g1/.i)`1 by A95,A102,A107,A105,GOBOARD1:def 1;
hence thesis by A98,A106,A91,A103,GOBOARD1:def 1;
end;
then
A108: X_axis(g1) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1) by
GOBOARD4:def 2;
for k being Nat st k in dom g1 & k+1 in dom g1 holds g1/.k
<> g1/.(k+1)
proof
let k be Nat;
assume that
A109: k in dom g1 and
A110: k+1 in dom g1;
A111: g1.k=g1/.k by A109,PARTFUN1:def 6;
k<k+1 by NAT_1:13;
then g1.k<>g1.(k+1) by A13,A109,A110;
hence thesis by A110,A111,PARTFUN1:def 6;
end;
then L~g1 meets L~g2 by A11,A12,A18,A19,A108,A68,A48,A88,A25,GOBOARD4:4;
then L~g1 /\ L~g2 <> {};
then L~f1 /\ L~f2 <> {} by A14,A21,XBOOLE_1:3,27;
hence thesis;
end;
begin :: NORM OF POINTS IN TOPREAL n
theorem Th27:
for a,b,r1,r2 being Real st a<=r1 & r1<=b & a<=r2 & r2<=b holds
|.r1-r2.|<=b-a
proof
let a,b,r1,r2 be Real;
assume that
A1: a<=r1 and
A2: r1<=b & a<=r2 and
A3: r2<=b;
per cases;
suppose
A4: r1-r2>=0;
A5: r1-r2<=b-r2 & b-r2<=b-a by A2,XREAL_1:9,10;
|.r1-r2.|=r1-r2 by A4,ABSVALUE:def 1;
hence thesis by A5,XXREAL_0:2;
end;
suppose
r1-r2<0;
then
A6: |.r1-r2.|=-(r1-r2) by ABSVALUE:def 1
.=r2-r1;
r2-r1<=b-r1 & b-r1<=b-a by A1,A3,XREAL_1:9,10;
hence thesis by A6,XXREAL_0:2;
end;
end;
reserve p,p1,p2 for Point of TOP-REAL N;
theorem Th28:
for x1,x2 being Point of Euclid N st x1=p1 & x2=p2 holds |.p1 -
p2.| = dist(x1,x2)
proof
let x1,x2 be Point of Euclid N;
assume
A1: x1=p1 & x2=p2;
reconsider x19=x1,x29=x2 as Element of REAL N;
(Pitag_dist N).(x19,x29) = |.x19-x29.| by EUCLID:def 6
.=|.p1-p2.| by A1;
hence thesis by METRIC_1:def 1;
end;
theorem Th29:
for p being Point of TOP-REAL 2 holds |.p.|^2 = (p`1)^2+(p`2)^2
proof
let p be Point of TOP-REAL 2;
reconsider w=p as Element of REAL 2 by EUCLID:22;
A1: (sqr w).2=(p`2)^2 by VALUED_1:11;
0 <= Sum sqr w by RVSUM_1:86;
then
A2: |.p.|^2=Sum sqr w by SQUARE_1:def 2;
len sqr w =2 & (sqr w).1=(p`1)^2 by CARD_1:def 7,VALUED_1:11;
then sqr w=<*(p`1)^2,(p`2)^2*> by A1,FINSEQ_1:44;
hence thesis by A2,RVSUM_1:77;
end;
theorem Th30:
for p being Point of TOP-REAL 2 holds |.p.| = sqrt((p`1)^2+(p`2) ^2)
proof
let p be Point of TOP-REAL 2;
(|.p.|)^2= (p`1)^2+(p`2)^2 by Th29;
hence thesis by SQUARE_1:22;
end;
theorem Th31:
for p being Point of TOP-REAL 2 holds |.p.|<=|.p`1.|+|.p`2.|
proof
let p be Point of TOP-REAL 2;
(|.p.|)^2= (p`1)^2+(p`2)^2 by Th29;
then sqrt((p`1)^2+(p`2)^2)=|.p.| by SQUARE_1:22;
hence thesis by COMPLEX1:78;
end;
theorem Th32:
for p1,p2 being Point of TOP-REAL 2
holds |.p1-p2.|<=|.p1`1-p2`1.|+|.p1`2-p2`2.|
proof
let p1,p2 be Point of TOP-REAL 2;
p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:3;
hence thesis by Th31;
end;
theorem Th33:
for p being Point of TOP-REAL 2 holds |.p`1.|<=|.p.| & |.p`2.| <=|.p.|
proof
let p be Point of TOP-REAL 2;
|.p.| = sqrt((p`1)^2+(p`2)^2) by Th30;
hence thesis by COMPLEX1:79;
end;
theorem Th34:
for p1,p2 being Point of TOP-REAL 2 holds |.p1`1-p2`1.|<=|.p1-
p2.| & |.p1`2-p2`2.|<=|.p1-p2.|
proof
let p1,p2 be Point of TOP-REAL 2;
p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:3;
hence thesis by Th33;
end;
::$CT
theorem Th35:
p in LSeg(p1,p2) implies |.p-p1.|<=|.p1-p2.| & |.p-p2.|<=|.p1-p2 .|
proof
assume
A1: p in LSeg(p1,p2);
then consider r such that
A2: 0<=r and
A3: r<=1 and
A4: p=(1-r)*p1+r*p2 by RLTOPSP1:76;
A5: 0<=1-r by A3,XREAL_1:48;
p-p1= (1-r)*p1-p1+r*p2 by A4,RLVECT_1:def 3
.=(1-r)*p1-1*p1+r*p2 by RLVECT_1:def 8
.=(1+-r-1)*p1+r*p2 by RLVECT_1:35
.=r*p2+-r*p1 by RLVECT_1:79
.=r*p2+r*(-p1) by RLVECT_1:25
.=r*(p2-p1) by RLVECT_1:def 5;
then |.p-p1.|=|.r.|*|.p2-p1.| by TOPRNS_1:7
.=|.r.|*|.p1-p2.| by TOPRNS_1:27
.=r*|.p1-p2.| by A2,ABSVALUE:def 1;
then
A6: |.p1-p2.|- |.p-p1.|=(1-r)*|.p1-p2.|;
consider r such that
A7: 0<=r and
A8: r<=1 and
A9: p=(1-r)*p2+r*p1 by A1,RLTOPSP1:76;
p-p2= (1-r)*p2+-p2+r*p1 by A9,RLVECT_1:def 3
.=(1-r)*p2-1*p2+r*p1 by RLVECT_1:def 8
.=(1+-r-1)*p2+r*p1 by RLVECT_1:35
.=r*p1+-r*p2 by RLVECT_1:79
.=r*p1+r*(-p2) by RLVECT_1:25
.=r*(p1-p2) by RLVECT_1:def 5;
then |.p-p2.|=|.r.|*|.p1-p2.| by TOPRNS_1:7
.=r*|.p1-p2.| by A7,ABSVALUE:def 1;
then
A10: |.p1-p2.|- |.p-p2.|=(1-r)*|.p1-p2.|;
0<=1-r by A8,XREAL_1:48;
hence thesis by A6,A5,A10,XREAL_1:49;
end;
begin :: EXTENDED GOBOARD THEOREM AND FASHODA MEET THEOREM
reserve M for non empty MetrSpace;
theorem Th36:
for P,Q being Subset of TopSpaceMetr(M) st P <> {} & P is
compact & Q <> {} & Q is compact holds min_dist_min(P,Q)>=0
proof
let P,Q be Subset of TopSpaceMetr(M);
assume P <> {} & P is compact & Q <> {} & Q is compact;
then ex x1,x2 being Point of M st x1 in P & x2 in Q & dist( x1,x2) =
min_dist_min(P,Q) by WEIERSTR:30;
hence thesis by METRIC_1:5;
end;
theorem Th37:
for P,Q being Subset of TopSpaceMetr(M) st P <> {} & P is
compact & Q <> {} & Q is compact holds P misses Q iff min_dist_min(P,Q)>0
proof
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} and
A2: P is compact and
A3: Q <> {} and
A4: Q is compact;
A5: now
set p = the Element of P /\ Q;
assume
A6: P /\ Q <>{};
then
A7: p in P by XBOOLE_0:def 4;
then reconsider p9=p as Element of TopSpaceMetr(M);
reconsider q=p9 as Point of M by TOPMETR:12;
the distance of M is Reflexive by METRIC_1:def 6;
then (the distance of M).(q,q)=0 by METRIC_1:def 2;
then
A8: dist(q,q)=0 by METRIC_1:def 1;
p in Q by A6,XBOOLE_0:def 4;
hence not min_dist_min(P,Q)>0 by A2,A4,A7,A8,WEIERSTR:34;
end;
consider x1,x2 being Point of M such that
A9: x1 in P & x2 in Q and
A10: dist(x1,x2) = min_dist_min(P,Q) by A1,A2,A3,A4,WEIERSTR:30;
A11: the distance of M is discerning by METRIC_1:def 7;
now
assume not min_dist_min(P,Q)>0;
then dist(x1,x2)=0 by A1,A2,A3,A4,A10,Th36;
then (the distance of M).(x1,x2)=0 by METRIC_1:def 1;
then x1=x2 by A11,METRIC_1:def 3;
hence P /\ Q <> {} by A9,XBOOLE_0:def 4;
end;
hence thesis by A5;
end;
:: Approximation of finite sequence by special finite sequence
theorem Th38:
for f being FinSequence of TOP-REAL 2,
a,c,d being Real st 1<=len
f & X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) & Y_axis(f)
lies_between c, d & a>0 & (for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|
<a) holds ex g being FinSequence of TOP-REAL 2 st g is special & g.1=f.1 & g.
len g=f.len f & len g>=len f & X_axis(g) lies_between (X_axis(f)).1, (X_axis(f)
).(len f) & Y_axis(g) lies_between c, d & (for j st j in dom g holds ex k st k
in dom f & |. g/.j - f/.k .|<a)& for j st 1<=j & j+1<=len g holds |. g/.j - g/.
(j+1) .|<a
proof
let f be FinSequence of TOP-REAL 2,a,c,d be Real;
assume that
A1: 1<=len f and
A2: X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) and
A3: Y_axis(f) lies_between c, d and
A4: a>0 and
A5: for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a;
A6: f.len f=f/.len f by A1,FINSEQ_4:15;
defpred P[set,object] means
for j st $1=2*j or $1=2*j -'1 holds ($1 =2*j
implies $2=|[(f/.j)`1,(f/.(j+1))`2]|) &($1 =2*j-'1 implies $2=f/.j);
A7: for k be Nat st k in Seg (2*(len f)-'1) ex x being object st P[k,x]
proof
let k be Nat;
assume
A8: k in Seg (2*(len f)-'1);
then
A9: 1<=k by FINSEQ_1:1;
per cases by NAT_D:12;
suppose
A10: k mod 2=0;
consider i being Nat such that
A11: k=2*i+ (k mod 2) and
k mod 2<2 by NAT_D:def 2;
for j st k=2*j or k=2*j -'1 holds (k =2*j implies |[(f/.i)`1,(f/.(i
+1))`2]| =|[(f/.j)`1,(f/.(j+1))`2]|) &(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))
`2]|=f/.j)
proof
let j;
assume k=2*j or k=2*j -'1;
now
assume
A12: k=2*j-'1;
now
0 qua Nat-1<0;
then
A13: 0-'1=0 by XREAL_0:def 2;
assume j=0;
hence contradiction by A8,A12,A13,FINSEQ_1:1;
end;
then
A14: j>=0 qua Nat+1 by NAT_1:13;
k=2*(j-1)+(1+1)-1 by A9,A12,NAT_D:39
.=2*(j-1)+1;
then k= 2*(j-'1)+1 by A14,XREAL_1:233;
hence contradiction by A10,NAT_D:def 2;
end;
hence thesis by A10,A11;
end;
hence thesis;
end;
suppose
A15: k mod 2=1;
consider i being Nat such that
A16: k=2*i+ (k mod 2) and
A17: k mod 2<2 by NAT_D:def 2;
for j st k=2*j or k=2*j -'1 holds (k =2*j implies f/.(i+1)=|[(f/.j)
`1,(f/.(j+1))`2]|) &(k =2*j-'1 implies f/.(i+1)=f/.j)
proof
let j;
assume
A18: k=2*j or k=2*j -'1;
per cases by A18;
suppose
A19: k=2*j-'1;
A20: now
assume k=2*j-'1;
then k=2*(j-1)+(1+1)-1 by A9,NAT_D:39
.=2*(j-1)+1;
hence f/.(i+1)=f/.j by A15,A16;
end;
k=2*j-1 by A9,A19,NAT_D:39;
hence thesis by A20;
end;
suppose
A21: k=2*j;
then
A22: 2*(j-i)=1 by A15,A16;
then j-i>=0;
then
A23: j-i=j-'i by XREAL_0:def 2;
j-i=0 or j-i>0 by A22;
then j-i>=0 qua Nat+1 by A15,A16,A21,A23,NAT_1:13;
then 2*(j-i)>=2*1 by XREAL_1:64;
hence thesis by A16,A17,A21;
end;
end;
hence thesis;
end;
end;
ex p being FinSequence st dom p = Seg (2*(len f)-'1) & for k be Nat st
k in Seg (2*(len f)-'1) holds P[k,p.k] from FINSEQ_1:sch 1(A7);
then consider p being FinSequence such that
A24: dom p = Seg (2*(len f)-'1) and
A25: for k be Nat st k in Seg (2*(len f)-'1) holds for j st k=2*j or k=
2*j -'1 holds (k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|) &(k =2*j-'1
implies p.k=f/.j);
rng p c= the carrier of TOP-REAL 2
proof
let y be object;
assume y in rng p;
then consider x being object such that
A26: x in dom p and
A27: y=p.x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A26;
x in Seg len p by A26,FINSEQ_1:def 3;
then
A28: 1 <= i by FINSEQ_1:1;
per cases by NAT_D:12;
suppose
A29: i mod 2=0;
consider j being Nat such that
A30: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A24,A25,A26,A29,A30;
hence thesis by A27;
end;
suppose
A31: i mod 2=1;
consider j being Nat such that
A32: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A28,A31,A32,NAT_D:39;
then p.i=f/.(j+1) by A24,A25,A26,A31,A32;
hence thesis by A27;
end;
end;
then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A33: len p=(2*(len f)-'1) by A24,FINSEQ_1:def 3;
for i be Nat st 1 <= i & i+1 <= len g1 holds (g1/.i)`1 = (g1/.(i+1))`1
or (g1/.i)`2 = (g1/.(i+1))`2
proof
let i be Nat;
assume that
A34: 1 <= i and
A35: i+1 <= len g1;
A36: i<len g1 by A35,NAT_1:13;
then
A37: g1.i=g1/.i by A34,FINSEQ_4:15;
A38: 1<i+1 by A34,NAT_1:13;
then
A39: i+1 in Seg len g1 by A35,FINSEQ_1:1;
A40: i in Seg (2*(len f)-'1) by A33,A34,A36,FINSEQ_1:1;
A41: g1.(i+1)=g1/.(i+1) by A35,A38,FINSEQ_4:15;
per cases by NAT_D:12;
suppose
A42: i mod 2=0;
consider j being Nat such that
A43: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
1<=1+i by NAT_1:11;
then 2*(j+1)-'1 =2*(j+1)-1 by A42,A43,NAT_D:39;
then
A44: g1.(i+1)=f/.(j+1) by A25,A33,A39,A42,A43;
g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A40,A42,A43;
hence thesis by A37,A41,A44;
end;
suppose
A45: i mod 2=1;
consider j being Nat such that
A46: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
i+1=2*(j+1) by A45,A46;
then
A47: g1.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A25,A33,A39;
2*(j+1)-'1 =2*(j+1)-1 by A34,A45,A46,NAT_D:39;
then g1.i=f/.(j+1) by A25,A40,A45,A46;
hence thesis by A37,A41,A47;
end;
end;
then
A48: g1 is special by TOPREAL1:def 5;
A49: 2*(len f)>=2*1 by A1,XREAL_1:64;
then
A50: 2*(len f)-'1= 2*(len f)-1 by XREAL_1:233,XXREAL_0:2;
for i st i in dom (Y_axis(g1)) holds c <= (Y_axis(g1)).i & (Y_axis(g1)
).i <= d
proof
let i;
A51: len (Y_axis(f))=len f by GOBOARD1:def 2;
assume
A52: i in dom (Y_axis(g1));
then
A53: i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
then
A54: i in Seg len g1 by GOBOARD1:def 2;
i in Seg len g1 by A53,GOBOARD1:def 2;
then
A55: i<=len g1 by FINSEQ_1:1;
A56: 1<=i by A53,FINSEQ_1:1;
then
A57: g1/.i=(g1.i) by A55,FINSEQ_4:15;
A58: (Y_axis(g1)).i = (g1/.i)`2 by A52,GOBOARD1:def 2;
per cases by NAT_D:12;
suppose
A59: i mod 2=0;
consider j being Nat such that
A60: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A33,A54,A59,A60;
then
A61: (g1/.i)`2=(f/.(j+1))`2 by A57;
2*j+1<=2*(len f)-1+1 by A33,A50,A55,A59,A60,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A62: j+1 in dom (Y_axis(f)) by A51,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 2;
hence thesis by A3,A58,A61,A62,GOBOARD4:def 2;
end;
suppose
A63: i mod 2=1;
consider j being Nat such that
A64: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A56,A63,A64,NAT_D:39;
then
A65: (g1/.i)`2=(f/.(j+1))`2 by A25,A33,A54,A57,A63,A64;
2*j+1<=2*(len f)-1+1 by A33,A50,A55,A63,A64,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A66: j+1 in dom (Y_axis(f)) by A51,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 2;
hence thesis by A3,A58,A65,A66,GOBOARD4:def 2;
end;
end;
then
A67: Y_axis(g1) lies_between c, d by GOBOARD4:def 2;
for i st i in dom (X_axis(g1)) holds (X_axis(f)).1 <= (X_axis(g1)).i &
(X_axis(g1)).i <= (X_axis(f)).(len f)
proof
let i;
A68: len (X_axis(f))=len f by GOBOARD1:def 1;
assume
A69: i in dom (X_axis(g1));
then
A70: i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
then
A71: i in Seg len g1 by GOBOARD1:def 1;
i in Seg len g1 by A70,GOBOARD1:def 1;
then
A72: i<=len g1 by FINSEQ_1:1;
A73: 1<=i by A70,FINSEQ_1:1;
then
A74: g1/.i=(g1.i) by A72,FINSEQ_4:15;
A75: (X_axis(g1)).i = (g1/.i)`1 by A69,GOBOARD1:def 1;
per cases by NAT_D:12;
suppose
A76: i mod 2=0;
consider j being Nat such that
A77: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A33,A71,A76,A77;
then
A78: (g1/.i)`1=(f/.j)`1 by A74;
2*j+1<=2*(len f)-1+1 by A33,A50,A72,A76,A77,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then
A79: 2*j/2<2*(len f)/2 by XREAL_1:74;
j>0 by A70,A76,A77,FINSEQ_1:1;
then j>=0 qua Nat+1 by NAT_1:13;
then j in Seg len f by A79,FINSEQ_1:1;
then
A80: j in dom (X_axis(f)) by A68,FINSEQ_1:def 3;
then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 1;
hence thesis by A2,A75,A78,A80,GOBOARD4:def 2;
end;
suppose
A81: i mod 2=1;
consider j being Nat such that
A82: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A73,A81,A82,NAT_D:39;
then
A83: (g1/.i)`1=(f/.(j+1))`1 by A25,A33,A71,A74,A81,A82;
2*j+1<=2*(len f)-1+1 by A33,A50,A72,A81,A82,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A84: j+1 in dom (X_axis(f)) by A68,FINSEQ_1:def 3;
then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 1;
hence thesis by A2,A75,A83,A84,GOBOARD4:def 2;
end;
end;
then
A85: X_axis(g1) lies_between (X_axis(f)).1, (X_axis(f)).(len f) by
GOBOARD4:def 2;
len f + len f>=len f+1 by A1,XREAL_1:6;
then
A86: 2*(len f)-1>=len f +1-1 by XREAL_1:9;
A87: 2*1-'1=1+1-'1 .=1 by NAT_D:34;
A88: 2*(len f)-1>= 1+1-1 by A49,XREAL_1:9;
then 1 in Seg (2*(len f)-'1) by A50,FINSEQ_1:1;
then
A89: p.1=f/.1 by A25,A87;
A90: for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
proof
let i;
assume that
A91: 1<=i and
A92: i+1<=len g1;
A93: g1.(i+1)=g1/.(i+1) by A92,FINSEQ_4:15,NAT_1:11;
i<=len g1 by A92,NAT_1:13;
then
A94: i in Seg len g1 by A91,FINSEQ_1:1;
i<=len g1 by A92,NAT_1:13;
then
A95: g1.i=g1/.i by A91,FINSEQ_4:15;
1<=i+1 by NAT_1:11;
then
A96: i+1 in Seg (2*(len f)-'1) by A33,A92,FINSEQ_1:1;
per cases by NAT_D:12;
suppose
A97: i mod 2=0;
consider j being Nat such that
A98: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
A99: g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A33,A94,A97,A98;
1<=1+i by NAT_1:11;
then 2*(j+1)-'1 =2*(j+1)-1 by A97,A98,NAT_D:39;
then g1.(i+1)=f/.(j+1) by A25,A96,A97,A98;
then
A101: (g1/.(i+1))`1=(f/.(j+1))`1 & (g1/.(i+1))`2=(f/.(j+1))`2 by A92,
FINSEQ_4:15,NAT_1:11;
A102: g1/.i-g1/.(i+1) =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2
]| by EUCLID:61
.=|[(f/.j)`1-(f/.(j+1))`1,0]| by A95,A99,A101;
2*j+1<=2*(len f)-1+1 by A33,A50,A92,A97,A98,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then
A104: j+1<=len f by NAT_1:13;
|.g1/.i-g1/.(i+1).|= sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i-g1/.(
i+1))`2))^2) by Th30
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0^2) by A102
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
then |.g1/.i-g1/.(i+1).|=|.(f/.j)`1-(f/.(j+1))`1.| by COMPLEX1:72;
then
A105: |.g1/.i-g1/.(i+1).| <=|.f/.j-f/.(j+1).| by Th34;
j>0 by A91,A97,A98;
then j>=0 qua Nat+1 by NAT_1:13;
then |. f/.j-f/.(j+1) .|<a by A5,A104;
hence thesis by A105,XXREAL_0:2;
end;
suppose
A106: i mod 2=1;
consider j being Nat such that
A107: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A91,A106,A107,NAT_D:39;
then
A108: (g1/.i)`1=(f/.(j+1))`1 & (g1/.i)`2=(f/.(j+1))`2 by A25,A33,A94,A95,A106
,A107;
i+1=2*(j+1) by A106,A107;
then
A109: g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A25,A96,A93;
A111: g1/.i-g1/.(i+1) =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2
]| by EUCLID:61
.=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]| by A109,A108;
2*(j+1)+1<=2*(len f)-1+1 by A33,A50,A92,A106,A107,XREAL_1:6;
then 2*(j+1)<2*(len f) by NAT_1:13;
then 2*(j+1)/2<2*(len f)/2 by XREAL_1:74;
then (j+1)+1<=len f by NAT_1:13;
then
A113: |. f/.(j+1)-f/.(j+1+1) .|<a by A5,NAT_1:11;
|.g1/.i-g1/.(i+1).|= sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i- g1/.
(i+1))`2))^2) by Th30
.= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2) by A111;
then |.g1/.i-g1/.(i+1).|=|.(f/.(j+1))`2-(f/.(j+1+1))`2.| by COMPLEX1:72;
then |.g1/.i-g1/.(i+1).| <=|.f/.(j+1)-f/.(j+1+1).| by Th34;
hence thesis by A113,XXREAL_0:2;
end;
end;
A114: for i st i in dom g1 holds ex k st k in dom f & |. g1/.i - f/.k .| < a
proof
let i;
assume
A115: i in dom g1;
then
A116: i in Seg len g1 by FINSEQ_1:def 3;
then
A117: i<=len g1 by FINSEQ_1:1;
A118: 1<=i by A116,FINSEQ_1:1;
then
A119: g1.i=g1/.i by A117,FINSEQ_4:15;
per cases by NAT_D:12;
suppose
A120: i mod 2=0;
consider j being Nat such that
A121: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
j>0 by A116,A120,A121,FINSEQ_1:1;
then
A122: j>=0 qua Nat+1 by NAT_1:13;
A123: g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A24,A25,A115,A120,A121;
then
A124: (g1/.i)`1=(f/.j)`1 by A119;
A125: (g1/.i)`2=(f/.(j+1))`2 by A119,A123;
A126: g1/.i-f/.j=|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-( (f/.j))`2]| by EUCLID:61
.=|[0,(g1/.i)`2-(f/.j)`2]| by A124;
then (g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2;
then |.g1/.i-f/.j.|= sqrt(((g1/.i-f/.j)`1)^2+((g1/.i)`2-(f/.j)`2)^2) by
Th30
.= sqrt(0^2+(((f/.(j+1))`2-(f/.j)`2))^2) by A125,A126
.= sqrt((((f/.(j+1))`2-(f/.j)`2))^2);
then |.g1/.i-f/.j.|=|.(f/.(j+1))`2-(f/.j)`2.| by COMPLEX1:72
.=|.(f/.j)`2 -(f/.(j+1))`2.| by UNIFORM1:11;
then
A127: |.g1/.i-f/.j.| <=|.f/.j-f/.(j+1).| by Th34;
2*j+1<=2*(len f)-1+1 by A33,A50,A117,A120,A121,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then
A128: 2*j/2<2*(len f)/2 by XREAL_1:74;
then j+1<=len f by NAT_1:13;
then |. f/.j-f/.(j+1) .|<a by A5,A122;
then
A129: |. g1/.i - f/.j .|<a by A127,XXREAL_0:2;
j in dom f by A122,A128,FINSEQ_3:25;
hence thesis by A129;
end;
suppose
A130: i mod 2=1;
consider j being Nat such that
A131: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A118,A130,A131,NAT_D:39;
then g1.i=f/.(j+1) by A24,A25,A115,A130,A131;
then
A132: |.g1/.i-f/.(j+1).|=|.0.TOP-REAL 2.| by A119,RLVECT_1:5
.=0 by TOPRNS_1:23;
2*j+1+1<=2*(len f)-1+1 by A33,A50,A117,A130,A131,XREAL_1:6;
then 2*j+1<2*(len f) by NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then
A133: j+1<=len f by NAT_1:13;
1<=j+1 by NAT_1:11;
then j+1 in dom f by A133,FINSEQ_3:25;
hence thesis by A4,A132;
end;
end;
(2*(len f)-'1) in Seg (2*(len f)-'1) by A50,A88,FINSEQ_1:1;
then g1.len g1=f.len f by A25,A33,A6;
hence thesis by A1,A33,A48,A50,A89,A86,A85,A67,A114,A90,FINSEQ_4:15;
end;
theorem Th39:
for f being FinSequence of TOP-REAL 2,a,c,d being Real
st 1<=len
f & Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) & X_axis(f)
lies_between c, d & a>0 & (for i st 1<=i & i+1<=len f holds |. (f/.i)-(f/.(i+1)
) .|<a) holds ex g being FinSequence of TOP-REAL 2 st g is special & g.1=f.1 &
g.len g=f.len f & len g>=len f & Y_axis(g) lies_between (Y_axis(f)).1, (Y_axis(
f)).(len f) & X_axis(g) lies_between c, d & (for j st j in dom g holds ex k st
k in dom f & |. g/.j - f/.k .| < a)& for j st 1<=j & j+1<=len g holds |. g/.j -
g/.(j+1) .|<a
proof
A1: 2*1-'1=1+1-'1 .=1 by NAT_D:34;
let f be FinSequence of TOP-REAL 2,a,c,d be Real;
assume that
A2: 1<=len f and
A3: Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) and
A4: X_axis(f) lies_between c, d and
A5: a>0 and
A6: for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a;
len f + len f>=len f+1 by A2,XREAL_1:6;
then
A7: 2*(len f)-1>=len f +1-1 by XREAL_1:9;
defpred P[set,object] means for j st $1=2*j or $1=2*j -'1 holds ($1 =2*j
implies $2=|[(f/.j)`1,(f/.(j+1))`2]|) &($1 =2*j-'1 implies $2=f/.j);
A8: for k be Nat st k in Seg (2*(len f)-'1) ex x being object st P[k,x]
proof
let k be Nat;
assume
A9: k in Seg (2*(len f)-'1);
then
A10: 1<=k by FINSEQ_1:1;
per cases by NAT_D:12;
suppose
A11: k mod 2=0;
consider i being Nat such that
A12: k=2*i+ (k mod 2) and
k mod 2<2 by NAT_D:def 2;
for j st k=2*j or k=2*j -'1 holds (k =2*j implies |[(f/.i)`1,(f/.(i
+1))`2]| =|[(f/.j)`1,(f/.(j+1))`2]|) &(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))
`2]|=f/.j)
proof
let j;
assume k=2*j or k=2*j -'1;
now
assume
A13: k=2*j-'1;
now
0 qua Nat-1<0;
then
A14: 0-'1=0 by XREAL_0:def 2;
assume j=0;
hence contradiction by A9,A13,A14,FINSEQ_1:1;
end;
then
A15: j>=0 qua Nat+1 by NAT_1:13;
k=2*(j-1)+(1+1)-1 by A10,A13,NAT_D:39
.=2*(j-1)+1;
then k= 2*(j-'1)+1 by A15,XREAL_1:233;
hence contradiction by A11,NAT_D:def 2;
end;
hence thesis by A11,A12;
end;
hence thesis;
end;
suppose
A16: k mod 2=1;
consider i being Nat such that
A17: k=2*i+ (k mod 2) and
A18: k mod 2<2 by NAT_D:def 2;
for j st k=2*j or k=2*j -'1 holds (k =2*j implies f/.(i+1)=|[(f/.j)
`1,(f/.(j+1))`2]|) &(k =2*j-'1 implies f/.(i+1)=f/.j)
proof
let j;
assume
A19: k=2*j or k=2*j -'1;
per cases by A19;
suppose
A20: k=2*j-'1;
A21: now
assume k=2*j-'1;
then k=2*(j-1)+(1+1)-1 by A10,NAT_D:39
.=2*(j-1)+1;
hence f/.(i+1)=f/.j by A16,A17;
end;
k=2*j-1 by A10,A20,NAT_D:39;
hence thesis by A21;
end;
suppose
A22: k=2*j;
then
A23: 2*(j-i)=1 by A16,A17;
then j-i>=0;
then
A24: j-i=j-'i by XREAL_0:def 2;
j-i=0 or j-i>0 by A23;
then j-i>=0 qua Nat+1 by A16,A17,A22,A24,NAT_1:13;
then 2*(j-i)>=2*1 by XREAL_1:64;
hence thesis by A17,A18,A22;
end;
end;
hence thesis;
end;
end;
ex p being FinSequence st dom p = Seg (2*(len f)-'1) & for k be Nat st
k in Seg (2*(len f)-'1) holds P[k,p.k] from FINSEQ_1:sch 1(A8);
then consider p being FinSequence such that
A25: dom p = Seg (2*(len f)-'1) and
A26: for k be Nat st k in Seg (2*(len f)-'1) holds for j st k=2*j or k=
2*j -'1 holds (k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|) &(k =2*j-'1
implies p.k=f/.j);
rng p c= the carrier of TOP-REAL 2
proof
let y be object;
assume y in rng p;
then consider x being object such that
A27: x in dom p and
A28: y=p.x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A27;
x in Seg len p by A27,FINSEQ_1:def 3;
then
A29: 1 <= i by FINSEQ_1:1;
per cases by NAT_D:12;
suppose
A30: i mod 2=0;
consider j being Nat such that
A31: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A26,A27,A30,A31;
hence thesis by A28;
end;
suppose
A32: i mod 2=1;
consider j being Nat such that
A33: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-1=2*(j+1)-'1 by A29,A32,A33,NAT_D:39;
then p.i=f/.(j+1) by A25,A26,A27,A32,A33;
hence thesis by A28;
end;
end;
then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A34: len p=(2*(len f)-'1) by A25,FINSEQ_1:def 3;
for i be Nat st 1 <= i & i+1 <= len g1 holds (g1/.i)`1 = (g1/.(i+1))`1
or (g1/.i)`2 = (g1/.(i+1))`2
proof
let i be Nat;
assume that
A35: 1 <= i and
A36: i+1 <= len g1;
1<i+1 by A35,NAT_1:13;
then
A37: i+1 in Seg len g1 & g1/.(i+1)=g1.(i+1) by A36,FINSEQ_1:1,FINSEQ_4:15;
i<len g1 by A36,NAT_1:13;
then
A38: i in Seg (2*(len f)-'1) & g1.i=g1/.i by A34,A35,FINSEQ_1:1,FINSEQ_4:15;
per cases by NAT_D:12;
suppose
A39: i mod 2=0;
consider j being Nat such that
A40: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
1<=1+i by NAT_1:11;
then 2*(j+1)-'1 =2*(j+1)-1 by A39,A40,NAT_D:39;
then
A41: g1/.(i+1)=f/.(j+1) by A26,A34,A37,A39,A40;
g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A26,A38,A39,A40;
hence thesis by A41;
end;
suppose
A42: i mod 2=1;
consider j being Nat such that
A43: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
i+1=2*(j+1) by A42,A43;
then
A44: g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A26,A34,A37;
2*(j+1)-'1 =2*(j+1)-1 by A35,A42,A43,NAT_D:39;
then g1/.i=f/.(j+1) by A26,A38,A42,A43;
hence thesis by A44;
end;
end;
then
A45: g1 is special by TOPREAL1:def 5;
A46: 2*(len f)>=2*1 by A2,XREAL_1:64;
then
A47: 2*(len f)-'1= 2*(len f)-1 by XREAL_1:233,XXREAL_0:2;
for i st i in dom (Y_axis(g1)) holds (Y_axis(f)).1 <= (Y_axis(g1)).i &
(Y_axis(g1)).i <= (Y_axis(f)).(len f)
proof
let i;
A48: len (Y_axis(f))=len f by GOBOARD1:def 2;
assume
A49: i in dom (Y_axis(g1));
then
A50: i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
then
A51: i in Seg len g1 by GOBOARD1:def 2;
i in Seg len g1 by A50,GOBOARD1:def 2;
then
A52: i<=len g1 by FINSEQ_1:1;
A53: 1<=i by A50,FINSEQ_1:1;
then
A54: g1/.i=(g1.i) by A52,FINSEQ_4:15;
A55: (Y_axis(g1)).i = (g1/.i)`2 by A49,GOBOARD1:def 2;
per cases by NAT_D:12;
suppose
A56: i mod 2=0;
consider j being Nat such that
A57: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A26,A34,A51,A54,A56,A57;
then
A58: (g1/.i)`2=(f/.(j+1))`2;
2*j+1<=2*(len f)-1+1 by A34,A47,A52,A56,A57,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A59: j+1 in dom (Y_axis(f)) by A48,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 2;
hence thesis by A3,A55,A58,A59,GOBOARD4:def 2;
end;
suppose
A60: i mod 2=1;
consider j being Nat such that
A61: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A53,A60,A61,NAT_D:39;
then
A62: (g1/.i)`2=(f/.(j+1))`2 by A26,A34,A51,A54,A60,A61;
2*j+1<=2*(len f)-1+1 by A34,A47,A52,A60,A61,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A63: j+1 in dom (Y_axis(f)) by A48,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 2;
hence thesis by A3,A55,A62,A63,GOBOARD4:def 2;
end;
end;
then
A64: Y_axis(g1) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) by
GOBOARD4:def 2;
A65: 2*(len f)-1>= 1+1-1 by A46,XREAL_1:9;
then 1 in Seg (2*(len f)-'1) by A47,FINSEQ_1:1;
then p.1=f/.1 by A26,A1;
then
A66: g1.1=f.1 by A2,FINSEQ_4:15;
A67: for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
proof
let i;
assume that
A68: 1<=i and
A69: i+1<=len g1;
A70: g1.(i+1)=g1/.(i+1) by A69,FINSEQ_4:15,NAT_1:11;
i<=len g1 by A69,NAT_1:13;
then
A71: i in Seg len g1 by A68,FINSEQ_1:1;
1<=i+1 by NAT_1:11;
then
A72: i+1 in Seg (2*(len f)-'1) by A34,A69,FINSEQ_1:1;
i<=len g1 by A69,NAT_1:13;
then
A73: g1.i=g1/.i by A68,FINSEQ_4:15;
per cases by NAT_D:12;
suppose
A74: i mod 2=0;
consider j being Nat such that
A75: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
A76: g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A26,A34,A71,A73,A74,A75;
1<=1+i by NAT_1:11;
then 2*(j+1)-'1 =2*(j+1)-1 by A74,A75,NAT_D:39;
then
A78: g1/.(i+1)=f/.(j+1) by A26,A72,A70,A74,A75;
g1/.i-g1/.(i+1) =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2
]| by EUCLID:61
.=|[(f/.j)`1-(f/.(j+1))`1,0]| by A76,A78;
then (g1/.i-g1/.(i+1))`1=(f/.j)`1-(f/.(j+1))`1 & (g1/.i-g1/.(i+1))`2=0;
then |.g1/.i-g1/.(i+1).|= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0^2) by Th30
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
then |.g1/.i-g1/.(i+1).|=|.(f/.j)`1-(f/.(j+1))`1.| by COMPLEX1:72;
then
A79: |.g1/.i-g1/.(i+1).|<=|.f/.j-f/.(j+1).| by Th34;
2*j+1<=2*(len f)-1+1 by A34,A47,A69,A74,A75,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then
A80: j+1<=len f by NAT_1:13;
j>0 by A68,A74,A75;
then j>=0 qua Nat+1 by NAT_1:13;
then |. f/.j-f/.(j+1) .|<a by A6,A80;
hence thesis by A79,XXREAL_0:2;
end;
suppose
A81: i mod 2=1;
consider j being Nat such that
A82: i=2*j+ (i mod 2) and
i mod 2<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A68,A81,A82,NAT_D:39;
then
A83: g1/.i=f/.(j+1) by A26,A34,A71,A73,A81,A82;
i+1=2*(j+1) by A81,A82;
then
A84: g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A26,A72,A70;
g1/.i-g1/.(i+1) =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2
]| by EUCLID:61
.=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]| by A83,A84;
then (g1/.i-g1/.(i+1))`1=0 & (g1/.i-g1/.(i+1))`2=(f/.(j+1))`2-(f/.(j+1+
1))`2;
then |.g1/.i-g1/.(i+1).|= sqrt(0^2+(((f/.(j+1))`2-(f/.(j+1+1))`2))^2)
by Th30
.= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2);
then |.g1/.i-g1/.(i+1).|=|.(f/.(j+1))`2-(f/.(j+1+1))`2.| by COMPLEX1:72;
then
A86: |.g1/.i-g1/.(i+1).| <=|.f/.(j+1)-f/.(j+1+1).| by Th34;
2*(j+1)+1<=2*(len f)-1+1 by A34,A47,A69,A81,A82,XREAL_1:6;
then 2*(j+1)<2*(len f) by NAT_1:13;
then 2*(j+1)/2<2*(len f)/2 by XREAL_1:74;
then (j+1)+1<=len f by NAT_1:13;
then |. f/.(j+1)-f/.(j+1+1) .|<a by A6,NAT_1:11;
hence thesis by A86,XXREAL_0:2;
end;
end;
A87: for i st i in dom g1 holds ex k st k in dom f & |. g1/.i - f/.k .| < a
proof
let i;
assume
A88: i in dom g1;
then
A89: i<=len g1 by FINSEQ_3:25;
A90: 1<=i by A88,FINSEQ_3:25;
then
A91: g1.i=g1/.i by A89,FINSEQ_4:15;
per cases by NAT_D:12;
suppose
A92: i mod 2=0;
consider j being Nat such that
A93: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
j>0 by A88,A92,A93,FINSEQ_3:25;
then
A94: j>=0 qua Nat+1 by NAT_1:13;
A95: g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A25,A26,A88,A91,A92,A93;
then
A96: (g1/.i)`1=(f/.j)`1;
A97: g1/.i-f/.j =|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-(f/.j)`2]| by EUCLID:61
.=|[0,(g1/.i)`2-(f/.j)`2]| by A96;
then
A98: (g1/.i-f/.j)`1=0;
(g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by A97;
then |.g1/.i-f/.j.|= sqrt((((g1/.i-f/.j)`1))^2+(((g1/.i)`2-(f/.j)`2))^2
) by Th30
.= sqrt((((f/.(j+1))`2-(f/.j)`2))^2) by A95,A98;
then |.g1/.i-f/.j.|=|.(f/.(j+1))`2-(f/.j)`2.| by COMPLEX1:72
.=|.(f/.j)`2 -(f/.(j+1))`2.| by UNIFORM1:11;
then
A99: |.g1/.i-f/.j.| <=|.f/.j-f/.(j+1).| by Th34;
2*j+1<=2*(len f)-1+1 by A34,A47,A89,A92,A93,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then
A100: 2*j/2<2*(len f)/2 by XREAL_1:74;
then j+1<=len f by NAT_1:13;
then |. f/.j-f/.(j+1) .|<a by A6,A94;
then
A101: |. g1/.i - f/.j .|<a by A99,XXREAL_0:2;
j in dom f by A94,A100,FINSEQ_3:25;
hence thesis by A101;
end;
suppose
A102: i mod 2=1;
consider j being Nat such that
A103: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A90,A102,A103,NAT_D:39;
then g1/.i=f/.(j+1) by A25,A26,A88,A91,A102,A103;
then
A104: |.g1/.i-f/.(j+1).|=|.0.TOP-REAL 2.| by RLVECT_1:5
.=0 by TOPRNS_1:23;
2*j+1+1<=2*(len f)-1+1 by A34,A47,A89,A102,A103,XREAL_1:6;
then 2*j+1<2*(len f) by NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then
A105: j+1<=len f by NAT_1:13;
1<=j+1 by NAT_1:11;
then j+1 in dom f by A105,FINSEQ_3:25;
hence thesis by A5,A104;
end;
end;
for i st i in dom (X_axis(g1)) holds c <= (X_axis(g1)).i & (X_axis(g1)
).i <= d
proof
let i;
A106: len (X_axis(f))=len f by GOBOARD1:def 1;
assume
A107: i in dom (X_axis(g1));
then
A108: i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
then
A109: i in Seg len g1 by GOBOARD1:def 1;
then
A110: i<=len g1 by FINSEQ_1:1;
A111: 1<=i by A108,FINSEQ_1:1;
then
A112: g1/.i=(g1.i) by A110,FINSEQ_4:15;
A113: (X_axis(g1)).i = (g1/.i)`1 by A107,GOBOARD1:def 1;
per cases by NAT_D:12;
suppose
A114: i mod 2=0;
consider j being Nat such that
A115: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A26,A34,A109,A112,A114,A115;
then
A116: (g1/.i)`1=(f/.j)`1;
2*j+1<=2*(len f)-1+1 by A34,A47,A110,A114,A115,XREAL_1:6;
then 2*j<2*(len f) by NAT_1:13;
then
A117: 2*j/2<2*(len f)/2 by XREAL_1:74;
j>0 by A108,A114,A115,FINSEQ_1:1;
then j>=0 qua Nat+1 by NAT_1:13;
then j in Seg len f by A117,FINSEQ_1:1;
then
A118: j in dom (X_axis(f)) by A106,FINSEQ_1:def 3;
then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 1;
hence thesis by A4,A113,A116,A118,GOBOARD4:def 2;
end;
suppose
A119: i mod 2=1;
consider j being Nat such that
A120: i=2*j+ (i mod 2) and
(i mod 2)<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
2*(j+1)-'1 =2*(j+1)-1 by A111,A119,A120,NAT_D:39;
then
A121: (g1/.i)`1=(f/.(j+1))`1 by A26,A34,A109,A112,A119,A120;
2*j+1<=2*(len f)-1+1 by A34,A47,A110,A119,A120,NAT_1:13;
then 2*j<2*(len f) by NAT_1:13;
then 2*j/2<2*(len f)/2 by XREAL_1:74;
then 1<=j+1 & j+1<=len f by NAT_1:11,13;
then j+1 in Seg len f by FINSEQ_1:1;
then
A122: j+1 in dom (X_axis(f)) by A106,FINSEQ_1:def 3;
then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 1;
hence thesis by A4,A113,A121,A122,GOBOARD4:def 2;
end;
end;
then
A123: X_axis(g1) lies_between c, d by GOBOARD4:def 2;
(2*(len f)-'1) in Seg (2*(len f)-'1) by A47,A65,FINSEQ_1:1;
then p.(2*(len f)-'1)=f/.len f by A26;
hence thesis by A2,A34,A45,A47,A66,A7,A64,A123,A87,A67,FINSEQ_4:15;
end;
theorem Th40:
for f being FinSequence of TOP-REAL 2 st 1 <=len f holds len
X_axis(f)=len f & X_axis(f).1=(f/.1)`1 & X_axis(f).len f=(f/.len f)`1
proof
let f be FinSequence of TOP-REAL 2;
A1: len (X_axis(f)) = len f by GOBOARD1:def 1;
assume
A2: 1 <=len f;
then len f in Seg len f by FINSEQ_1:1;
then
A3: len f in dom (X_axis(f)) by A1,FINSEQ_1:def 3;
1 in Seg len f by A2,FINSEQ_1:1;
then 1 in dom (X_axis(f)) by A1,FINSEQ_1:def 3;
hence thesis by A3,GOBOARD1:def 1;
end;
theorem Th41:
for f being FinSequence of TOP-REAL 2 st 1 <=len f holds len
Y_axis(f)=len f & Y_axis(f).1=(f/.1)`2 & Y_axis(f).len f=(f/.len f)`2
proof
let f be FinSequence of TOP-REAL 2;
A1: len (Y_axis(f)) = len f by GOBOARD1:def 2;
assume
A2: 1 <=len f;
then len f in Seg len f by FINSEQ_1:1;
then
A3: len f in dom (Y_axis(f)) by A1,FINSEQ_1:def 3;
1 in Seg len f by A2,FINSEQ_1:1;
then 1 in dom (Y_axis(f)) by A1,FINSEQ_1:def 3;
hence thesis by A3,GOBOARD1:def 2;
end;
theorem Th42:
for f being FinSequence of TOP-REAL 2 st i in dom f holds X_axis
(f).i=(f/.i)`1 & Y_axis(f).i=(f/.i)`2
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: i in dom f;
len (X_axis(f)) = len f by GOBOARD1:def 1;
then i in dom (X_axis(f)) by A1,FINSEQ_3:29;
hence (X_axis(f)).i = (f/.i)`1 by GOBOARD1:def 1;
len (Y_axis(f)) = len f by GOBOARD1:def 2;
then i in dom Y_axis f by A1,FINSEQ_3:29;
hence thesis by GOBOARD1:def 2;
end;
:: Goboard Theorem in continuous case
theorem Th43:
for P,Q being non empty Subset of TOP-REAL 2, p1,p2,q1,q2 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & (for p
being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1) & (for p
being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1) & (for p
being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2) & (for p
being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2) holds P meets
Q
proof
let P,Q be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q is_an_arc_of q1,q2 and
A3: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2 `1 and
A4: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2 `1 and
A5: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2 `2 and
A6: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2 `2;
consider g being Function of I[01], (TOP-REAL 2) |Q such that
A7: g is being_homeomorphism and
A8: g.0 = q1 and
A9: g.1 = q2 by A2,TOPREAL1:def 1;
A10: the TopStruct of TOP-REAL 2 = TopSpaceMetr(Euclid 2) by EUCLID:def 8;
then reconsider P9=P,Q9=Q as Subset of TopSpaceMetr(Euclid 2);
P is compact by A1,JORDAN5A:1;
then
A11: P9 is compact by A10,COMPTS_1:23;
Q is compact by A2,JORDAN5A:1;
then
A12: Q9 is compact by A10,COMPTS_1:23;
set e=min_dist_min(P9,Q9)/5;
consider f being Function of I[01], (TOP-REAL 2) |P such that
A13: f is being_homeomorphism and
A14: f.0 = p1 and
A15: f.1 = p2 by A1,TOPREAL1:def 1;
consider f1 being Function of I[01],TOP-REAL 2 such that
A16: f=f1 and
A17: f1 is continuous and
f1 is one-to-one by A13,JORDAN7:15;
consider g1 being Function of I[01],TOP-REAL 2 such that
A18: g=g1 and
A19: g1 is continuous and
g1 is one-to-one by A7,JORDAN7:15;
assume P /\ Q= {};
then P misses Q;
then
A20: min_dist_min(P9,Q9)>0 by A11,A12,Th37;
then
A21: e>0/5 by XREAL_1:74;
then consider hb being FinSequence of REAL such that
A22: hb.1=0 and
A23: hb.len hb=1 and
A24: 5<=len hb and
A25: rng hb c= the carrier of I[01] and
A26: hb is increasing and
A27: for i being Nat,R being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len hb & R=[.hb/.i,hb/.(i+1).] & W=g1.:(R) holds
diameter(W)<e by A19,UNIFORM1:13;
consider h being FinSequence of REAL such that
A28: h.1=0 and
A29: h.len h=1 and
A30: 5<=len h and
A31: rng h c= the carrier of I[01] and
A32: h is increasing and
A33: for i being Nat,R being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len h & R=[.h/.i,h/.(i+1).] & W=f1.:(R) holds diameter(
W)<e by A17,A21,UNIFORM1:13;
deffunc F(Nat)=f1.(h.$1);
ex h19 being FinSequence st len h19=len h & for i be Nat st i in dom
h19 holds h19.i=F(i) from FINSEQ_1:sch 2;
then consider h19 being FinSequence such that
A34: len h19=len h and
A35: for i be Nat st i in dom h19 holds h19.i=f1.(h.i);
A36: dom g1= [#](I[01]) by A7,A18,TOPS_2:def 5
.=the carrier of I[01];
rng h19 c= the carrier of TOP-REAL 2
proof
let y be object;
assume y in rng h19;
then consider x being object such that
A37: x in dom h19 and
A38: y=h19.x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A37;
dom h19=Seg len h19 by FINSEQ_1:def 3;
then i in dom h by A34,A37,FINSEQ_1:def 3;
then
A39: h.i in rng h by FUNCT_1:def 3;
A40: dom f1= [#](I[01]) by A13,A16,TOPS_2:def 5
.=the carrier of I[01];
A41: rng f=[#]((TOP-REAL 2) |P) by A13,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
h19.i=f1.(h.i) by A35,A37;
then h19.i in rng f by A16,A31,A39,A40,FUNCT_1:def 3;
hence thesis by A38,A41;
end;
then reconsider h1=h19 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A42: len h1>=1 by A30,A34,XXREAL_0:2;
then
A43: h1.1=h1/.1 by FINSEQ_4:15;
A44: for i st 1<=i & i+1<=len h1 holds |.h1/.i-h1/.(i+1).|<e
proof
reconsider Pa=P as Subset of TOP-REAL 2;
reconsider W1=P as Subset of Euclid 2 by TOPREAL3:8;
let i;
assume that
A45: 1<=i and
A46: i+1<=len h1;
A47: 1<i+1 by A45,NAT_1:13;
then
A48: h.(i+1)=h/.(i+1) by A34,A46,FINSEQ_4:15;
A49: i+1 in dom h19 by A46,A47,FINSEQ_3:25;
then
A50: h19.(i+1)=f1.(h.(i+1)) by A35;
then
A51: h1/.(i+1)=f1.(h.(i+1)) by A46,A47,FINSEQ_4:15;
A52: i<len h1 by A46,NAT_1:13;
then
A53: h.i=h/.i by A34,A45,FINSEQ_4:15;
A54: i in dom h by A34,A45,A52,FINSEQ_3:25;
then
A55: h.i in rng h by FUNCT_1:def 3;
A56: i+1 in dom h by A34,A46,A47,FINSEQ_3:25;
then h.(i+1) in rng h by FUNCT_1:def 3;
then reconsider R=[.h/.i,h/.(i+1).] as Subset of I[01] by A31,A55,A53,A48,
BORSUK_1:40,XXREAL_2:def 12;
reconsider W=f1.:R as Subset of Euclid 2 by TOPREAL3:8;
A57: Pa is compact by A1,JORDAN5A:1;
reconsider Pa as non empty Subset of TOP-REAL 2;
A58: rng f=[#]((TOP-REAL 2) |P) by A13,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
set r1=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))+1;
A59: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
proof
let x,y be Point of Euclid 2;
assume that
A60: x in W1 and
A61: y in W1;
reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A60,A61;
A62: S-bound Pa <= pw2`2 & pw2`2 <= N-bound Pa by A57,A61,PSCOMP_1:24;
S-bound Pa <= pw1`2 & pw1`2 <= N-bound Pa by A57,A60,PSCOMP_1:24;
then
A63: |.pw1`2-pw2`2.|<=(N-bound Pa) - (S-bound Pa) by A62,Th27;
A64: W-bound Pa <= pw2`1 & pw2`1 <= E-bound Pa by A57,A61,PSCOMP_1:24;
W-bound Pa <= pw1`1 & pw1`1 <= E-bound Pa by A57,A60,PSCOMP_1:24;
then |.pw1`1-pw2`1.|<=(E-bound Pa) - (W-bound Pa) by A64,Th27;
then
A65: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Pa) - (W-bound Pa))+(
(N-bound Pa) - (S-bound Pa)) by A63,XREAL_1:7;
((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) <= ((
E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) +1 by XREAL_1:29;
then
A66: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A65,XXREAL_0:2;
dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-pw2
`2.| by Th28,Th32;
hence thesis by A66,XXREAL_0:2;
end;
A67: p1 in Pa by A1,TOPREAL1:1;
then S-bound Pa <= p1`2 & p1`2 <= N-bound Pa by A57,PSCOMP_1:24;
then (S-bound Pa)<=(N-bound Pa) by XXREAL_0:2;
then
A68: 0<=((N-bound Pa) - (S-bound Pa)) by XREAL_1:48;
W-bound Pa <= p1`1 & p1`1 <= E-bound Pa by A57,A67,PSCOMP_1:24;
then (W-bound Pa)<=(E-bound Pa) by XXREAL_0:2;
then 0<=((E-bound Pa) - (W-bound Pa)) by XREAL_1:48;
then
A69: W1 is bounded by A68,A59,TBSP_1:def 7;
A70: dom f1= [#](I[01]) by A13,A16,TOPS_2:def 5
.=the carrier of I[01];
i+1 in dom h by A34,A46,A47,FINSEQ_3:25;
then h.(i+1) in rng h by FUNCT_1:def 3;
then h19.(i+1) in rng f by A16,A31,A50,A70,FUNCT_1:def 3;
then
A71: f1.(h.(i+1)) is Element of TOP-REAL 2 by A35,A49,A58;
A72: i in dom h19 by A45,A52,FINSEQ_3:25;
then
A73: h19.i=f1.(h.i) by A35;
then h19.i in rng f by A16,A31,A55,A70,FUNCT_1:def 3;
then f1.(h.i) is Element of TOP-REAL 2 by A35,A72,A58;
then reconsider w1=f1.(h.i),w2=f1.(h.(i+1)) as Point of Euclid 2 by A71,
TOPREAL3:8;
i<i+1 by NAT_1:13;
then
A74: h/.i <= h/.(i+1) by A32,A54,A53,A56,A48,SEQM_3:def 1;
then h.i in R by A53,XXREAL_1:1;
then
A75: w1 in f1.:R by A70,FUNCT_1:def 6;
h.(i+1) in R by A48,A74,XXREAL_1:1;
then
A76: w2 in f1.:R by A70,FUNCT_1:def 6;
dom f1=[#](I[01]) by A13,A16,TOPS_2:def 5;
then P=f1.:([.0,1.]) by A16,A58,BORSUK_1:40,RELAT_1:113;
then W is bounded by A69,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
then
A77: dist(w1,w2)<=diameter(W) by A75,A76,TBSP_1:def 8;
diameter(W)<e by A33,A34,A45,A52;
then
A78: dist(w1,w2)<e by A77,XXREAL_0:2;
h1/.i=f1.(h.i) by A45,A52,A73,FINSEQ_4:15;
hence thesis by A51,A78,Th28;
end;
A79: for i st i in dom h1 holds (h1/.1)`1<=(h1/.i)`1 & (h1/.i)`1<=(h1/.len
h1)`1
proof
len h in dom h19 by A34,A42,FINSEQ_3:25;
then h1.len h1=f1.(h.len h) by A34,A35;
then
A80: h1/.len h1=f1.(h.len h) by A42,FINSEQ_4:15;
let i;
assume
A81: i in dom h1;
then h1.i=f1.(h.i) by A35;
then
A82: h1/.i=f1.(h.i) by A81,PARTFUN1:def 6;
i in Seg len h by A34,A81,FINSEQ_1:def 3;
then i in dom h by FINSEQ_1:def 3;
then
A83: h.i in rng h by FUNCT_1:def 3;
dom f1= [#](I[01]) by A13,A16,TOPS_2:def 5
.=the carrier of I[01];
then
A84: h1/.i in rng f by A16,A31,A82,A83,FUNCT_1:def 3;
1 in dom h19 by A42,FINSEQ_3:25;
then h1.1=f1.(h.1) by A35;
then
A85: h1/.1=f1.(h.1) by A42,FINSEQ_4:15;
rng f=[#]((TOP-REAL 2) |P) by A13,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
hence thesis by A3,A14,A15,A16,A28,A29,A85,A80,A84;
end;
for i st i in dom (X_axis(h1)) holds (X_axis(h1)).1<=(X_axis(h1)).i &
(X_axis(h1)).i<=(X_axis(h1)).(len h1)
proof
let i;
A86: (X_axis(h1)).1=(h1/.1)`1 & (X_axis(h1)).len h1=(h1/.len h1)`1 by A42,Th40;
assume i in dom (X_axis(h1));
then i in Seg len (X_axis(h1)) by FINSEQ_1:def 3;
then i in Seg len h1 by A42,Th40;
then
A87: i in dom h1 by FINSEQ_1:def 3;
then (X_axis(h1)).i = (h1/.i)`1 by Th42;
hence thesis by A79,A87,A86;
end;
then
A88: X_axis(h1) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) by
GOBOARD4:def 2;
A89: for i st i in dom h1 holds q1`2<=(h1/.i)`2 & (h1/.i)`2<=q2`2
proof
let i;
A90: rng f=[#]((TOP-REAL 2) |P) by A13,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
assume
A91: i in dom h1;
then h1.i=f1.(h.i) by A35;
then
A92: h1/.i=f1.(h.i) by A91,PARTFUN1:def 6;
i in Seg len h1 by A91,FINSEQ_1:def 3;
then i in dom h by A34,FINSEQ_1:def 3;
then
A93: h.i in rng h by FUNCT_1:def 3;
dom f1= [#](I[01]) by A13,A16,TOPS_2:def 5
.=the carrier of I[01];
then h1/.i in rng f by A16,A31,A92,A93,FUNCT_1:def 3;
hence thesis by A5,A90;
end;
for i st i in dom (Y_axis(h1)) holds q1`2<=(Y_axis(h1)).i & (Y_axis(h1
)).i<=q2`2
proof
let i;
assume i in dom (Y_axis(h1));
then i in Seg len (Y_axis(h1)) by FINSEQ_1:def 3;
then i in Seg len h1 by A42,Th41;
then
A94: i in dom h1 by FINSEQ_1:def 3;
then (Y_axis(h1)).i = (h1/.i)`2 by Th42;
hence thesis by A89,A94;
end;
then Y_axis(h1) lies_between q1`2,q2`2 by GOBOARD4:def 2;
then consider f2 being FinSequence of TOP-REAL 2 such that
A95: f2 is special and
A96: f2.1=h1.1 and
A97: f2.len f2=h1.len h1 and
A98: len f2>=len h1 and
A99: X_axis(f2) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
Y_axis(f2) lies_between q1`2,q2`2 and
A100: for j st j in dom f2 holds ex k st k in dom h1 & |.(f2/.j - h1/.k
).|<e and
A101: for j st 1<=j & j+1<=len f2 holds |.f2/.j - f2/.(j+1).|<e by A21,A44,A42
,A88,Th38;
A102: len f2>=1 by A42,A98,XXREAL_0:2;
then
A103: f2.len f2=f2/.len f2 by FINSEQ_4:15;
deffunc F(Nat)=g1.(hb.$1);
ex h29 being FinSequence st len h29=len hb & for i be Nat st i in dom
h29 holds h29.i=F(i) from FINSEQ_1:sch 2;
then consider h29 being FinSequence such that
A104: len h29=len hb and
A105: for i be Nat st i in dom h29 holds h29.i=g1.(hb.i);
rng h29 c= the carrier of TOP-REAL 2
proof
let y be object;
assume y in rng h29;
then consider x being object such that
A106: x in dom h29 and
A107: y=h29.x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A106;
dom h29=Seg len h29 by FINSEQ_1:def 3;
then i in dom hb by A104,A106,FINSEQ_1:def 3;
then
A108: hb.i in rng hb by FUNCT_1:def 3;
A109: dom g1= [#](I[01]) by A7,A18,TOPS_2:def 5
.=the carrier of I[01];
A110: rng g=[#]((TOP-REAL 2) |Q) by A7,TOPS_2:def 5
.=Q by PRE_TOPC:def 5;
h29.i=g1.(hb.i) by A105,A106;
then h29.i in rng g by A18,A25,A108,A109,FUNCT_1:def 3;
hence thesis by A107,A110;
end;
then reconsider h2=h29 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A111: rng f=[#]((TOP-REAL 2) |P) by A13,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
A112: for i st 1<=i & i+1<=len h2 holds |. (h2/.i)-(h2/.(i+1)) .|<e
proof
reconsider Qa=Q as Subset of TOP-REAL 2;
reconsider W1=Q as Subset of Euclid 2 by TOPREAL3:8;
let i;
assume that
A113: 1<=i and
A114: i+1<=len h2;
A115: Qa is compact by A2,JORDAN5A:1;
reconsider Qa as non empty Subset of TOP-REAL 2;
A116: rng g=[#]((TOP-REAL 2) |Q) by A7,TOPS_2:def 5
.=Q by PRE_TOPC:def 5;
set r1= ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))+1;
A117: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
proof
let x,y be Point of Euclid 2;
assume that
A118: x in W1 and
A119: y in W1;
reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A118,A119;
A120: S-bound Qa <= pw2`2 & pw2`2 <= N-bound Qa by A115,A119,PSCOMP_1:24;
S-bound Qa <= pw1`2 & pw1`2 <= N-bound Qa by A115,A118,PSCOMP_1:24;
then
A121: |.pw1`2-pw2`2.|<=(N-bound Qa) - (S-bound Qa) by A120,Th27;
A122: W-bound Qa <= pw2`1 & pw2`1 <= E-bound Qa by A115,A119,PSCOMP_1:24;
W-bound Qa <= pw1`1 & pw1`1 <= E-bound Qa by A115,A118,PSCOMP_1:24;
then |.pw1`1-pw2`1.|<=(E-bound Qa) - (W-bound Qa) by A122,Th27;
then
A123: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Qa) - (W-bound Qa))+
((N-bound Qa) - (S-bound Qa)) by A121,XREAL_1:7;
((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) <= ((
E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) +1 by XREAL_1:29;
then
A124: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A123,XXREAL_0:2;
dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-
pw2`2.| by Th28,Th32;
hence thesis by A124,XXREAL_0:2;
end;
A125: q1 in Qa by A2,TOPREAL1:1;
then S-bound Qa <= q1`2 & q1`2 <= N-bound Qa by A115,PSCOMP_1:24;
then (S-bound Qa)<=(N-bound Qa) by XXREAL_0:2;
then
A126: 0<=((N-bound Qa) - (S-bound Qa)) by XREAL_1:48;
W-bound Qa <= q1`1 & q1`1 <= E-bound Qa by A115,A125,PSCOMP_1:24;
then (W-bound Qa)<=(E-bound Qa) by XXREAL_0:2;
then 0<=((E-bound Qa) - (W-bound Qa)) by XREAL_1:48;
then
A127: W1 is bounded by A126,A117,TBSP_1:def 7;
A128: dom g1= [#](I[01]) by A7,A18,TOPS_2:def 5
.=the carrier of I[01];
A129: 1<i+1 by A113,NAT_1:13;
then i+1 in Seg len hb by A104,A114,FINSEQ_1:1;
then i+1 in dom hb by FINSEQ_1:def 3;
then
A130: hb.(i+1) in rng hb by FUNCT_1:def 3;
A131: i<len h2 by A114,NAT_1:13;
then
A132: hb.i=hb/.i by A104,A113,FINSEQ_4:15;
A133: i+1 in dom h29 by A114,A129,FINSEQ_3:25;
then h29.(i+1)=g1.(hb.(i+1)) by A105;
then h29.(i+1) in rng g by A18,A25,A128,A130,FUNCT_1:def 3;
then
A134: g1.(hb.(i+1)) is Element of TOP-REAL 2 by A105,A133,A116;
A135: hb.(i+1)=hb/.(i+1) by A104,A114,A129,FINSEQ_4:15;
i in dom h29 by A113,A131,FINSEQ_3:25;
then
A136: h29.i=g1.(hb.i) by A105;
i in Seg len hb by A104,A113,A131,FINSEQ_1:1;
then
A137: i in dom hb by FINSEQ_1:def 3;
then
A138: hb.i in rng hb by FUNCT_1:def 3;
then h29.i in rng g by A18,A25,A136,A128,FUNCT_1:def 3;
then reconsider
w1=g1.(hb.i),w2=g1.(hb.(i+1)) as Point of Euclid 2 by A136,A116,A134,
TOPREAL3:8;
i+1 in Seg len hb by A104,A114,A129,FINSEQ_1:1;
then
A139: i+1 in dom hb by FINSEQ_1:def 3;
then hb.(i+1) in rng hb by FUNCT_1:def 3;
then reconsider
R=[.hb/.i,hb/.(i+1).] as Subset of I[01] by A25,A138,A132,A135,BORSUK_1:40
,XXREAL_2:def 12;
i<i+1 by NAT_1:13;
then
A140: hb/.i <= hb/.(i+1) by A26,A137,A132,A139,A135,SEQM_3:def 1;
then hb.i in R by A132,XXREAL_1:1;
then
A141: w1 in g1.:(R) by A128,FUNCT_1:def 6;
hb.(i+1) in R by A135,A140,XXREAL_1:1;
then
A142: w2 in g1.:(R) by A128,FUNCT_1:def 6;
reconsider W=g1.:(R) as Subset of Euclid 2 by TOPREAL3:8;
dom g1=[#](I[01]) by A7,A18,TOPS_2:def 5;
then Q=g1.:([.0,1.]) by A18,A116,BORSUK_1:40,RELAT_1:113;
then W is bounded by A127,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
then
A143: dist(w1,w2)<=diameter(W) by A141,A142,TBSP_1:def 8;
diameter(W)<e by A27,A104,A113,A131;
then
A144: dist(w1,w2)<e by A143,XXREAL_0:2;
h2.(i+1)=h2/.(i+1) by A114,A129,FINSEQ_4:15;
then
A145: h2/.(i+1)=g1.(hb.(i+1)) by A105,A133;
h2/.i=g1.(hb.i) by A113,A131,A136,FINSEQ_4:15;
hence thesis by A145,A144,Th28;
end;
A146: 1<=len hb by A24,XXREAL_0:2;
then
A147: len hb in dom hb by FINSEQ_3:25;
A148: 1<=len hb by A24,XXREAL_0:2;
then
A149: h2.len h2=h2/.len h2 by A104,FINSEQ_4:15;
A150: dom hb=Seg len hb by FINSEQ_1:def 3;
A151: for i st i in dom hb holds h2/.i=g1.(hb.i)
proof
let i;
assume
A152: i in dom hb;
then i in dom h29 by A104,FINSEQ_3:29;
then
A153: h2.i=g1.(hb.i) by A105;
1<=i & i<=len hb by A150,A152,FINSEQ_1:1;
hence thesis by A104,A153,FINSEQ_4:15;
end;
A154: f2.1=f2/.1 by A102,FINSEQ_4:15;
A155: 1<=len h by A30,XXREAL_0:2;
then 1 in dom h19 by A34,FINSEQ_3:25;
then
A156: h1/.1=f1.(h.1) by A35,A43;
len h in dom h19 by A34,A155,FINSEQ_3:25;
then
A157: f2/.1<>f2/.len f2 by A1,A14,A15,A16,A28,A29,A34,A35,A96,A97,A43,A154,A103
,A156,JORDAN6:37;
5<=len f2 by A30,A34,A98,XXREAL_0:2;
then
A158: 2<=len f2 by XXREAL_0:2;
A159: h1.len h1=h1/.len h1 by A42,FINSEQ_4:15;
then
A160: X_axis(f2).len f2=(h1/.len h1)`1 by A97,A102,A103,Th40
.=X_axis(h1).len h1 by A42,Th40;
A161: h2.1=h2/.1 by A148,A104,FINSEQ_4:15;
A162: len h2>=1 by A24,A104,XXREAL_0:2;
A163: for i st i in dom h2 holds (h2/.1)`2<=(h2/.i)`2 & (h2/.i)`2<=(h2/.len
h2)`2
proof
let i;
assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then i in dom hb by A104,FINSEQ_1:def 3;
then
A164: h2/.i=g1.(hb.i) & hb.i in rng hb by A151,FUNCT_1:def 3;
dom g1= [#](I[01]) by A7,A18,TOPS_2:def 5
.=the carrier of I[01];
then
A165: h2/.i in rng g by A18,A25,A164,FUNCT_1:def 3;
1 in Seg len hb by A104,A162,FINSEQ_1:1;
then 1 in dom hb by FINSEQ_1:def 3;
then
A166: h2/.1=g1.(hb.1) by A151;
len hb in Seg len hb by A104,A162,FINSEQ_1:1;
then len hb in dom hb by FINSEQ_1:def 3;
then
A167: h2/.len h2=g1.(hb.len hb) by A104,A151;
rng g=[#]((TOP-REAL 2) |Q) by A7,TOPS_2:def 5
.=Q by PRE_TOPC:def 5;
hence thesis by A6,A8,A9,A18,A22,A23,A166,A167,A165;
end;
for i st i in dom (Y_axis(h2)) holds (Y_axis(h2)).1<=(Y_axis(h2)).i &
(Y_axis(h2)).i <=(Y_axis(h2)).(len h2)
proof
let i;
A168: (Y_axis(h2)).1=(h2/.1)`2 & (Y_axis(h2)).len h2=(h2/.len h2)`2 by A162
,Th41;
assume i in dom (Y_axis(h2));
then i in Seg len (Y_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A162,Th41;
then
A169: i in dom h2 by FINSEQ_1:def 3;
then (Y_axis(h2)).i = (h2/.i)`2 by Th42;
hence thesis by A163,A169,A168;
end;
then
A170: Y_axis(h2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) by
GOBOARD4:def 2;
A171: for i st i in dom h2 holds p1`1<=(h2/.i)`1 & (h2/.i)`1<=p2`1
proof
let i;
A172: rng g=[#]((TOP-REAL 2) |Q) by A7,TOPS_2:def 5
.=Q by PRE_TOPC:def 5;
assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then i in dom hb by A104,FINSEQ_1:def 3;
then
A173: h2/.i=g1.(hb.i) & hb.i in rng hb by A151,FUNCT_1:def 3;
dom g1= [#](I[01]) by A7,A18,TOPS_2:def 5
.=the carrier of I[01];
then h2/.i in rng g by A18,A25,A173,FUNCT_1:def 3;
hence thesis by A4,A172;
end;
for i st i in dom (X_axis(h2)) holds p1`1<= (X_axis(h2)).i & (X_axis(
h2)).i<=p2`1
proof
let i;
assume i in dom (X_axis(h2));
then i in Seg len (X_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A162,Th40;
then
A174: i in dom h2 by FINSEQ_1:def 3;
then (X_axis(h2)).i = (h2/.i)`1 by Th42;
hence thesis by A171,A174;
end;
then X_axis(h2) lies_between p1`1, p2`1 by GOBOARD4:def 2;
then consider g2 being FinSequence of TOP-REAL 2 such that
A175: g2 is special and
A176: g2.1=h2.1 and
A177: g2.len g2=h2.len h2 and
A178: len g2>=len h2 and
A179: Y_axis(g2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) &
X_axis(g2) lies_between p1`1,p2`1 and
A180: for j st j in dom g2 holds ex k st k in dom h2 & |.((g2/.j) - h2
/.k).|<e and
A181: for j st 1<=j & j+1<=len g2 holds |.(g2/.j) - g2/.(j+1).|<e by A21,A162
,A170,A112,Th39;
5<=len g2 by A24,A104,A178,XXREAL_0:2;
then
A182: 2<=len g2 by XXREAL_0:2;
A183: len g2>=1 by A162,A178,XXREAL_0:2;
then g2.1=g2/.1 by FINSEQ_4:15;
then
A184: (Y_axis(g2)).1=(h2/.1)`2 by A176,A183,A161,Th41
.=(Y_axis(h2)).1 by A162,Th41;
1 in dom hb by A146,FINSEQ_3:25;
then h2/.1=g1.(hb.1) by A151;
then
A185: g2.1<>g2.len g2 by A2,A8,A9,A18,A22,A23,A104,A151,A176,A177,A161,A149
,A147,JORDAN6:37;
len hb in dom hb by A148,FINSEQ_3:25;
then
A186: (g2.len g2)=q2 by A9,A18,A23,A104,A151,A177,A149;
g2/.len g2=g2.len g2 by A183,FINSEQ_4:15;
then
A187: Y_axis(g2).len g2=q2`2 by A183,A186,Th41;
1 in dom hb by A148,FINSEQ_3:25;
then
A188: (h2/.1)=q1 by A8,A18,A22,A151;
A189: rng g=[#]((TOP-REAL 2) |Q) by A7,TOPS_2:def 5
.=Q by PRE_TOPC:def 5;
len h in dom h19 by A34,A42,FINSEQ_3:25;
then (h1/.len h1)=p2 by A15,A16,A29,A34,A35,A159;
then
A190: X_axis(f2).len f2=p2`1 by A97,A102,A159,A103,Th40;
1 in dom h19 by A42,FINSEQ_3:25;
then h1.1=f1.(h.1) by A35;
then
A191: X_axis(f2).1=p1`1 by A14,A16,A28,A96,A102,A154,Th40;
g2.len g2=g2/.len g2 by A183,FINSEQ_4:15;
then
A192: Y_axis(g2).len g2=(h2/.len h2)`2 by A177,A183,A149,Th41
.=Y_axis(h2).len h2 by A162,Th41;
g2/.1=g2.1 by A183,FINSEQ_4:15;
then
A193: Y_axis(g2).1=q1`2 by A176,A183,A188,A161,Th41;
(X_axis(f2)).1=(h1/.1)`1 by A96,A102,A43,A154,Th40
.=(X_axis(h1)).1 by A42,Th40;
then L~f2 meets L~g2 by A95,A99,A175,A179,A154,A103,A191,A190,A193,A187,A160
,A184,A192,A158,A182,A157,A185,Th26;
then consider s being object such that
A194: s in L~f2 and
A195: s in L~g2 by XBOOLE_0:3;
reconsider ps=s as Point of TOP-REAL 2 by A194;
ps in union{ LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by A195,TOPREAL1:def 4;
then consider y such that
A196: ps in y & y in { LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by TARSKI:def 4;
ps in union{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by A194,TOPREAL1:def 4;
then consider x such that
A197: ps in x & x in { LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by TARSKI:def 4;
consider i such that
A198: x=LSeg(f2,i) and
A199: 1 <= i and
A200: i+1 <= len f2 by A197;
LSeg(f2,i)=LSeg(f2/.i,f2/.(i+1)) by A199,A200,TOPREAL1:def 3;
then
A201: |.ps-f2/.i.|<=|.f2/.i-f2/.(i+1).| by A197,A198,Th35;
i<len f2 by A200,NAT_1:13;
then i in dom f2 by A199,FINSEQ_3:25;
then consider k such that
A202: k in dom h1 and
A203: |.f2/.i - h1/.k.|<e by A100;
k in dom h by A34,A202,FINSEQ_3:29;
then
A204: h.k in rng h by FUNCT_1:def 3;
reconsider p11=h1/.k as Point of TOP-REAL 2;
|.f2/.i-f2/.(i+1).|<e by A101,A199,A200;
then |.ps-f2/.i.|<e by A201,XXREAL_0:2;
then |.ps-h1/.k.|<=|.ps-f2/.i.|+|.f2/.i-h1/.k.| & |.ps-f2/.i.|+|.f2/.i-h1/.
k.|<e+ e by A203,TOPRNS_1:34,XREAL_1:8;
then |.ps-h1/.k.|<e+e by XXREAL_0:2;
then
A205: |.(p11-ps).|<e+e by TOPRNS_1:27;
k in Seg len h1 by A202,FINSEQ_1:def 3;
then 1<=k & k<=len h1 by FINSEQ_1:1;
then h1.k=h1/.k by FINSEQ_4:15;
then
A206: h1/.k=f1.(h.k) by A35,A202;
consider j such that
A207: y=LSeg(g2,j) and
A208: 1 <= j and
A209: j+1 <= len g2 by A196;
LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) by A208,A209,TOPREAL1:def 3;
then
A210: |.ps-(g2/.j).|<=|.(g2/.j)-g2/.(j+1).| by A196,A207,Th35;
j<len g2 by A209,NAT_1:13;
then j in Seg len g2 by A208,FINSEQ_1:1;
then j in dom g2 by FINSEQ_1:def 3;
then consider k9 being Nat such that
A211: k9 in dom h2 and
A212: |.((g2/.j) - h2/.k9).|<e by A180;
k9 in Seg len h2 by A211,FINSEQ_1:def 3;
then
A213: k9 in dom hb by A104,FINSEQ_1:def 3;
then
A214: hb.k9 in rng hb by FUNCT_1:def 3;
reconsider q11=h2/.k9 as Point of TOP-REAL 2;
|.(g2/.j)-g2/.(j+1).|<e by A181,A208,A209;
then |.ps-(g2/.j).|<e by A210,XXREAL_0:2;
then |.ps-h2/.k9.|<=|.ps-(g2/.j).|+|.(g2/.j)-h2/.k9.| & |.ps-(g2/.j).|+|.(
g2/.j)- (h2/.k9).|<e+e by A212,TOPRNS_1:34,XREAL_1:8;
then |.ps-(h2/.k9).|<e+e by XXREAL_0:2;
then |.(p11-q11).|<= |.(p11-ps).|+|.(ps-q11).| & |.(p11-ps).|+|.(ps-q11).|
<e+e+( e+e) by A205,TOPRNS_1:34,XREAL_1:8;
then
A215: |.(p11-q11).|<e+e+e+e by XXREAL_0:2;
h2/.k9=g1.(hb.k9) by A151,A213;
then
A216: h2/.k9 in rng g by A18,A25,A214,A36,FUNCT_1:def 3;
reconsider x1=p11,x2=q11 as Point of Euclid 2 by EUCLID:22;
dom f1= [#](I[01]) by A13,A16,TOPS_2:def 5
.=the carrier of I[01];
then h1/.k in P by A16,A31,A206,A204,A111,FUNCT_1:def 3;
then min_dist_min(P9,Q9)<=dist(x1,x2) by A11,A12,A216,A189,WEIERSTR:34;
then min_dist_min(P9,Q9)<=|.(p11-q11).| by Th28;
then min_dist_min(P9,Q9)<4*e by A215,XXREAL_0:2;
then 4*e-5*e>0 by XREAL_1:50;
then (4-5)*e/e>0 by A21,XREAL_1:139;
then 4-5>0 by A20;
hence contradiction;
end;
reserve X,Y for non empty TopSpace;
theorem Th44:
for f being Function of X,Y, P being non empty Subset of Y, f1
being Function of X,Y|P st f=f1 & f is continuous holds f1 is continuous
proof
let f be Function of X,Y, P be non empty Subset of Y, f1 be Function of X,Y|
P;
assume that
A1: f=f1 and
A2: f is continuous;
A3: [#]Y <> {};
A4: for P1 being Subset of (Y|P) st P1 is open holds f1"P1 is open
proof
let P1 be Subset of (Y|P);
assume P1 is open;
then P1 in the topology of (Y|P) by PRE_TOPC:def 2;
then consider Q being Subset of Y such that
A5: Q in the topology of Y and
A6: P1 = Q /\ [#](Y|P) by PRE_TOPC:def 4;
reconsider Q as Subset of Y;
A7: f"Q=f1"(rng f1 /\ Q) by A1,RELAT_1:133;
A8: [#](Y|P)=P by PRE_TOPC:def 5;
then rng f1 /\ Q c= P /\ Q by XBOOLE_1:26;
then
A9: f1"(rng f1 /\ Q) c= f1"P1 by A6,A8,RELAT_1:143;
Q is open by A5,PRE_TOPC:def 2;
then
A10: f"Q is open by A3,A2,TOPS_2:43;
f1"P1 c= f"Q by A1,A6,RELAT_1:143,XBOOLE_1:17;
hence thesis by A10,A7,A9,XBOOLE_0:def 10;
end;
[#](Y|P) <> {};
hence thesis by A4,TOPS_2:43;
end;
theorem Th45:
for f being Function of X,Y, P being non empty Subset of Y st X
is compact & Y is T_2 & f is continuous one-to-one & P=rng f holds ex f1 being
Function of X,(Y|P) st f=f1 & f1 is being_homeomorphism
proof
let f be Function of X,Y,P be non empty Subset of Y such that
A1: X is compact and
A2: Y is T_2 and
A3: f is continuous one-to-one and
A4: P=rng f;
the carrier of (Y|P)=P & dom f=the carrier of X by FUNCT_2:def 1,PRE_TOPC:8;
then reconsider f2=f as Function of X,(Y|P) by A4,FUNCT_2:1;
A5: dom f2=[#]X & f2 is continuous by A3,Th44,FUNCT_2:def 1;
rng f2=[#](Y|P) & Y|P is T_2 by A2,A4,PRE_TOPC:def 5,TOPMETR:2;
hence thesis by A1,A3,A5,COMPTS_1:17;
end;
::$N Fashoda Meet Theorem
theorem
for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real ,
O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is
continuous one-to-one & (f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d & (for r
being Point of I[01] holds a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)`1<=b
& c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d) holds rng f meets rng g
proof
let f,g be Function of I[01],TOP-REAL 2,a,b,c,d be Real, O,I be Point
of I[01];
assume that
A1: O=0 & I=1 and
A2: f is continuous one-to-one and
A3: g is continuous one-to-one and
A4: (f.O)`1=a and
A5: (f.I)`1=b and
A6: (g.O)`2=c and
A7: (g.I)`2=d and
A8: for r being Point of I[01] holds a<=(f.r)`1 & (f.r)`1<=b & a<=(g.r)
`1 & (g.r)`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d;
reconsider P=rng f as non empty Subset of TOP-REAL 2;
A9: I[01] is compact by HEINE:4,TOPMETR:20;
then consider f1 being Function of I[01],((TOP-REAL 2) |P) such that
A10: f=f1 and
A11: f1 is being_homeomorphism by A2,Th45;
reconsider Q=rng g as non empty Subset of TOP-REAL 2;
consider g1 being Function of I[01],((TOP-REAL 2) |Q) such that
A12: g=g1 and
A13: g1 is being_homeomorphism by A3,A9,Th45;
reconsider q2=g1.I as Point of TOP-REAL 2 by A7,A12;
reconsider q1=g1.O as Point of TOP-REAL 2 by A6,A12;
A14: Q is_an_arc_of q1,q2 by A1,A13,TOPREAL1:def 1;
reconsider p2=f1.I as Point of TOP-REAL 2 by A5,A10;
reconsider p1=f1.O as Point of TOP-REAL 2 by A4,A10;
A15: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1
proof
let p be Point of TOP-REAL 2;
assume p in P;
then ex x being object st x in dom f1 & p=f1.x by A10,FUNCT_1:def 3;
hence thesis by A4,A5,A8,A10;
end;
A16: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1
proof
let p be Point of TOP-REAL 2;
assume p in Q;
then ex x being object st x in dom g1 & p=g1.x by A12,FUNCT_1:def 3;
hence thesis by A4,A5,A8,A10,A12;
end;
A17: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2 `2
proof
let p be Point of TOP-REAL 2;
assume p in Q;
then ex x being object st x in dom g1 & p=g1.x by A12,FUNCT_1:def 3;
hence thesis by A6,A7,A8,A12;
end;
A18: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2
proof
let p be Point of TOP-REAL 2;
assume p in P;
then ex x being object st x in dom f1 & p=f1.x by A10,FUNCT_1:def 3;
hence thesis by A6,A7,A8,A10,A12;
end;
P is_an_arc_of p1,p2 by A1,A11,TOPREAL1:def 1;
hence thesis by A14,A15,A16,A18,A17,Th43;
end;