:: Homeomorphisms of {J}ordan Curves
:: by Adam Naumowicz and Grzegorz Bancerek
::
:: Copyright (c) 2005-2021 Association of Mizar Users

definition
let n be Element of NAT ;
let A be Subset of ();
let a, b be Point of ();
pred a,b realize-max-dist-in A means :: JORDAN24:def 1
( a in A & b in A & ( for x, y being Point of () st x in A & y in A holds
dist (a,b) >= dist (x,y) ) );
end;

:: deftheorem defines realize-max-dist-in JORDAN24:def 1 :
for n being Element of NAT
for A being Subset of ()
for a, b being Point of () holds
( a,b realize-max-dist-in A iff ( a in A & b in A & ( for x, y being Point of () 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 (), the topology of () #) = TopSpaceMetr ()
by EUCLID:def 8;

theorem Th1: :: JORDAN24:1
for C being non empty compact Subset of () ex p1, p2 being Point of () st p1,p2 realize-max-dist-in C
proof end;

definition
let M be non empty MetrStruct ;
let f be Function of (),();
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 :
for M being non empty MetrStruct
for f being Function of (),() holds
( f is isometric iff ex g being isometric Function of M,M st g = f );

registration
let M be non empty MetrStruct ;
cluster V1() V4( the carrier of ()) V5( the carrier of ()) non empty Function-like V26( the carrier of ()) quasi_total onto isometric for Element of K16(K17( the carrier of (), the carrier of ()));
existence
ex b1 being Function of (),() st
( b1 is onto & b1 is isometric )
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 (), the carrier of ()));
coherence
for b1 being Function of (),() st b1 is isometric holds
b1 is continuous
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 (), the carrier of ()));
coherence
for b1 being Function of (),() st b1 is onto & b1 is isometric holds
b1 is being_homeomorphism
proof end;
end;

definition
let a be Real;
func Rotate a -> Function of (),() means :Def3: :: JORDAN24:def 3
for p being Point of () holds it . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]|;
existence
ex b1 being Function of (),() st
for p being Point of () holds b1 . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]|
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for p being Point of () holds b1 . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]| ) & ( for p being Point of () holds b2 . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Rotate JORDAN24:def 3 :
for a being Real
for b2 being Function of (),() holds
( b2 = Rotate a iff for p being Point of () holds b2 . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]| );

Lm2: now :: thesis: for a being Real
for c being Complex
for i being Integer holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i)))
let a be Real; :: thesis: for c being Complex
for i being Integer holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i)))

let c be Complex; :: thesis: for i being Integer holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i)))
let i be Integer; :: 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 holds Rotate a = Rotate (a + ((2 * PI) * i))
let a be Real; :: thesis: for i being Integer holds Rotate a = Rotate (a + ((2 * PI) * i))
let i be Integer; :: thesis: Rotate a = Rotate (a + ((2 * PI) * i))
thus Rotate a = Rotate (a + ((2 * PI) * i)) :: thesis: verum
proof
let p be Point of (); :: according to FUNCT_2:def 8 :: thesis: () . p = (Rotate (a + ((2 * PI) * i))) . p
set q = (p 1) + ((p 2) * <i>);
A1: Rotate (((p 1) + ((p 2) * <i>)),a) = Rotate (((p 1) + ((p 2) * <i>)),(a + ((2 * PI) * i))) by Lm2;
thus () . p = |[(Re (Rotate (((p 1) + ((p 2) * <i>)),a))),(Im (Rotate (((p 1) + ((p 2) * <i>)),a)))]| by Def3
.= (Rotate (a + ((2 * PI) * i))) . p by ; :: thesis: verum
end;
end;

theorem Th2: :: JORDAN24:2
for a being Real
for f being Function of (),() st f = Rotate a holds
( f is onto & f is isometric )
proof end;

theorem Th3: :: JORDAN24:3
for p1, p2 being Point of ()
for P being Subset of ()
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 ()
for P being Subset of ()
for A being Real st p1,p2 realize-max-dist-in P holds
() . p1,() . p2 realize-max-dist-in () .: 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 :
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 );

::<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 ()
for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds
f .: S is Jordan
proof end;