:: Homeomorphisms of {J}ordan Curves :: by Adam Naumowicz and Grzegorz Bancerek :: :: Received September 15, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin definition let n be Element of NAT ; let A be Subset of (TOP-REAL n); let a, b be Point of (TOP-REAL n); preda,b realize-max-dist-in A means :Def1: :: 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; :: deftheorem Def1 defines realize-max-dist-in JORDAN24:def_1_:_ for n being Element of NAT for A being Subset of (TOP-REAL n) for a, b being Point of (TOP-REAL n) holds ( a,b realize-max-dist-in A iff ( 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) ) ) ); set rl = - 1; set rp = 1; set a = |[(- 1),0]|; set b = |[1,0]|; Lm1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; theorem Th1: :: JORDAN24:1 for C being non empty compact Subset of (TOP-REAL 2) ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C proofend; definition let M be non empty MetrStruct ; let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); attrf is isometric means :Def2: :: JORDAN24:def 2 ex g being isometric Function of M,M st g = f; end; :: deftheorem Def2 defines isometric JORDAN24:def_2_:_ for M being non empty MetrStruct for f being Function of (TopSpaceMetr M),(TopSpaceMetr M) holds ( f is isometric iff ex g being isometric Function of M,M st g = f ); registration let M be non empty MetrStruct ; cluster non empty V16() V19( the carrier of (TopSpaceMetr M)) V20( the carrier of (TopSpaceMetr M)) Function-like V26( the carrier of (TopSpaceMetr M)) quasi_total onto isometric for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); existence ex b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st ( b1 is onto & b1 is isometric ) proofend; end; registration let M be non empty MetrSpace; cluster Function-like quasi_total isometric -> continuous for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); coherence for b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b1 is isometric holds b1 is continuous proofend; end; registration let M be non empty MetrSpace; cluster Function-like quasi_total onto isometric -> being_homeomorphism for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); coherence for b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b1 is onto & b1 is isometric holds b1 is being_homeomorphism proofend; end; definition let a be Real; func Rotate a -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def3: :: 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)))]|; existence ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for p being Point of (TOP-REAL 2) holds b1 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| proofend; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Rotate JORDAN24:def_3_:_ for a being Real for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = Rotate a iff for p being Point of (TOP-REAL 2) holds b2 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ); Lm2: now__::_thesis:_for_a_being_Real for_c_being_complex_number_ for_i_being_integer_number_holds_Rotate_(c,a)_=_Rotate_(c,(a_+_((2_*_PI)_*_i))) let a be Real; ::_thesis: for c being complex number for i being integer number holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) let c be complex number ; ::_thesis: for i being integer number holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) let i be integer number ; ::_thesis: Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) 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; ::_thesis: verum end; Lm3: now__::_thesis:_for_a_being_Real for_i_being_integer_number_holds_Rotate_a_=_Rotate_(a_+_((2_*_PI)_*_i)) let a be Real; ::_thesis: for i being integer number holds Rotate a = Rotate (a + ((2 * PI) * i)) let i be integer number ; ::_thesis: Rotate a = Rotate (a + ((2 * PI) * i)) thus Rotate a = Rotate (a + ((2 * PI) * i)) ::_thesis: verum proof let p be Point of (TOP-REAL 2); :: according toFUNCT_2:def_8 ::_thesis: (Rotate a) . p = (Rotate (a + ((2 * PI) * i))) . p set q = (p `1) + ((p `2) * ); A1: Rotate (((p `1) + ((p `2) * )),a) = Rotate (((p `1) + ((p `2) * )),(a + ((2 * PI) * i))) by Lm2; thus (Rotate a) . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| by Def3 .= (Rotate (a + ((2 * PI) * i))) . p by A1, Def3 ; ::_thesis: verum end; end; theorem Th2: :: 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 & f is isometric ) proofend; theorem Th3: :: JORDAN24:3 for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) for A, B, D being real number 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 proofend; theorem Th4: :: JORDAN24:4 for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) 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 proofend; theorem Th5: :: JORDAN24:5 for z being complex number for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r)) proofend; theorem Th6: :: JORDAN24:6 for r being Real holds Rotate (- r) = Rotate ((2 * PI) - r) proofend; Lm4: for T1, T2 being TopSpace for f being Function of T1,T2 for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds f is being_homeomorphism proofend; theorem :: JORDAN24:7 for C being Simple_closed_curve ex f being Homeomorphism of TOP-REAL 2 st |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C proofend; definition let T1, T2 be TopStruct ; let f be Function of T1,T2; attrf is closed means :: JORDAN24:def 4 for A being Subset of T1 st A is closed holds f .: A is closed ; end; :: deftheorem defines closed JORDAN24:def_4_:_ for T1, T2 being TopStruct for f being Function of T1,T2 holds ( f is closed iff for A being Subset of T1 st A is closed holds f .: A is closed ); :: :: theorem :: JORDAN24:8 for X, Y being non empty TopSpace for f being continuous Function of X,Y st f is one-to-one & f is onto holds ( f is being_homeomorphism iff f is closed ) proofend; theorem Th9: :: JORDAN24:9 for X being set for A being Subset of X holds ( A ` = {} iff A = X ) proofend; theorem :: JORDAN24:10 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 st A is connected holds f .: A is connected by TOPS_2:61; theorem Th11: :: JORDAN24:11 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 st A is a_component holds f .: A is a_component proofend; theorem Th12: :: JORDAN24:12 for T1, T2 being non empty TopSpace for f being Function of T1,T2 for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A)) proofend; theorem Th13: :: JORDAN24:13 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is continuous holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous proofend; theorem Th14: :: JORDAN24:14 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism proofend; theorem Th15: :: JORDAN24:15 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A, B being Subset of T1 st A is_a_component_of B holds f .: A is_a_component_of f .: B proofend; theorem :: JORDAN24:16 for S being Subset of (TOP-REAL 2) for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds f .: S is Jordan proofend;