:: Homeomorphisms of {J}ordan Curves
:: by Adam Naumowicz and Grzegorz Bancerek
::
:: Received September 15, 2005
:: Copyright (c) 2005-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, PRE_TOPC, EUCLID, TOPREAL2, SUBSET_1, METRIC_1,
XXREAL_0, ARYTM_1, CARD_1, PCOMPS_1, XBOOLE_0, RCOMP_1, WEIERSTR,
FUNCT_1, VECTMETR, ORDINAL2, CONNSP_2, TOPS_1, TARSKI, RELAT_1, ARYTM_3,
TOPS_2, REAL_1, FINSEQ_6, COMPLEX1, MCART_1, XCMPLX_0, INT_1, SIN_COS,
COMPTRIG, STRUCT_0, SQUARE_1, JGRAPH_2, TOPGRP_1, FUNCT_2, RELAT_2,
CONNSP_1, JORDAN1, JORDAN24;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, SQUARE_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
REAL_1, INT_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, COMPTS_1,
METRIC_1, PCOMPS_1, EUCLID, TOPREAL2, JORDAN1, TOPREAL6, WEIERSTR,
VECTMETR, CONNSP_2, JGRAPH_2, COMPLEX2, COMPTRIG, SIN_COS, TOPGRP_1,
TMAP_1;
constructors REAL_1, SQUARE_1, SIN_COS, COMPTRIG, COMPLEX2, TOPS_1, CONNSP_1,
TOPS_2, COMPTS_1, TMAP_1, TOPREAL2, JORDAN1, WEIERSTR, TOPGRP_1,
VECTMETR, TOPREAL6, JGRAPH_2, FUNCSDOM, NEWTON;
registrations RELSET_1, FUNCT_2, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1,
STRUCT_0, PRE_TOPC, PCOMPS_1, EUCLID, TOPREAL2, TOPGRP_1, VECTMETR,
INT_1, SIN_COS6, TMAP_1, RELAT_1, SIN_COS, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_2, CONNSP_1, BORSUK_1, VECTMETR, TOPS_2,
SPRECT_1;
equalities XBOOLE_0, COMPLEX2, SQUARE_1, SUBSET_1, PCOMPS_1, STRUCT_0;
expansions XBOOLE_0, FUNCT_2, TOPS_2;
theorems TOPGRP_1, PRE_TOPC, EUCLID, SQUARE_1, XREAL_1, JORDAN1K, JGRAPH_7,
TOPREAL2, TOPS_2, FUNCT_2, RELAT_1, FUNCT_1, XBOOLE_1, WEIERSTR,
CONNSP_2, GOBOARD6, METRIC_1, VECTMETR, JGRAPH_2, COMPLEX2, XCMPLX_0,
COMPLEX1, COMPTRIG, SIN_COS, XCMPLX_1, TMAP_1, JORDAN16, RFUNCT_2,
TIETZE, XXREAL_0, XBOOLE_0, TOPREAL6, COMPTS_1;
schemes FUNCT_2;
begin
reserve p1, p2 for Point of TOP-REAL 2,
C for Simple_closed_curve,
P for Subset of TOP-REAL 2;
definition
let n be Element of NAT, A be Subset of TOP-REAL n, a, b be Point of
TOP-REAL n;
pred a,b realize-max-dist-in A means
a in A & b in A & for x, y being
Point of TOP-REAL n st x in A & y in A holds dist(a,b) >= dist(x,y);
end;
set rl = -1;
set rp = 1;
set a = |[rl,0]|;
set b = |[rp,0]|;
Lm1: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
theorem Th1:
for C being non empty compact Subset of TOP-REAL 2 ex p1,p2 st p1
,p2 realize-max-dist-in C
proof
let C be non empty compact Subset of TOP-REAL 2;
reconsider D=C as Subset of TopSpaceMetr Euclid 2 by Lm1;
A1: D is compact by Lm1,COMPTS_1:23;
then consider x1,x2 being Point of Euclid 2 such that
A2: x1 in D & x2 in D and
A3: dist(x1,x2) = max_dist_max(D,D) by WEIERSTR:33;
reconsider a=x1,b=x2 as Point of TOP-REAL 2 by EUCLID:67;
take a,b;
thus a in C & b in C by A2;
let x, y be Point of TOP-REAL 2 such that
A4: x in C & y in C;
reconsider x9=x,y9=y as Point of Euclid 2 by EUCLID:67;
dist(x9,y9) <= max_dist_max(D,D) by A1,A4,WEIERSTR:34;
then dist(x,y) <= max_dist_max(D,D) by TOPREAL6:def 1;
hence thesis by A3,TOPREAL6:def 1;
end;
definition
let M be non empty MetrStruct;
let f be Function of TopSpaceMetr M, TopSpaceMetr M;
attr f is isometric means
:Def2:
ex g being isometric Function of M,M st g=f;
end;
registration
let M be non empty MetrStruct;
cluster onto isometric for Function of TopSpaceMetr M, TopSpaceMetr M;
existence
proof
set f = the onto isometric Function of M,M;
reconsider f as Function of TopSpaceMetr M,TopSpaceMetr M;
take f;
thus thesis;
end;
end;
registration
let M be non empty MetrSpace;
cluster isometric -> continuous for
Function of TopSpaceMetr M, TopSpaceMetr M;
coherence
proof
let f be Function of TopSpaceMetr M, TopSpaceMetr M;
assume f is isometric;
then consider g being isometric Function of M,M such that
A1: g=f;
let W be Point of TopSpaceMetr M;
let G be a_neighborhood of f.W;
reconsider fw=f.W,w=W as Point of M;
f.W in Int G by CONNSP_2:def 1;
then consider r being Real such that
A2: r > 0 and
A3: Ball(fw,r) c= G by GOBOARD6:4;
reconsider H=Ball(w,r) as a_neighborhood of W by A2,GOBOARD6:91;
take H;
thus f.:H c= G
proof
let a be object;
assume a in f.:H;
then consider b being object such that
A4: b in dom f and
A5: b in H and
A6: f.b = a by FUNCT_1:def 6;
reconsider b as Point of TopSpaceMetr M by A4;
reconsider b9=b as Point of M;
dist(b9,w) < r by A5,METRIC_1:11;
then dist(g.b9,fw) < r by A1,VECTMETR:def 3;
then a in Ball(fw,r) by A1,A6,METRIC_1:11;
hence thesis by A3;
end;
end;
end;
registration
let M be non empty MetrSpace;
cluster onto isometric -> being_homeomorphism for Function of TopSpaceMetr M,
TopSpaceMetr M;
coherence
proof
let f be Function of TopSpaceMetr M, TopSpaceMetr M;
assume
A1: f is onto isometric;
then reconsider
f1=f as onto isometric Function of TopSpaceMetr M,TopSpaceMetr M;
thus dom f = [#]TopSpaceMetr M by FUNCT_2:def 1;
consider g being isometric Function of M,M such that
A2: g=f by A1;
g is onto by A1,A2;
hence rng f = [#]TopSpaceMetr M by A2;
thus f is one-to-one by A2;
f1 is continuous;
hence f is continuous;
f" is isometric Function of TopSpaceMetr M,TopSpaceMetr M by A1,Def2;
hence thesis;
end;
end;
definition
let a be Real;
func Rotate(a) -> Function of TOP-REAL 2,TOP-REAL 2 means
:Def3:
for p being
Point of TOP-REAL 2 holds it.p = |[Re Rotate(p`1+(p`2)*<i>,a),Im Rotate(p`1+(p
`2)*<i>,a)]|;
existence
proof
deffunc F(Point of TOP-REAL 2) = |[Re Rotate($1`1+($1`2)*<i>,a),Im Rotate(
$1`1+($1`2)*<i>,a)]|;
consider f being Function of TOP-REAL 2,TOP-REAL 2 such that
A1: for p being Point of TOP-REAL 2 holds f.p=F(p) from FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function of TOP-REAL 2,TOP-REAL 2 such that
A2: for p being Point of TOP-REAL 2 holds f.p = |[Re Rotate(p`1+(p`2)*
<i>,a),Im Rotate(p`1+(p`2)*<i>,a)]| and
A3: for p being Point of TOP-REAL 2 holds g.p = |[Re Rotate(p`1+(p`2)*
<i>,a),Im Rotate(p`1+(p`2)*<i>,a)]|;
now
let p be Point of TOP-REAL 2;
thus f.p = |[Re Rotate(p`1+(p`2)*<i>,a),Im Rotate(p`1+(p`2)*<i>,a)]| by
A2
.= g.p by A3;
end;
hence f=g;
end;
end;
Lm2: now
let a be Real;
let c be Complex;
let i be Integer;
cos (a+Arg c) = cos (a+Arg c+2*PI*i) by COMPLEX2:9;
hence Rotate(c,a) = Rotate(c,a+2*PI*i) by COMPLEX2:8;
end;
Lm3: now
let a be Real;
let i be Integer;
thus Rotate(a) = Rotate(a+2*PI*i)
proof
let p be Point of TOP-REAL 2;
set q = p`1+(p`2)*<i>;
A1: Rotate(q,a) = Rotate(q,a+2*PI*i) by Lm2;
thus (Rotate(a)).p = |[Re Rotate(q,a),Im Rotate(q,a)]| by Def3
.= (Rotate(a+2*PI*i)).p by A1,Def3;
end;
end;
theorem Th2:
for a being Real for f being Function of TopSpaceMetr Euclid 2,
TopSpaceMetr Euclid 2 st f = Rotate a holds f is onto isometric
proof
let a be Real;
consider A being Real such that
A1: A = 2*PI*(-[\a/(2*PI)/])+a and
A2: 0 <= A and
A3: A < 2*PI by COMPLEX2:1;
reconsider A as Real;
let f be Function of TopSpaceMetr Euclid 2, TopSpaceMetr Euclid 2 such that
A4: f = Rotate a;
reconsider g=f as Function of Euclid 2,Euclid 2;
A5: Rotate A = Rotate a by A1,Lm3;
g is onto isometric
proof
thus rng g = the carrier of Euclid 2
proof
thus rng g c= the carrier of Euclid 2;
let o be object;
assume o in the carrier of Euclid 2;
then reconsider p=o as Point of TOP-REAL 2 by EUCLID:67;
set pz=p`1+(p`2)*<i>;
reconsider pz as Element of COMPLEX by XCMPLX_0:def 2;
set arg=Arg pz;
per cases;
suppose
A6: pz<>0;
per cases;
suppose
A <= arg;
then
A7: 0<=arg-A by XREAL_1:48;
set qz=Rotate(pz,-A);
A8: |.Rotate(pz,-A).| = |.pz.| by COMPLEX2:53;
arg-A <= arg & arg < 2*PI by A2,COMPTRIG:34,XREAL_1:43;
then
A9: -A+arg < 2*PI by XXREAL_0:2;
qz<>0 by A6,COMPLEX2:52;
then Arg qz = -A+arg by A7,A9,A8,COMPTRIG:def 1;
then
A10: Rotate(qz,A) = pz by A8,COMPTRIG:62;
set q=|[Re qz,Im qz]|;
A11: dom g = the carrier of Euclid 2 by FUNCT_2:def 1;
g.q = |[Re Rotate(q`1+(q`2)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by A4,A5,Def3
.= |[Re Rotate(Re qz+(q`2)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by EUCLID:52
.= |[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by EUCLID:52
.= |[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(Re qz+(q`2)*<i>,A)
]| by EUCLID:52
.=|[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(Re qz+(Im qz)*<i>,A
)]| by EUCLID:52
.= |[Re Rotate(qz,A),Im Rotate(Re qz+(Im qz)*<i>,A)]| by
COMPLEX1:13
.= |[Re pz,Im pz]| by A10,COMPLEX1:13
.= |[p`1,Im pz]| by COMPLEX1:12
.= |[p`1,p`2]| by COMPLEX1:12
.= p by EUCLID:53;
hence thesis by A11,Lm1,FUNCT_1:def 3;
end;
suppose
A > arg;
then arg-A < 0 by XREAL_1:49;
then
A12: 2*PI+(arg-A) < 2*PI by XREAL_1:30;
set qz=Rotate(pz,-A);
set q=|[Re qz,Im qz]|;
A13: dom g = the carrier of Euclid 2 by FUNCT_2:def 1;
A14: |.Rotate(pz,-A).| = |.pz.| by COMPLEX2:53;
then qz= |.qz.|*cos (2*PI*1+(-A+arg))+ |.qz.|*sin (-A+arg) *<i> by
COMPLEX2:9;
then
A15: qz= |.qz.|*cos (2*PI+(arg-A))+ |.qz.|*sin (2*PI*1+(-A+arg)) *
<i> by COMPLEX2:8;
0<= 2*PI-A & arg >= 0 by A3,COMPTRIG:34,XREAL_1:48;
then
A16: 0<=2*PI-A+arg;
qz<>0 by A6,COMPLEX2:52;
then Arg qz = 2*PI+(arg-A) by A16,A12,A15,COMPTRIG:def 1;
then Rotate(qz,A) = |.qz.|*cos arg+ |.qz.|*sin (2*PI*1+arg) *<i> by
COMPLEX2:9;
then Rotate(qz,A) = |.qz.|*cos arg+ |.qz.|*sin arg *<i> by COMPLEX2:8
;
then
A17: Rotate(qz,A) = pz by A14,COMPTRIG:62;
g.q = |[Re Rotate(q`1+(q`2)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by A4,A5,Def3
.= |[Re Rotate(Re qz+(q`2)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by EUCLID:52
.= |[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(q`1+(q`2)*<i>,A)]|
by EUCLID:52
.= |[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(Re qz+(q`2)*<i>,A)
]| by EUCLID:52
.=|[Re Rotate(Re qz+(Im qz)*<i>,A),Im Rotate(Re qz+(Im qz)*<i>,A
)]| by EUCLID:52
.=|[Re Rotate(qz,A),Im Rotate(Re qz+(Im qz)*<i>,A)]| by COMPLEX1:13
.= |[Re pz,Im pz]| by A17,COMPLEX1:13
.= |[p`1,Im pz]| by COMPLEX1:12
.= |[p`1,p`2]| by COMPLEX1:12
.= p by EUCLID:53;
hence thesis by A13,Lm1,FUNCT_1:def 3;
end;
end;
suppose
A18: pz=0;
reconsider z=0 as Element of COMPLEX by XCMPLX_0:def 2;
set q=|[0,0]|;
A19: dom g = the carrier of Euclid 2 by FUNCT_2:def 1;
A20: p`1 = 0 by A18,COMPLEX1:4,12;
g.q = |[Re Rotate(q`1+(q`2)*<i>,a),Im Rotate(q`1+(q`2)*<i>,a)]|
by A4,Def3
.= |[Re Rotate(z+(q`2)*<i>,a),Im Rotate(q`1+(q`2)*<i>,a)]| by
EUCLID:52
.= |[Re Rotate(z+z*<i>,a),Im Rotate(q`1+(q`2)*<i>,a)]| by EUCLID:52
.= |[Re Rotate(z+z*<i>,a),Im Rotate(z+(q`2)*<i>,a)]| by EUCLID:52
.= |[Re Rotate(z,a),Im Rotate(z,a)]| by EUCLID:52
.= |[Re z,Im Rotate(z,a)]| by COMPLEX2:52
.= |[Re z,Im z]| by COMPLEX2:52
.= p by A18,A20,COMPLEX1:4,EUCLID:53;
hence thesis by A19,Lm1,FUNCT_1:def 3;
end;
end;
let X,Y be Point of Euclid 2;
reconsider x=X,y=Y,gx=g.X,gy=g.Y as Point of TOP-REAL 2 by EUCLID:67;
A21: |[Re Rotate((x`1)+(x`2)*<i>,a),Im Rotate((x`1)+(x`2)*<i>,a)]|`1= Re
Rotate((x `1)+(x`2)*<i>,a) & |[Re Rotate((x`1)+(x`2)*<i>,a),Im Rotate((x`1)+(x
`2)*<i>,a) ]|`2= Im Rotate((x`1)+(x`2)*<i>,a) by EUCLID:52;
reconsider xx=x`1+(x`2)*<i>,yy=y`1+(y`2)*<i> as Element of COMPLEX by
XCMPLX_0:def 2;
A22: |[Re Rotate((y`1)+(y`2)*<i>,a),Im Rotate((y`1)+(y`2)*<i>,a)]|`1= Re
Rotate((y `1)+(y`2)*<i>,a) & |[Re Rotate((y`1)+(y`2)*<i>,a),Im Rotate((y`1)+(y
`2)*<i>,a) ]|`2= Im Rotate((y`1)+(y`2)*<i>,a) by EUCLID:52;
A23: Re (y`1+(y`2)*<i>)=y`1 & Im (y`1+(y`2)*<i>)=y`2 by COMPLEX1:12;
A24: (sin a)^2+(cos a)^2 = 1 by SIN_COS:29;
A25: Re (x`1+(x`2)*<i>)=x`1 & Im (x`1+(x`2)*<i>)=x`2 by COMPLEX1:12;
x=|[x`1,x`2]| & y=|[y`1,y`2]| by EUCLID:53;
hence dist(X,Y) = sqrt ((x`1 - y`1)^2 + (x`2 - y`2)^2) by GOBOARD6:6
.= sqrt(((x`1)*(x`1) -2*x`1*y`1 + (y`1)*(y`1))*((sin a)*(sin a)+(cos a
)*(cos a)) + ((x`2)*(x`2) -2*x`2*y`2 + (y`2)*(y`2))*((sin a)^2+(cos a)^2)) by
A24
.= sqrt(((x`1*cos a-x`2*sin a)-(y`1*cos a-y`2*sin a))^2 + ((x`1*sin a+
x`2*cos a)^2-2*(x`1*sin a+x`2*cos a)*(y`1*sin a+y`2*cos a)+ (y`1*sin a+y`2*cos
a)^2))
.= sqrt(((Re Rotate(xx,a))-(y`1*cos a-y`2*sin a))^2 + ((x`1*sin a+x`2*
cos a)-(y`1*sin a+y`2*cos a))^2) by A25,COMPLEX2:56
.= sqrt(((Re Rotate(xx,a))-(y`1*cos a-y`2*sin a))^2 + ((Im Rotate(xx,a
))-(y`1*sin a+y`2*cos a))^2) by A25,COMPLEX2:56
.= sqrt(((Re Rotate(xx,a))-(Re Rotate(yy,a)))^2 + ((Im Rotate(xx,a))-(
y`1*sin a+y`2*cos a))^2) by A23,COMPLEX2:56
.= sqrt(((Re Rotate(xx,a))-(Re Rotate(yy,a)))^2 + ((Im Rotate(xx,a))-(
Im Rotate(yy,a)))^2) by A23,COMPLEX2:56
.= dist(|[Re Rotate((x`1)+(x`2)*<i>,a),Im Rotate((x`1)+(x`2)*<i>,a)]|,
|[Re Rotate((y`1)+(y`2)*<i>,a),Im Rotate((y`1)+(y`2)*<i>,a)]|) by A21,A22,
TOPREAL6:92
.= dist(|[Re Rotate((x`1)+(x`2)*<i>,a),Im Rotate((x`1)+(x`2)*<i>,a)]|,
gy) by A4,Def3
.= dist(gx,gy) by A4,Def3
.= dist(g.X,g.Y) by TOPREAL6:def 1;
end;
hence thesis;
end;
theorem Th3:
for A,B,D being Real st p1,p2 realize-max-dist-in P holds
AffineMap(A,B,A,D).p1,AffineMap(A,B,A,D).p2 realize-max-dist-in AffineMap(A,B,A
,D).:P
proof
let A,B,D be Real;
set a=p1,b=p2,C=P;
A1: dom AffineMap(A,B,A,D) = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
assume
A2: a,b realize-max-dist-in C;
then a in C;
hence AffineMap(A,B,A,D).a in AffineMap(A,B,A,D).:C by A1,FUNCT_1:def 6;
b in C by A2;
hence AffineMap(A,B,A,D).b in AffineMap(A,B,A,D).:C by A1,FUNCT_1:def 6;
let x, y be Point of TOP-REAL 2;
assume x in AffineMap(A,B,A,D).:C;
then consider X being object such that
A3: X in dom AffineMap(A,B,A,D) and
A4: X in C and
A5: AffineMap(A,B,A,D).X=x by FUNCT_1:def 6;
reconsider X as Point of TOP-REAL 2 by A3;
assume y in AffineMap(A,B,A,D).:C;
then consider Y being object such that
A6: Y in dom AffineMap(A,B,A,D) and
A7: Y in C and
A8: AffineMap(A,B,A,D).Y=y by FUNCT_1:def 6;
reconsider Y as Point of TOP-REAL 2 by A6;
A9: (X`1-Y`1)^2>=0 & (X`2-Y`2)^2>=0 by XREAL_1:63;
A10: (a`1-b`1)^2 >=0 & (a`2-b`2)^2 >=0 by XREAL_1:63;
A11: A^2>=0 by XREAL_1:63;
then
A12: sqrt(A^2)>=0 by SQUARE_1:def 2;
A13: dist(AffineMap(A,B,A,D).a,AffineMap(A,B,A,D).b) = dist(|[A*(a`1)+B,A*(a
`2)+D]|,AffineMap(A,B,A,D).b) by JGRAPH_2:def 2
.= dist(|[A*(a`1)+B,A*(a`2)+D]|,|[A*(b`1)+B,A*(b`2)+D]|) by JGRAPH_2:def 2
.= sqrt((|[A*(a`1)+B,A*(a`2)+D]|`1-|[A*(b`1)+B,A*(b`2)+D]|`1)^2 + (|[A*(
a`1)+B,A*(a`2)+D]|`2-|[A*(b`1)+B,A*(b`2)+D]|`2)^2) by TOPREAL6:92
.= sqrt((A*(a`1)+B-|[A*(b`1)+B,A*(b`2)+D]|`1)^2 + (|[A*(a`1)+B,A*(a`2)+D
]|`2-|[A*(b`1)+B,A*(b`2)+D]|`2)^2) by EUCLID:52
.= sqrt((A*(a`1)+B-(A*(b`1)+B))^2 + (|[A*(a`1)+B,A*(a`2)+D]|`2-|[A*(b`1)
+B,A*(b`2)+D]|`2)^2) by EUCLID:52
.= sqrt((A*(a`1)+B-(A*(b`1)+B))^2 + (A*(a`2)+D-|[A*(b`1)+B,A*(b`2)+D]|`2
)^2) by EUCLID:52
.= sqrt((A*(a`1)+B-(A*(b`1)+B))^2 + (A*(a`2)+D-(A*(b`2)+D))^2) by EUCLID:52
.= sqrt(A^2*((a`1-b`1)^2 + (a`2-b`2)^2))
.= sqrt(A^2)*sqrt((a`1-b`1)^2 + (a`2-b`2)^2) by A11,A10,SQUARE_1:29
.= sqrt(A^2)*dist(a,b) by TOPREAL6:92;
A14: dist(x,y) = dist(|[A*(X`1)+B,A*(X`2)+D]|,AffineMap(A,B,A,D).Y) by A5,A8,
JGRAPH_2:def 2
.= dist(|[A*(X`1)+B,A*(X`2)+D]|,|[A*(Y`1)+B,A*(Y`2)+D]|) by JGRAPH_2:def 2
.= sqrt((|[A*(X`1)+B,A*(X`2)+D]|`1-|[A*(Y`1)+B,A*(Y`2)+D]|`1)^2 + (|[A*(
X`1)+B,A*(X`2)+D]|`2-|[A*(Y`1)+B,A*(Y`2)+D]|`2)^2) by TOPREAL6:92
.= sqrt((A*(X`1)+B-|[A*(Y`1)+B,A*(Y`2)+D]|`1)^2 + (|[A*(X`1)+B,A*(X`2)+D
]|`2-|[A*(Y`1)+B,A*(Y`2)+D]|`2)^2) by EUCLID:52
.= sqrt((A*(X`1)+B-(A*(Y`1)+B))^2 + (|[A*(X`1)+B,A*(X`2)+D]|`2-|[A*(Y`1)
+B,A*(Y`2)+D]|`2)^2) by EUCLID:52
.= sqrt((A*(X`1)+B-(A*(Y`1)+B))^2 + (A*(X`2)+D-|[A*(Y`1)+B,A*(Y`2)+D]|`2
)^2) by EUCLID:52
.= sqrt((A*(X`1)+B-(A*(Y`1)+B))^2 + (A*(X`2)+D-(A*(Y`2)+D))^2) by EUCLID:52
.= sqrt(A^2*((X`1-Y`1)^2 + (X`2-Y`2)^2))
.= sqrt(A^2)*sqrt((X`1-Y`1)^2 + (X`2-Y`2)^2) by A11,A9,SQUARE_1:29
.= sqrt(A^2)*dist(X,Y) by TOPREAL6:92;
dist(a,b) >= dist(X,Y) by A2,A4,A7;
hence thesis by A13,A14,A12,XREAL_1:64;
end;
theorem Th4:
for A being Real st p1,p2 realize-max-dist-in P holds (Rotate A).
p1,(Rotate A).p2 realize-max-dist-in (Rotate A).:P
proof
let A be Real;
reconsider f=Rotate A as Function of TopSpaceMetr Euclid 2, TopSpaceMetr
Euclid 2 by Lm1;
set C=P;
A1: dom Rotate A = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
assume
A2: p1,p2 realize-max-dist-in C;
then p1 in C & p2 in C;
hence (Rotate A).p1 in (Rotate A).:C & (Rotate A).p2 in (Rotate A).:C by A1,
FUNCT_1:def 6;
let x, y be Point of TOP-REAL 2 such that
A3: x in (Rotate A).:C and
A4: y in (Rotate A).:C;
f is isometric by Th2;
then consider g being isometric Function of Euclid 2,Euclid 2 such that
A5: f=g;
consider yy being object such that
A6: yy in dom Rotate A and
A7: yy in C and
A8: (Rotate A).yy=y by A4,FUNCT_1:def 6;
reconsider yy as Point of TOP-REAL 2 by A6;
consider xx being object such that
A9: xx in dom Rotate A and
A10: xx in C and
A11: (Rotate A).xx=x by A3,FUNCT_1:def 6;
reconsider xx as Point of TOP-REAL 2 by A9;
reconsider p19=p1,p29=p2,xx9=xx,yy9=yy as Point of Euclid 2 by EUCLID:67;
dist(p1,p2) >= dist(xx,yy) by A2,A10,A7;
then dist(p19,p29) >= dist(xx,yy) by TOPREAL6:def 1;
then dist(p19,p29) >= dist(xx9,yy9) by TOPREAL6:def 1;
then dist(g.p19,g.p29) >= dist(xx9,yy9) by VECTMETR:def 3;
then dist(g.p19,g.p29) >= dist(g.xx9,g.yy9) by VECTMETR:def 3;
then dist((Rotate A).p1,(Rotate A).p2) >= dist(g.xx9,g.yy9) by A5,
TOPREAL6:def 1;
hence thesis by A11,A8,A5,TOPREAL6:def 1;
end;
theorem Th5:
for z being Complex, r being Real holds Rotate(z,-r) =
Rotate(z,2*PI-r)
proof
let z be Complex, r be Real;
thus Rotate(z,-r) = |.z.|*cos (2*PI*1+(-r+Arg z))+ |.z.|*sin (-r+Arg z) *<i>
by COMPLEX2:9
.= Rotate(z,2*PI-r) by COMPLEX2:8;
end;
theorem Th6:
for r being Real holds Rotate(-r) = Rotate(2*PI-r)
proof
let r be Real;
now
let p be Point of TOP-REAL 2;
thus (Rotate(2*PI-r)).p = |[Re Rotate(p`1+(p`2)*<i>,2*PI-r),Im Rotate(p`1+
(p`2)*<i>,2*PI-r)]| by Def3
.= |[Re Rotate(p`1+(p`2)*<i>,-r),Im Rotate(p`1+(p`2)*<i>,2*PI-r)]| by Th5
.= |[Re Rotate(p`1+(p`2)*<i>,-r),Im Rotate(p`1+(p`2)*<i>,-r)]| by Th5;
end;
hence thesis by Def3;
end;
Lm4: for T1,T2 being TopSpace, f being Function of T1,T2, g being Function of
the TopStruct of T1, the TopStruct of T2 st g=f & g is being_homeomorphism
holds f is being_homeomorphism
by PRE_TOPC:34;
theorem
ex f being Homeomorphism of TOP-REAL 2 st |[-1,0]|,|[1,0]|
realize-max-dist-in f.:C
proof
reconsider z=0 as Element of COMPLEX by XCMPLX_0:def 2;
consider x,y being Point of TOP-REAL 2 such that
A1: x<>y and
A2: x in C & y in C by TOPREAL2:4;
A3: dist(x,y) > 0 by A1,JORDAN1K:22;
consider p1,p2 such that
A4: p1,p2 realize-max-dist-in C by Th1;
reconsider g=AffineMap(1,-p1`1,1,-p1`2) as being_homeomorphism Function of
TOP-REAL 2,TOP-REAL 2 by JGRAPH_7:50;
set D=g.:C,q1=g.p1,q2=g.p2;
set arg=Arg(q2`1+q2`2 * <i>);
reconsider qq=q2`1+(q2`2)*<i> as Element of COMPLEX by XCMPLX_0:def 2;
set h=Rotate(-arg);
A5: h=Rotate(2*PI-arg) by Th6;
q1,q2 realize-max-dist-in D by A4,Th3;
then
A6: (Rotate(2*PI-arg)).q1,(Rotate(2*PI-arg)).q2 realize-max-dist-in (Rotate
(2*PI-arg)).:D by Th4;
reconsider h0=h as onto isometric Function of TopSpaceMetr Euclid 2,
TopSpaceMetr Euclid 2 by Lm1,Th2;
A7: Rotate(z,-arg) = 0 by COMPLEX2:52;
h0 is being_homeomorphism;
then reconsider
h as being_homeomorphism Function of TOP-REAL 2,TOP-REAL 2 by Lm1,Lm4;
set F=h.:D,s1=h.q1,s2=h.q2;
q1 = |[1 * (p1`1)+-p1`1,1 * (p1`2)+-p1`2]| by JGRAPH_2:def 2
.= |[0,0]|;
then
A8: s1 = |[Re Rotate(|[0,0]|`1+(|[0,0]|`2)*<i>,-arg), Im Rotate(|[0,0]|`1+(
|[0,0]|`2)*<i>,-arg)]| by Def3
.= |[Re Rotate(0+(|[0,0]|`2) * <i>,-arg), Im Rotate(|[0,0]|`1+(|[0,0]|`2
)*<i>,-arg)]| by EUCLID:52
.= |[Re Rotate(0+0 * <i>,-arg), Im Rotate(|[0,0]|`1+(|[0,0]|`2)*<i>,-arg
)]| by EUCLID:52
.= |[Re Rotate(0+0 * <i>,-arg), Im Rotate(0+(|[0,0]|`2)*<i>,-arg)]| by
EUCLID:52
.= |[0,0]| by A7,COMPLEX1:4,EUCLID:52;
Rotate(qq,-arg) = |.(q2`1+(q2`2)*<i>).|+0 * <i> by COMPLEX2:55;
then
A9: s2 = |[Re (|.(q2`1+(q2`2)*<i>).|+0 *<i>), Im (|.(q2`1+(q2`2)*<i>) .|+0
*<i>)]| by Def3
.= |[|.(q2`1+(q2`2)*<i>).|,Im (|.(q2`1+(q2`2)*<i>).|+0 * <i>)]| by
COMPLEX1:12
.= |[|.(q2`1+(q2`2)*<i>).|,0]| by COMPLEX1:12;
then
A10: s2`2 = 0 by EUCLID:52;
dist(p1,p2)>=dist(x,y) by A4,A2;
then
A11: p1<>p2 by A3,TOPREAL6:93;
A12: now
dom g = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then
A13: q1<>q2 by A11,FUNCT_1:def 4;
assume
A14: s2`1=0;
dom h = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then s1<>s2 by A13,FUNCT_1:def 4;
hence contradiction by A8,A9,A14,EUCLID:52;
end;
s2`1 = |.(q2`1+(q2`2)*<i>).| by A9,EUCLID:52;
then s2`1>=0 by COMPLEX1:46;
then reconsider j=AffineMap(2/(s2`1),-1,2/(s2`1),0) as being_homeomorphism
Function of TOP-REAL 2,TOP-REAL 2 by A12,JGRAPH_7:50;
set E=j.:F,r1=j.s1,r2=j.s2;
A15: r2=|[2/(s2`1)*s2`1+-1,2/(s2`1)*s2`2+0]| by JGRAPH_2:def 2
.=|[2+-1,2/(s2`1)*s2`2+0]| by A12,XCMPLX_1:87
.=b by A10;
set f=j*(h*g);
h*g is being_homeomorphism by TOPS_2:57;
then f is being_homeomorphism by TOPS_2:57;
then reconsider f as Homeomorphism of TOP-REAL 2 by TOPGRP_1:def 4;
take f;
(h*g).:C=F by RELAT_1:126;
then
A16: f.:C=E by RELAT_1:126;
r1=|[2/(s2`1)*s1`1+-1,2/(s2`1)*s1`2+0]| by JGRAPH_2:def 2
.= |[2/(s2`1)*0+-1,2/(s2`1)*s1`2+0]| by A8,EUCLID:52
.= a by A8,EUCLID:52;
hence thesis by A5,A15,A16,A6,Th3;
end;
definition
let T1,T2 be TopStruct;
let f be Function of T1,T2;
attr f is closed means
for A being Subset of T1 st A is closed holds f.:A is closed;
end;
::<DESC name="przekszta/lcenie domkni/ete" monograph="topology"/>
::<DESC name="1.4.18 Twierdzenie o homeomorfizmie (cz/e/s/c): (a) iff (b)" monograph="topology"/>
theorem
for X,Y being non empty TopSpace, f being continuous Function of X,Y
st f is one-to-one onto holds f is being_homeomorphism iff f is closed
proof
let X,Y be non empty TopSpace;
let f be continuous Function of X,Y such that
A1: f is one-to-one onto;
thus f is being_homeomorphism implies f is closed by TOPS_2:58;
assume
A2: for A being Subset of X st A is closed holds f.:A is closed;
A3: [#] X = the carrier of X & [#] Y = the carrier of Y;
A4: dom f = the carrier of X by FUNCT_2:def 1;
A5: now
let A be Subset of X;
assume f.:A is closed;
then f"(f.:A) is closed by PRE_TOPC:def 6;
hence A is closed by A1,A4,FUNCT_1:94;
end;
thus thesis by A1,A2,A4,A3,A5,TOPS_2:58;
end;
theorem Th9:
for X being set, A being Subset of X holds A` = {} iff A = X
by XBOOLE_1:37;
theorem
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st f is
being_homeomorphism for A being Subset of T1 st A is connected holds f.:A is
connected by TOPS_2:61;
theorem Th11:
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st
f is being_homeomorphism for A being Subset of T1 st A is a_component
holds f.:A is a_component
proof
let T1,T2 be non empty TopSpace, f be Function of T1,T2;
assume
A1: f is being_homeomorphism;
let A be Subset of T1;
assume that
A2: A is connected and
A3: for B being Subset of T1 st B is connected holds A c= B implies A = B;
thus f.:A is connected by A1,A2,TOPS_2:61;
let B be Subset of T2;
rng f = the carrier of T2 by A1;
then
A4: f.:(f"B) = B by FUNCT_1:77;
A5: f"(f.:A) = A by A1,FUNCT_1:94;
assume that
A6: B is connected and
A7: f.:A c= B;
f"B is connected by A1,A6,TOPS_2:62;
hence thesis by A3,A4,A5,A7,RELAT_1:143;
end;
theorem Th12:
for T1,T2 being non empty TopSpace, f being Function of T1,T2, A
being Subset of T1 holds f|A is Function of T1|A, T2|(f.:A)
proof
let T1,T2 be non empty TopSpace, f be Function of T1,T2, A be Subset of T1;
A1: rng (f|A) = f.:A by RELAT_1:115;
dom f = the carrier of T1 by FUNCT_2:def 1;
then
A2: dom (f|A) = A by RELAT_1:62;
[#](T1|A) = A & [#](T2|(f.:A)) = f.:A by PRE_TOPC:def 5;
hence thesis by A2,A1,FUNCT_2:2;
end;
theorem Th13:
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st
f is continuous for A being Subset of T1, g being Function of T1|A, T2|(f.:A)
st g = f|A holds g is continuous
proof
let T1,T2 be non empty TopSpace;
let f be Function of T1,T2;
assume
A1: f is continuous;
let A be Subset of T1;
let g be Function of T1|A, T2|(f.:A);
assume
A2: g = f|A;
A3: dom f = the carrier of T1 by FUNCT_2:def 1;
A4: [#](T1|A) = A by PRE_TOPC:def 5;
per cases;
suppose
A is empty;
hence thesis by TIETZE:4;
end;
suppose
A is non empty;
then reconsider S1 = T1|A, S2 = T2|(f.:A) as non empty TopSpace by A3;
f|A = f|(T1|A) by A4,TMAP_1:def 3;
then
A5: g is continuous Function of S1, T2 by A1,A2;
g is Function of S1,S2;
hence thesis by A5,JORDAN16:8;
end;
end;
theorem Th14:
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st
f is being_homeomorphism for A being Subset of T1, g being Function of T1|A, T2
|(f.:A) st g = f|A holds g is being_homeomorphism
proof
let T1,T2 be non empty TopSpace;
let f be Function of T1,T2;
assume that
A1: dom f = [#]T1 and
A2: rng f = [#]T2 and
A3: f is one-to-one and
A4: f is continuous and
A5: f" is continuous;
let A be Subset of T1;
f is onto by A2;
then
A6: f qua Function" = f" by A3,TOPS_2:def 4;
then
A7: f".:(f.:A) = f"(f.:A) by A3,FUNCT_1:85
.= A by A1,A3,FUNCT_1:94;
A8: dom f = the carrier of T1 by FUNCT_2:def 1;
let g be Function of T1|A, T2|(f.:A);
assume
A9: g = f|A;
[#](T1|A) = A & [#](T2|(f.:A)) = f.:A by PRE_TOPC:def 5;
hence
A10: dom g = [#](T1|A) & rng g = [#](T2|(f.:A)) by A9,A8,RELAT_1:62,115;
A11: g is onto by A10;
thus g is one-to-one by A3,A9,FUNCT_1:52;
then
A12: g qua Function" = g" by A11,TOPS_2:def 4;
thus g is continuous by A4,A9,Th13;
g" = f"|(f.:A) by A3,A9,A6,A12,RFUNCT_2:17;
hence thesis by A5,A7,Th13;
end;
theorem Th15:
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st
f is being_homeomorphism for A,B being Subset of T1 st A is_a_component_of B
holds f.:A is_a_component_of f.:B
proof
let T1,T2 be non empty TopSpace, f be Function of T1,T2 such that
A1: f is being_homeomorphism;
let A,B be Subset of T1;
given A1 being Subset of T1|B such that
A2: A1 = A and
A3: A1 is a_component;
A4: [#](T2|(f.:B)) = f.:B by PRE_TOPC:def 5;
A5: dom f = the carrier of T1 by FUNCT_2:def 1;
A6: [#](T1|B) = B by PRE_TOPC:def 5;
then reconsider A2 = f.:A as Subset of T2|(f.:B) by A2,A4,RELAT_1:123;
per cases;
suppose
A7: B is empty;
then f.:B = {};
then
A8: A2 = {} by A4,XBOOLE_1:3;
{} T2 = f.:B by A7;
hence thesis by A8,JORDAN1K:6;
end;
suppose
B is non empty;
then reconsider S1 = T1|B, S2 = T2|(f.:B) as non empty TopSpace by A5;
take A2;
thus A2 = f.:A;
reconsider fB = f|B as Function of S1,S2 by Th12;
fB.:A = A2 by A2,A6,RELAT_1:129;
hence thesis by A1,A2,A3,Th11,Th14;
end;
end;
theorem
for S being Subset of TOP-REAL 2, f being Homeomorphism of TOP-REAL 2
st S is Jordan holds f.:S is Jordan
proof
let S be Subset of TOP-REAL 2, f be Homeomorphism of TOP-REAL 2;
set s = the Element of S`;
assume
A1: S` <> {};
then s in S`;
then reconsider s as Element of TOP-REAL 2;
given A1,A2 being Subset of TOP-REAL 2 such that
A2: S` = A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: A1 is_a_component_of S` & A2 is_a_component_of S`;
A6: not s in S by A1,XBOOLE_0:def 5;
hereby
assume (f.:S)` = {};
then f.:S = the carrier of TOP-REAL 2 by Th9;
then ex s9 being Element of TOP-REAL 2 st s9 in S & f.s = f. s9 by
FUNCT_2:65;
hence contradiction by A6,FUNCT_2:56;
end;
take B1 = f.:A1, B2 = f.:A2;
f.:(A1 \/ A2) = B1 \/ B2 by RELAT_1:120;
hence (f.:S)` = B1 \/ B2 by A2,JORDAN1K:5;
thus B1 misses B2 by A3,FUNCT_1:66;
thus (Cl B1) \ B1 = (f.:Cl A1)\B1 by TOPS_2:60
.= f.:((Cl A2) \ A2) by A4,FUNCT_1:64
.= (f.:Cl A2) \ B2 by FUNCT_1:64
.= (Cl B2) \ B2 by TOPS_2:60;
f.:(S`) = (f.:S)` by JORDAN1K:5;
hence thesis by A5,Th15;
end;