:: Homeomorphisms of {J}ordan Curves :: by Adam Naumowicz and Grzegorz Bancerek :: :: Received September 15, 2005 :: Copyright (c) 2005-2021 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;