JORDAN24: Homeomorphisms of {J}ordan Curves

:: Homeomorphisms of {J}ordan Curves
:: by Adam Naumowicz and Grzegorz Bancerek
::
:: Received September 15, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0, FUNCT_2, CONNSP_1, BORSUK_1, VECTMETR, TOPS_2, SPRECT_1;
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;
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;
constructors HIDDEN, 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;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLE_0, COMPLEX2, SQUARE_1, SUBSET_1, PCOMPS_1, STRUCT_0;
expansions XBOOLE_0, FUNCT_2, TOPS_2;

definition

let n be Element of NAT ;
let A be Subset of (TOP-REAL n);
let 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;

:: deftheorem defines realize-max-dist-in JORDAN24:def 1 :

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

proof end;

definition

let M be non empty MetrStruct ;
let f be Function of (TopSpaceMetr M),(TopSpaceMetr M);

attr f 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 :

registration

let M be non empty MetrStruct ;

cluster V1() V4( the carrier of (TopSpaceMetr M)) V5( the carrier of (TopSpaceMetr M)) non empty Function-like V26( the carrier of (TopSpaceMetr M)) quasi_total onto isometric for Element of K16(K17( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M)));

existence

proof end;

end;

registration

let M be non empty MetrSpace;

cluster Function-like quasi_total isometric -> continuous for Element of K16(K17( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M)));

coherence

proof end;

end;

registration

let M be non empty MetrSpace;

cluster Function-like quasi_total onto isometric -> being_homeomorphism for Element of K16(K17( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M)));

coherence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Rotate JORDAN24:def 3 :

Lm2: now :: thesis:

let a be Real; :: thesis:
let c be Complex; :: thesis:
let i be Integer; :: thesis:
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:

end;

Lm3: now :: thesis:

let a be Real; :: thesis:
let i be Integer; :: thesis:
thus Rotate a = Rotate (a + ((2 * PI) * i)) :: thesis:

proof

let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def 8 :: thesis:
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:

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 )

proof end;

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 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 end;

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

proof end;

theorem Th5: :: JORDAN24:5

for z being Complex
for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))

proof end;

theorem Th6: :: JORDAN24:6

for r being Real holds Rotate (- r) = Rotate ((2 * PI) - r)

proof end;

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
by PRE_TOPC:34;

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

proof end;

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;

:: deftheorem defines closed JORDAN24:def 4 :

::<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 :: 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 )

proof end;

theorem Th9: :: JORDAN24:9

for X being set
for A being Subset of X holds
( A ` = {} iff A = X ) by XBOOLE_1:37;

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

proof end;

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))

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;