:: Homeomorphisms of {J}ordan Curves
:: by Adam Naumowicz and Grzegorz Bancerek
::
:: Received September 15, 2005
:: Copyright (c) 2005-2018 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;
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
:: JORDAN24:def 1
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;
theorem :: JORDAN24:1
for C being non empty compact Subset of TOP-REAL 2 ex p1,p2 st p1
,p2 realize-max-dist-in C;
definition
let M be non empty MetrStruct;
let f be Function of TopSpaceMetr M, TopSpaceMetr M;
attr f is isometric means
:: JORDAN24:def 2
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;
end;
registration
let M be non empty MetrSpace;
cluster isometric -> continuous for
Function of TopSpaceMetr M, TopSpaceMetr M;
end;
registration
let M be non empty MetrSpace;
cluster onto isometric -> being_homeomorphism for Function of TopSpaceMetr M,
TopSpaceMetr M;
end;
definition
let a be Real;
func Rotate(a) -> Function of TOP-REAL 2,TOP-REAL 2 means
:: JORDAN24:def 3
for p being
Point of TOP-REAL 2 holds it.p = |[Re Rotate(p`1+(p`2)**,a),Im Rotate(p`1+(p
`2)***,a)]|;
end;
theorem :: JORDAN24:2
for a being Real for f being Function of TopSpaceMetr Euclid 2,
TopSpaceMetr Euclid 2 st f = Rotate a holds f is onto isometric;
theorem :: JORDAN24:3
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;
theorem :: JORDAN24:4
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;
theorem :: JORDAN24:5
for z being Complex, r being Real holds Rotate(z,-r) =
Rotate(z,2*PI-r);
theorem :: JORDAN24:6
for r being Real holds Rotate(-r) = Rotate(2*PI-r);
theorem :: JORDAN24:7
ex f being Homeomorphism of TOP-REAL 2 st |[-1,0]|,|[1,0]|
realize-max-dist-in f.:C;
definition
let T1,T2 be TopStruct;
let f be Function of T1,T2;
attr f is closed means
:: JORDAN24:def 4
for A being Subset of T1 st A is closed holds f.:A is closed;
end;
::
::
theorem :: JORDAN24:8
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;
theorem :: JORDAN24:9
for X being set, A being Subset of X holds A` = {} iff A = X;
theorem :: JORDAN24:10
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;
theorem :: JORDAN24:11
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;
theorem :: JORDAN24:12
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);
theorem :: JORDAN24:13
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;
theorem :: JORDAN24:14
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;
theorem :: JORDAN24:15
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;
theorem :: JORDAN24:16
for S being Subset of TOP-REAL 2, f being Homeomorphism of TOP-REAL 2
st S is Jordan holds f.:S is Jordan;
*