:: by Adam Naumowicz and Grzegorz Bancerek

::

:: Received September 15, 2005

:: Copyright (c) 2005-2016 Association of Mizar Users

definition
end;

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

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

proof end;

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

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 ;

ex b_{1} being Function of (TopSpaceMetr M),(TopSpaceMetr M) st

( b_{1} is onto & b_{1} is isometric )

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

( b

proof end;

registration

let M be non empty MetrSpace;

for b_{1} being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b_{1} is isometric holds

b_{1} is continuous

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

coherence for b

b

proof end;

registration

let M be non empty MetrSpace;

for b_{1} being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b_{1} is onto & b_{1} is isometric holds

b_{1} is being_homeomorphism

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

b

proof end;

definition

let a be Real;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for p being Point of (TOP-REAL 2) holds b_{1} . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]|

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) holds

b_{1} = b_{2}

end;
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) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]|;

existence for p being Point of (TOP-REAL 2) holds it . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]|;

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Rotate JORDAN24:def 3 :

for a being Real

for b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{2} = Rotate a iff for p being Point of (TOP-REAL 2) holds b_{2} . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| );

for a being Real

for b

( b

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

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

Lm3: now :: thesis: for a being Real

for i being Integer holds Rotate a = Rotate (a + ((2 * PI) * i))

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

end;
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 (TOP-REAL 2); :: according to FUNCT_2:def 8 :: thesis: (Rotate a) . 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 (Rotate a) . 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 A1, Def3 ; :: thesis: verum

end;
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 (Rotate a) . 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 A1, Def3 ; :: thesis: verum

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 )

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

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

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;

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;

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

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 )

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 :: JORDAN24:10

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

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

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

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

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

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

for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds

f .: S is Jordan

proof end;

::<DESC name="1.4.18 Twierdzenie o homeomorfizmie (cz/e/s/c): (a) iff (b)" monograph="topology"/>