:: Graph Theoretical Properties of Arcs in the Plane and Fashoda
:: Meet Theorem
:: by Yatsuka Nakamura
::
:: Received August 21, 1998
:: Copyright (c) 1998-2016 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;
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;
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 {};
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=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 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 FinSequence of the carrier' of PGraph(X);
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=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 oriented Chain of PGraph(X);
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=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 st g is_Shortcut_of f holds 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 gf.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 {} 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: i1i2;
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: j1 or j+1i;
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: iLSeg(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=1 by A6,NAT_D:44;
then
A8: f1 is_oriented_vertex_seq_of PairF(f) by Th7;
A9: 1+1i 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*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**{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**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=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 {};
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: i1 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 & if.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{} by A7,XBOOLE_0:def 4;
then
A8: LSeg(f,1) meets LSeg(f,2);
A9: len f{} 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;
then
A10: i=len g by A6,XXREAL_0:1;
now
per cases;
case
A11: 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 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 1f1.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;
kg2.(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;
kg1.(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) .|
=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 .|0 and
A5: for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|=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=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,EUCLID:52;
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,EUCLID:52;
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) .|0 by A91,A97,A98;
then j>=0 qua Nat+1 by NAT_1:13;
then |. f/.j-f/.(j+1) .|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,EUCLID:52;
A125: (g1/.i)`2=(f/.(j+1))`2 by A119,A123,EUCLID:52;
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 by EUCLID:52;
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,EUCLID:52
.= 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) .|0 & (for i st 1<=i & i+1<=len f holds |. (f/.i)-(f/.(i+1)
) .|=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) .|0 and
A6: for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|=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**=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 by EUCLID:52;
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) .|*0 by A68,A74,A75;
then j>=0 qua Nat+1 by NAT_1:13;
then |. f/.j-f/.(j+1) .|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 by EUCLID:52;
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 by EUCLID:52;
(g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by A97,EUCLID:52;
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,EUCLID:52;
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) .|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=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).|=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
).|=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)) .|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).|=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;
i0 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;