:: JORDAN24 semantic presentation
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
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C
reconsider D = C as Subset of (TopSpaceMetr (Euclid 2)) by Lm1;
A1: D is compact by Lm1, COMPTS_1:23;
then consider x1, x2 being Point of (Euclid 2) such that
A2: ( x1 in D & x2 in D ) and
A3: dist (x1,x2) = max_dist_max (D,D) by WEIERSTR:33;
reconsider a = x1, b = x2 as Point of (TOP-REAL 2) by EUCLID:67;
take a ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st a,p2 realize-max-dist-in C
take b ; ::_thesis: a,b realize-max-dist-in C
thus ( a in C & b in C ) by A2; :: according to JORDAN24:def_1 ::_thesis: for x, y being Point of (TOP-REAL 2) st x in C & y in C holds
dist (a,b) >= dist (x,y)
let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in C & y in C implies dist (a,b) >= dist (x,y) )
assume A4: ( x in C & y in C ) ; ::_thesis: dist (a,b) >= dist (x,y)
reconsider x9 = x, y9 = y as Point of (Euclid 2) by EUCLID:67;
dist (x9,y9) <= max_dist_max (D,D) by A1, A4, WEIERSTR:34;
then dist (x,y) <= max_dist_max (D,D) by TOPREAL6:def_1;
hence dist (a,b) >= dist (x,y) by A3, TOPREAL6:def_1; ::_thesis: verum
end;
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 )
proof
set f = the onto isometric Function of M,M;
reconsider f = the onto isometric Function of M,M as Function of (TopSpaceMetr M),(TopSpaceMetr M) ;
take f ; ::_thesis: ( f is onto & f is isometric )
thus ( f is onto & f is isometric ) by Def2; ::_thesis: verum
end;
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
proof
let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); ::_thesis: ( f is isometric implies f is continuous )
assume f is isometric ; ::_thesis: f is continuous
then consider g being isometric Function of M,M such that
A1: g = f by Def2;
let W be Point of (TopSpaceMetr M); :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . W ex b2 being a_neighborhood of W st f .: b2 c= b1
let G be a_neighborhood of f . W; ::_thesis: ex b1 being a_neighborhood of W st f .: b1 c= G
reconsider fw = f . W, w = W as Point of M ;
f . W in Int G by CONNSP_2:def_1;
then consider r being real number such that
A2: r > 0 and
A3: Ball (fw,r) c= G by GOBOARD6:4;
reconsider H = Ball (w,r) as a_neighborhood of W by A2, GOBOARD6:91;
take H ; ::_thesis: f .: H c= G
thus f .: H c= G ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in G )
assume a in f .: H ; ::_thesis: a in G
then consider b being set such that
A4: b in dom f and
A5: b in H and
A6: f . b = a by FUNCT_1:def_6;
reconsider b = b as Point of (TopSpaceMetr M) by A4;
reconsider b9 = b as Point of M ;
dist (b9,w) < r by A5, METRIC_1:11;
then dist ((g . b9),fw) < r by A1, VECTMETR:def_3;
then a in Ball (fw,r) by A1, A6, METRIC_1:11;
hence a in G by A3; ::_thesis: verum
end;
end;
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
proof
let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); ::_thesis: ( f is onto & f is isometric implies f is being_homeomorphism )
assume A1: ( f is onto & f is isometric ) ; ::_thesis: f is being_homeomorphism
then reconsider f1 = f as onto isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) ;
thus dom f = [#] (TopSpaceMetr M) by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] (TopSpaceMetr M) & f is one-to-one & f is continuous & f " is continuous )
consider g being isometric Function of M,M such that
A2: g = f by A1, Def2;
g is onto by A1, A2;
hence rng f = [#] (TopSpaceMetr M) by A2, FUNCT_2:def_3; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A2; ::_thesis: ( f is continuous & f " is continuous )
f1 is continuous ;
hence f is continuous ; ::_thesis: f " is continuous
f " is isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A1, A2, Def2;
hence f " is continuous ; ::_thesis: verum
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
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)))]|
proof
deffunc H1( Point of (TOP-REAL 2)) -> Element of the carrier of (TOP-REAL 2) = |[(Re (Rotate ((($1 `1) + (($1 `2) * **)),a))),(Im (Rotate ((($1 `1) + (($1 `2) * **)),a)))]|;
consider f being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A1: for p being Point of (TOP-REAL 2) holds f . p = H1(p) from FUNCT_2:sch_4();
take f ; ::_thesis: for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]|
thus for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| by A1; ::_thesis: verum
end;
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
proof
let f, g be Function of (TOP-REAL 2),(TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| ) implies f = g )
assume that
A2: for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| and
A3: for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| ; ::_thesis: f = g
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_f_._p_=_g_._p
let p be Point of (TOP-REAL 2); ::_thesis: f . p = g . p
thus f . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),a))),(Im (Rotate (((p `1) + ((p `2) * **)),a)))]| by A2
.= g . p by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
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 to FUNCT_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 )
proof
let a be Real; ::_thesis: for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds
( f is onto & f is isometric )
consider A being real number such that
A1: A = ((2 * PI) * (- [\(a / (2 * PI))/])) + a and
A2: 0 <= A and
A3: A < 2 * PI by COMPLEX2:1;
reconsider A = A as Real by XREAL_0:def_1;
let f be Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)); ::_thesis: ( f = Rotate a implies ( f is onto & f is isometric ) )
assume A4: f = Rotate a ; ::_thesis: ( f is onto & f is isometric )
reconsider g = f as Function of (Euclid 2),(Euclid 2) ;
A5: Rotate A = Rotate a by A1, Lm3;
( g is onto & g is isometric )
proof
thus rng g = the carrier of (Euclid 2) :: according to FUNCT_2:def_3 ::_thesis: g is isometric
proof
thus rng g c= the carrier of (Euclid 2) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Euclid 2) c= rng g
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in the carrier of (Euclid 2) or o in rng g )
assume o in the carrier of (Euclid 2) ; ::_thesis: o in rng g
then reconsider p = o as Point of (TOP-REAL 2) by EUCLID:67;
set pz = (p `1) + ((p `2) * **);
reconsider pz = (p `1) + ((p `2) * **) as Element of COMPLEX by XCMPLX_0:def_2;
set arg = Arg pz;
percases ( pz <> 0 or pz = 0 ) ;
supposeA6: pz <> 0 ; ::_thesis: o in rng g
percases ( A <= Arg pz or A > Arg pz ) ;
suppose A <= Arg pz ; ::_thesis: o in rng g
then A7: 0 <= (Arg pz) - A by XREAL_1:48;
set qz = Rotate (pz,(- A));
A8: |.(Rotate (pz,(- A))).| = |.pz.| by COMPLEX2:53;
( (Arg pz) - A <= Arg pz & Arg pz < 2 * PI ) by A2, COMPTRIG:34, XREAL_1:43;
then A9: (- A) + (Arg pz) < 2 * PI by XXREAL_0:2;
Rotate (pz,(- A)) <> 0 by A6, COMPLEX2:52;
then Arg (Rotate (pz,(- A))) = (- A) + (Arg pz) by A7, A9, A8, COMPTRIG:def_1;
then A10: Rotate ((Rotate (pz,(- A))),A) = pz by A8, COMPLEX2:12;
set q = |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]|;
A11: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1;
g . |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| = |[(Re (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by A4, A5, Def3
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A)))]| by COMPLEX1:13
.= |[(Re pz),(Im pz)]| by A10, COMPLEX1:13
.= |[(p `1),(Im pz)]| by COMPLEX1:12
.= |[(p `1),(p `2)]| by COMPLEX1:12
.= p by EUCLID:53 ;
hence o in rng g by A11, Lm1, FUNCT_1:def_3; ::_thesis: verum
end;
suppose A > Arg pz ; ::_thesis: o in rng g
then (Arg pz) - A < 0 by XREAL_1:49;
then A12: (2 * PI) + ((Arg pz) - A) < 2 * PI by XREAL_1:30;
set qz = Rotate (pz,(- A));
set q = |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]|;
A13: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1;
A14: |.(Rotate (pz,(- A))).| = |.pz.| by COMPLEX2:53;
then Rotate (pz,(- A)) = (|.(Rotate (pz,(- A))).| * (cos (((2 * PI) * 1) + ((- A) + (Arg pz))))) + ((|.(Rotate (pz,(- A))).| * (sin ((- A) + (Arg pz)))) * **) by COMPLEX2:9;
then A15: Rotate (pz,(- A)) = (|.(Rotate (pz,(- A))).| * (cos ((2 * PI) + ((Arg pz) - A)))) + ((|.(Rotate (pz,(- A))).| * (sin (((2 * PI) * 1) + ((- A) + (Arg pz))))) * **) by COMPLEX2:8;
( 0 <= (2 * PI) - A & Arg pz >= 0 ) by A3, COMPTRIG:34, XREAL_1:48;
then A16: 0 <= ((2 * PI) - A) + (Arg pz) ;
Rotate (pz,(- A)) <> 0 by A6, COMPLEX2:52;
then Arg (Rotate (pz,(- A))) = (2 * PI) + ((Arg pz) - A) by A16, A12, A15, COMPTRIG:def_1;
then Rotate ((Rotate (pz,(- A))),A) = (|.(Rotate (pz,(- A))).| * (cos (Arg pz))) + ((|.(Rotate (pz,(- A))).| * (sin (((2 * PI) * 1) + (Arg pz)))) * **) by COMPLEX2:9;
then Rotate ((Rotate (pz,(- A))),A) = (|.(Rotate (pz,(- A))).| * (cos (Arg pz))) + ((|.(Rotate (pz,(- A))).| * (sin (Arg pz))) * **) by COMPLEX2:8;
then A17: Rotate ((Rotate (pz,(- A))),A) = pz by A14, COMPLEX2:12;
g . |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| = |[(Re (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by A4, A5, Def3
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A)))]| by EUCLID:52
.= |[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * **)),A)))]| by COMPLEX1:13
.= |[(Re pz),(Im pz)]| by A17, COMPLEX1:13
.= |[(p `1),(Im pz)]| by COMPLEX1:12
.= |[(p `1),(p `2)]| by COMPLEX1:12
.= p by EUCLID:53 ;
hence o in rng g by A13, Lm1, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
supposeA18: pz = 0 ; ::_thesis: o in rng g
reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def_2;
set q = |[0,0]|;
A19: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1;
A20: p `1 = 0 by A18, COMPLEX1:4, COMPLEX1:12;
g . |[0,0]| = |[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),a)))]| by A4, Def3
.= |[(Re (Rotate ((z + ((|[0,0]| `2) * **)),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),a)))]| by EUCLID:52
.= |[(Re (Rotate ((z + (z * **)),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),a)))]| by EUCLID:52
.= |[(Re (Rotate ((z + (z * **)),a))),(Im (Rotate ((z + ((|[0,0]| `2) * **)),a)))]| by EUCLID:52
.= |[(Re (Rotate (z,a))),(Im (Rotate (z,a)))]| by EUCLID:52
.= |[(Re z),(Im (Rotate (z,a)))]| by COMPLEX2:52
.= |[(Re z),(Im z)]| by COMPLEX2:52
.= p by A18, A20, COMPLEX1:4, EUCLID:53 ;
hence o in rng g by A19, Lm1, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
let X, Y be Point of (Euclid 2); :: according to VECTMETR:def_3 ::_thesis: dist (X,Y) = dist ((g . X),(g . Y))
reconsider x = X, y = Y, gx = g . X, gy = g . Y as Point of (TOP-REAL 2) by EUCLID:67;
A21: ( |[(Re (Rotate (((x `1) + ((x `2) * **)),a))),(Im (Rotate (((x `1) + ((x `2) * **)),a)))]| `1 = Re (Rotate (((x `1) + ((x `2) * **)),a)) & |[(Re (Rotate (((x `1) + ((x `2) * **)),a))),(Im (Rotate (((x `1) + ((x `2) * **)),a)))]| `2 = Im (Rotate (((x `1) + ((x `2) * **)),a)) ) by EUCLID:52;
reconsider xx = (x `1) + ((x `2) * **), yy = (y `1) + ((y `2) * **) as Element of COMPLEX by XCMPLX_0:def_2;
A22: ( |[(Re (Rotate (((y `1) + ((y `2) * **)),a))),(Im (Rotate (((y `1) + ((y `2) * **)),a)))]| `1 = Re (Rotate (((y `1) + ((y `2) * **)),a)) & |[(Re (Rotate (((y `1) + ((y `2) * **)),a))),(Im (Rotate (((y `1) + ((y `2) * **)),a)))]| `2 = Im (Rotate (((y `1) + ((y `2) * **)),a)) ) by EUCLID:52;
A23: ( Re ((y `1) + ((y `2) * **)) = y `1 & Im ((y `1) + ((y `2) * **)) = y `2 ) by COMPLEX1:12;
A24: ((sin a) ^2) + ((cos a) ^2) = 1 by SIN_COS:29;
A25: ( Re ((x `1) + ((x `2) * **)) = x `1 & Im ((x `1) + ((x `2) * **)) = x `2 ) by COMPLEX1:12;
( x = |[(x `1),(x `2)]| & y = |[(y `1),(y `2)]| ) by EUCLID:53;
hence dist (X,Y) = sqrt ((((x `1) - (y `1)) ^2) + (((x `2) - (y `2)) ^2)) by GOBOARD6:6
.= sqrt ((((((x `1) * (x `1)) - ((2 * (x `1)) * (y `1))) + ((y `1) * (y `1))) * (((sin a) * (sin a)) + ((cos a) * (cos a)))) + (((((x `2) * (x `2)) - ((2 * (x `2)) * (y `2))) + ((y `2) * (y `2))) * (((sin a) ^2) + ((cos a) ^2)))) by A24
.= sqrt ((((((x `1) * (cos a)) - ((x `2) * (sin a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + ((((((x `1) * (sin a)) + ((x `2) * (cos a))) ^2) - ((2 * (((x `1) * (sin a)) + ((x `2) * (cos a)))) * (((y `1) * (sin a)) + ((y `2) * (cos a))))) + ((((y `1) * (sin a)) + ((y `2) * (cos a))) ^2)))
.= sqrt ((((Re (Rotate (xx,a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + (((((x `1) * (sin a)) + ((x `2) * (cos a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A25, COMPLEX2:56
.= sqrt ((((Re (Rotate (xx,a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + (((Im (Rotate (xx,a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A25, COMPLEX2:56
.= sqrt ((((Re (Rotate (xx,a))) - (Re (Rotate (yy,a)))) ^2) + (((Im (Rotate (xx,a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A23, COMPLEX2:56
.= sqrt ((((Re (Rotate (xx,a))) - (Re (Rotate (yy,a)))) ^2) + (((Im (Rotate (xx,a))) - (Im (Rotate (yy,a)))) ^2)) by A23, COMPLEX2:56
.= dist (|[(Re (Rotate (((x `1) + ((x `2) * **)),a))),(Im (Rotate (((x `1) + ((x `2) * **)),a)))]|,|[(Re (Rotate (((y `1) + ((y `2) * **)),a))),(Im (Rotate (((y `1) + ((y `2) * **)),a)))]|) by A21, A22, TOPREAL6:92
.= dist (|[(Re (Rotate (((x `1) + ((x `2) * **)),a))),(Im (Rotate (((x `1) + ((x `2) * **)),a)))]|,gy) by A4, Def3
.= dist (gx,gy) by A4, Def3
.= dist ((g . X),(g . Y)) by TOPREAL6:def_1 ;
::_thesis: verum
end;
hence ( f is onto & f is isometric ) by Def2; ::_thesis: verum
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 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
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: 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
let P be Subset of (TOP-REAL 2); ::_thesis: 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
let A, B, D be real number ; ::_thesis: ( p1,p2 realize-max-dist-in P implies (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P )
set a = p1;
set b = p2;
set C = P;
A1: dom (AffineMap (A,B,A,D)) = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
assume A2: p1,p2 realize-max-dist-in P ; ::_thesis: (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P
then p1 in P by Def1;
hence (AffineMap (A,B,A,D)) . p1 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def_6; :: according to JORDAN24:def_1 ::_thesis: ( (AffineMap (A,B,A,D)) . p2 in (AffineMap (A,B,A,D)) .: P & ( for x, y being Point of (TOP-REAL 2) st x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P holds
dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) ) )
p2 in P by A2, Def1;
hence (AffineMap (A,B,A,D)) . p2 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def_6; ::_thesis: for x, y being Point of (TOP-REAL 2) st x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P holds
dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y)
let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P implies dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) )
assume x in (AffineMap (A,B,A,D)) .: P ; ::_thesis: ( not y in (AffineMap (A,B,A,D)) .: P or dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) )
then consider X being set such that
A3: X in dom (AffineMap (A,B,A,D)) and
A4: X in P and
A5: (AffineMap (A,B,A,D)) . X = x by FUNCT_1:def_6;
reconsider X = X as Point of (TOP-REAL 2) by A3;
assume y in (AffineMap (A,B,A,D)) .: P ; ::_thesis: dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y)
then consider Y being set such that
A6: Y in dom (AffineMap (A,B,A,D)) and
A7: Y in P and
A8: (AffineMap (A,B,A,D)) . Y = y by FUNCT_1:def_6;
reconsider Y = Y as Point of (TOP-REAL 2) by A6;
A9: ( ((X `1) - (Y `1)) ^2 >= 0 & ((X `2) - (Y `2)) ^2 >= 0 ) by XREAL_1:63;
A10: ( ((p1 `1) - (p2 `1)) ^2 >= 0 & ((p1 `2) - (p2 `2)) ^2 >= 0 ) by XREAL_1:63;
A11: A ^2 >= 0 by XREAL_1:63;
then A12: sqrt (A ^2) >= 0 by SQUARE_1:def_2;
A13: dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) = dist (|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]|,((AffineMap (A,B,A,D)) . p2)) by JGRAPH_2:def_2
.= dist (|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]|,|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]|) by JGRAPH_2:def_2
.= sqrt ((((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `1) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `1)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by TOPREAL6:92
.= sqrt (((((A * (p1 `1)) + B) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `1)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + ((((A * (p1 `2)) + D) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + ((((A * (p1 `2)) + D) - ((A * (p2 `2)) + D)) ^2)) by EUCLID:52
.= sqrt ((A ^2) * ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)))
.= (sqrt (A ^2)) * (sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))) by A11, A10, SQUARE_1:29
.= (sqrt (A ^2)) * (dist (p1,p2)) by TOPREAL6:92 ;
A14: dist (x,y) = dist (|[((A * (X `1)) + B),((A * (X `2)) + D)]|,((AffineMap (A,B,A,D)) . Y)) by A5, A8, JGRAPH_2:def_2
.= dist (|[((A * (X `1)) + B),((A * (X `2)) + D)]|,|[((A * (Y `1)) + B),((A * (Y `2)) + D)]|) by JGRAPH_2:def_2
.= sqrt ((((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `1) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `1)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by TOPREAL6:92
.= sqrt (((((A * (X `1)) + B) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `1)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + ((((A * (X `2)) + D) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52
.= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + ((((A * (X `2)) + D) - ((A * (Y `2)) + D)) ^2)) by EUCLID:52
.= sqrt ((A ^2) * ((((X `1) - (Y `1)) ^2) + (((X `2) - (Y `2)) ^2)))
.= (sqrt (A ^2)) * (sqrt ((((X `1) - (Y `1)) ^2) + (((X `2) - (Y `2)) ^2))) by A11, A9, SQUARE_1:29
.= (sqrt (A ^2)) * (dist (X,Y)) by TOPREAL6:92 ;
dist (p1,p2) >= dist (X,Y) by A2, A4, A7, Def1;
hence dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) by A13, A14, A12, XREAL_1:64; ::_thesis: verum
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
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: 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
let P be Subset of (TOP-REAL 2); ::_thesis: 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
let A be Real; ::_thesis: ( p1,p2 realize-max-dist-in P implies (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P )
reconsider f = Rotate A as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1;
set C = P;
A1: dom (Rotate A) = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
assume A2: p1,p2 realize-max-dist-in P ; ::_thesis: (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
then ( p1 in P & p2 in P ) by Def1;
hence ( (Rotate A) . p1 in (Rotate A) .: P & (Rotate A) . p2 in (Rotate A) .: P ) by A1, FUNCT_1:def_6; :: according to JORDAN24:def_1 ::_thesis: for x, y being Point of (TOP-REAL 2) st x in (Rotate A) .: P & y in (Rotate A) .: P holds
dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y)
let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in (Rotate A) .: P & y in (Rotate A) .: P implies dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) )
assume that
A3: x in (Rotate A) .: P and
A4: y in (Rotate A) .: P ; ::_thesis: dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y)
f is isometric by Th2;
then consider g being isometric Function of (Euclid 2),(Euclid 2) such that
A5: f = g by Def2;
consider yy being set such that
A6: yy in dom (Rotate A) and
A7: yy in P and
A8: (Rotate A) . yy = y by A4, FUNCT_1:def_6;
reconsider yy = yy as Point of (TOP-REAL 2) by A6;
consider xx being set such that
A9: xx in dom (Rotate A) and
A10: xx in P and
A11: (Rotate A) . xx = x by A3, FUNCT_1:def_6;
reconsider xx = xx as Point of (TOP-REAL 2) by A9;
reconsider p19 = p1, p29 = p2, xx9 = xx, yy9 = yy as Point of (Euclid 2) by EUCLID:67;
dist (p1,p2) >= dist (xx,yy) by A2, A10, A7, Def1;
then dist (p19,p29) >= dist (xx,yy) by TOPREAL6:def_1;
then dist (p19,p29) >= dist (xx9,yy9) by TOPREAL6:def_1;
then dist ((g . p19),(g . p29)) >= dist (xx9,yy9) by VECTMETR:def_3;
then dist ((g . p19),(g . p29)) >= dist ((g . xx9),(g . yy9)) by VECTMETR:def_3;
then dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist ((g . xx9),(g . yy9)) by A5, TOPREAL6:def_1;
hence dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) by A11, A8, A5, TOPREAL6:def_1; ::_thesis: verum
end;
theorem Th5: :: JORDAN24:5
for z being complex number
for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))
proof
let z be complex number ; ::_thesis: for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))
let r be Real; ::_thesis: Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))
thus Rotate (z,(- r)) = (|.z.| * (cos (((2 * PI) * 1) + ((- r) + (Arg z))))) + ((|.z.| * (sin ((- r) + (Arg z)))) * **) by COMPLEX2:9
.= Rotate (z,((2 * PI) - r)) by COMPLEX2:8 ; ::_thesis: verum
end;
theorem Th6: :: JORDAN24:6
for r being Real holds Rotate (- r) = Rotate ((2 * PI) - r)
proof
let r be Real; ::_thesis: Rotate (- r) = Rotate ((2 * PI) - r)
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_(Rotate_((2_*_PI)_-_r))_._p_=_|[(Re_(Rotate_(((p_`1)_+_((p_`2)_*_**)),(-_r)))),(Im_(Rotate_(((p_`1)_+_((p_`2)_*_**)),(-_r))))]|
let p be Point of (TOP-REAL 2); ::_thesis: (Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * **)),(- r))))]|
thus (Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),((2 * PI) - r)))),(Im (Rotate (((p `1) + ((p `2) * **)),((2 * PI) - r))))]| by Def3
.= |[(Re (Rotate (((p `1) + ((p `2) * **)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * **)),((2 * PI) - r))))]| by Th5
.= |[(Re (Rotate (((p `1) + ((p `2) * **)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * **)),(- r))))]| by Th5 ; ::_thesis: verum
end;
hence Rotate (- r) = Rotate ((2 * PI) - r) by Def3; ::_thesis: verum
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
proof
let T1, T2 be TopSpace; ::_thesis: 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
let f be Function of T1,T2; ::_thesis: 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
let g be Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #); ::_thesis: ( g = f & g is being_homeomorphism implies f is being_homeomorphism )
assume that
A1: g = f and
A2: g is being_homeomorphism ; ::_thesis: f is being_homeomorphism
( dom f = [#] TopStruct(# the carrier of T1, the topology of T1 #) & rng f = [#] TopStruct(# the carrier of T2, the topology of T2 #) ) by A1, A2, TOPS_2:def_5;
hence ( dom f = [#] T1 & rng f = [#] T2 ) ; :: according to TOPS_2:def_5 ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1, A2; ::_thesis: ( f is continuous & f " is continuous )
thus f is continuous by A1, A2, PRE_TOPC:34; ::_thesis: f " is continuous
g " is continuous by A2, TOPS_2:def_5;
hence f " is continuous by A1, PRE_TOPC:34; ::_thesis: verum
end;
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
let C be Simple_closed_curve; ::_thesis: ex f being Homeomorphism of TOP-REAL 2 st |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C
reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def_2;
consider x, y being Point of (TOP-REAL 2) such that
A1: x <> y and
A2: ( x in C & y in C ) by TOPREAL2:4;
A3: dist (x,y) > 0 by A1, JORDAN1K:22;
consider p1, p2 being Point of (TOP-REAL 2) such that
A4: p1,p2 realize-max-dist-in C by Th1;
reconsider g = AffineMap (1,(- (p1 `1)),1,(- (p1 `2))) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by JGRAPH_7:50;
set D = g .: C;
set q1 = g . p1;
set q2 = g . p2;
set arg = Arg (((g . p2) `1) + (((g . p2) `2) * **));
reconsider qq = ((g . p2) `1) + (((g . p2) `2) * **) as Element of COMPLEX by XCMPLX_0:def_2;
set h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * **))));
A5: Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))) = Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * **)))) by Th6;
g . p1,g . p2 realize-max-dist-in g .: C by A4, Th3;
then A6: (Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * **))))) . (g . p1),(Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * **))))) . (g . p2) realize-max-dist-in (Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * **))))) .: (g .: C) by Th4;
reconsider h0 = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))) as onto isometric Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1, Th2;
A7: Rotate (z,(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))) = 0 by COMPLEX2:52;
h0 is being_homeomorphism ;
then reconsider h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by Lm1, Lm4;
set F = h .: (g .: C);
set s1 = h . (g . p1);
set s2 = h . (g . p2);
g . p1 = |[((1 * (p1 `1)) + (- (p1 `1))),((1 * (p1 `2)) + (- (p1 `2)))]| by JGRAPH_2:def_2
.= |[0,0]| ;
then A8: h . (g . p1) = |[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))))))]| by Def3
.= |[(Re (Rotate ((0 + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))))))]| by EUCLID:52
.= |[(Re (Rotate ((0 + (0 * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))))))]| by EUCLID:52
.= |[(Re (Rotate ((0 + (0 * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))))),(Im (Rotate ((0 + ((|[0,0]| `2) * **)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * **)))))))]| by EUCLID:52
.= |[0,0]| by A7, COMPLEX1:4, EUCLID:52 ;
Rotate (qq,(- (Arg (((g . p2) `1) + (((g . p2) `2) * **))))) = |.(((g . p2) `1) + (((g . p2) `2) * **)).| + (0 * **) by COMPLEX2:55;
then A9: h . (g . p2) = |[(Re (|.(((g . p2) `1) + (((g . p2) `2) * **)).| + (0 * **))),(Im (|.(((g . p2) `1) + (((g . p2) `2) * **)).| + (0 * **)))]| by Def3
.= |[|.(((g . p2) `1) + (((g . p2) `2) * **)).|,(Im (|.(((g . p2) `1) + (((g . p2) `2) * **)).| + (0 * **)))]| by COMPLEX1:12
.= |[|.(((g . p2) `1) + (((g . p2) `2) * **)).|,0]| by COMPLEX1:12 ;
then A10: (h . (g . p2)) `2 = 0 by EUCLID:52;
dist (p1,p2) >= dist (x,y) by A4, A2, Def1;
then A11: p1 <> p2 by A3, TOPREAL6:93;
A12: now__::_thesis:_not_(h_._(g_._p2))_`1_=_0
dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
then A13: g . p1 <> g . p2 by A11, FUNCT_1:def_4;
assume A14: (h . (g . p2)) `1 = 0 ; ::_thesis: contradiction
dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
then h . (g . p1) <> h . (g . p2) by A13, FUNCT_1:def_4;
hence contradiction by A8, A9, A14, EUCLID:52; ::_thesis: verum
end;
(h . (g . p2)) `1 = |.(((g . p2) `1) + (((g . p2) `2) * **)).| by A9, EUCLID:52;
then (h . (g . p2)) `1 >= 0 by COMPLEX1:46;
then reconsider j = AffineMap ((2 / ((h . (g . p2)) `1)),(- 1),(2 / ((h . (g . p2)) `1)),0) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by A12, JGRAPH_7:50;
set E = j .: (h .: (g .: C));
set r1 = j . (h . (g . p1));
set r2 = j . (h . (g . p2));
A15: j . (h . (g . p2)) = |[(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `1)) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `2)) + 0)]| by JGRAPH_2:def_2
.= |[(2 + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `2)) + 0)]| by A12, XCMPLX_1:87
.= |[1,0]| by A10 ;
set f = j * (h * g);
h * g is being_homeomorphism by TOPS_2:57;
then j * (h * g) is being_homeomorphism by TOPS_2:57;
then reconsider f = j * (h * g) as Homeomorphism of TOP-REAL 2 by TOPGRP_1:def_4;
take f ; ::_thesis: |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C
(h * g) .: C = h .: (g .: C) by RELAT_1:126;
then A16: f .: C = j .: (h .: (g .: C)) by RELAT_1:126;
j . (h . (g . p1)) = |[(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `1)) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `2)) + 0)]| by JGRAPH_2:def_2
.= |[(((2 / ((h . (g . p2)) `1)) * 0) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `2)) + 0)]| by A8, EUCLID:52
.= |[(- 1),0]| by A8, EUCLID:52 ;
hence |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C by A5, A15, A16, A6, Th3; ::_thesis: verum
end;
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 )
proof
let X, Y be non empty TopSpace; ::_thesis: 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 )
let f be continuous Function of X,Y; ::_thesis: ( f is one-to-one & f is onto implies ( f is being_homeomorphism iff f is closed ) )
assume A1: ( f is one-to-one & f is onto ) ; ::_thesis: ( f is being_homeomorphism iff f is closed )
hereby ::_thesis: ( f is closed implies f is being_homeomorphism )
assume A2: f is being_homeomorphism ; ::_thesis: f is closed
thus f is closed ::_thesis: verum
proof
let A be Subset of X; :: according to JORDAN24:def_4 ::_thesis: ( A is closed implies f .: A is closed )
thus ( A is closed implies f .: A is closed ) by A2, TOPS_2:58; ::_thesis: verum
end;
end;
assume A3: for A being Subset of X st A is closed holds
f .: A is closed ; :: according to JORDAN24:def_4 ::_thesis: f is being_homeomorphism
A4: ( [#] X = the carrier of X & [#] Y = the carrier of Y ) ;
A5: dom f = the carrier of X by FUNCT_2:def_1;
A6: now__::_thesis:_for_A_being_Subset_of_X_st_f_.:_A_is_closed_holds_
A_is_closed
let A be Subset of X; ::_thesis: ( f .: A is closed implies A is closed )
assume f .: A is closed ; ::_thesis: A is closed
then f " (f .: A) is closed by PRE_TOPC:def_6;
hence A is closed by A1, A5, FUNCT_1:94; ::_thesis: verum
end;
rng f = the carrier of Y by A1, FUNCT_2:def_3;
hence f is being_homeomorphism by A1, A3, A5, A4, A6, TOPS_2:58; ::_thesis: verum
end;
theorem Th9: :: JORDAN24:9
for X being set
for A being Subset of X holds
( A ` = {} iff A = X )
proof
let X be set ; ::_thesis: for A being Subset of X holds
( A ` = {} iff A = X )
let A be Subset of X; ::_thesis: ( A ` = {} iff A = X )
(A `) ` = A ;
hence ( A ` = {} iff A = X ) by XBOOLE_1:37; ::_thesis: verum
end;
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
let T1, T2 be non empty TopSpace; ::_thesis: 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
let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for A being Subset of T1 st A is a_component holds
f .: A is a_component )
assume A1: f is being_homeomorphism ; ::_thesis: for A being Subset of T1 st A is a_component holds
f .: A is a_component
let A be Subset of T1; ::_thesis: ( A is a_component implies f .: A is a_component )
assume that
A2: A is connected and
A3: for B being Subset of T1 st B is connected & A c= B holds
A = B ; :: according to CONNSP_1:def_5 ::_thesis: f .: A is a_component
thus f .: A is connected by A1, A2, TOPS_2:61; :: according to CONNSP_1:def_5 ::_thesis: for b1 being Element of K6( the carrier of T2) holds
( not b1 is connected or not f .: A c= b1 or f .: A = b1 )
let B be Subset of T2; ::_thesis: ( not B is connected or not f .: A c= B or f .: A = B )
[#] T2 = the carrier of T2 ;
then rng f = the carrier of T2 by A1, TOPS_2:def_5;
then A4: f .: (f " B) = B by FUNCT_1:77;
dom f = the carrier of T1 by FUNCT_2:def_1;
then A5: f " (f .: A) = A by A1, FUNCT_1:94;
assume that
A6: B is connected and
A7: f .: A c= B ; ::_thesis: f .: A = B
f " B is connected by A1, A6, TOPS_2:62;
hence f .: A = B by A3, A4, A5, A7, RELAT_1:143; ::_thesis: verum
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
let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2
for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A))
let f be Function of T1,T2; ::_thesis: for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A))
let A be Subset of T1; ::_thesis: f | A is Function of (T1 | A),(T2 | (f .: A))
A1: rng (f | A) = f .: A by RELAT_1:115;
dom f = the carrier of T1 by FUNCT_2:def_1;
then A2: dom (f | A) = A by RELAT_1:62;
( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def_5;
hence f | A is Function of (T1 | A),(T2 | (f .: A)) by A2, A1, FUNCT_2:2; ::_thesis: verum
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
let T1, T2 be non empty TopSpace; ::_thesis: 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
let f be Function of T1,T2; ::_thesis: ( f is continuous implies for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous )
assume A1: f is continuous ; ::_thesis: for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous
let A be Subset of T1; ::_thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous
let g be Function of (T1 | A),(T2 | (f .: A)); ::_thesis: ( g = f | A implies g is continuous )
assume A2: g = f | A ; ::_thesis: g is continuous
A3: dom f = the carrier of T1 by FUNCT_2:def_1;
A4: [#] (T1 | A) = A by PRE_TOPC:def_5;
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: g is continuous
hence g is continuous by TIETZE:4; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: g is continuous
then reconsider S1 = T1 | A, S2 = T2 | (f .: A) as non empty TopSpace by A3;
f | A = f | (T1 | A) by A4, TMAP_1:def_3;
then A5: g is continuous Function of S1,T2 by A1, A2;
g is Function of S1,S2 ;
hence g is continuous by A5, JORDAN16:8; ::_thesis: verum
end;
end;
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
let T1, T2 be non empty TopSpace; ::_thesis: 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
let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies 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 )
assume that
A1: dom f = [#] T1 and
A2: rng f = [#] T2 and
A3: f is one-to-one and
A4: f is continuous and
A5: f " is continuous ; :: according to TOPS_2:def_5 ::_thesis: 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
let A be Subset of T1; ::_thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is being_homeomorphism
f is onto by A2, FUNCT_2:def_3;
then A6: f " = f " by A3, TOPS_2:def_4;
then A7: (f ") .: (f .: A) = f " (f .: A) by A3, FUNCT_1:85
.= A by A1, A3, FUNCT_1:94 ;
A8: dom f = the carrier of T1 by FUNCT_2:def_1;
let g be Function of (T1 | A),(T2 | (f .: A)); ::_thesis: ( g = f | A implies g is being_homeomorphism )
assume A9: g = f | A ; ::_thesis: g is being_homeomorphism
( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def_5;
hence A10: ( dom g = [#] (T1 | A) & rng g = [#] (T2 | (f .: A)) ) by A9, A8, RELAT_1:62, RELAT_1:115; :: according to TOPS_2:def_5 ::_thesis: ( g is one-to-one & g is continuous & g " is continuous )
A11: g is onto by A10, FUNCT_2:def_3;
thus g is one-to-one by A3, A9, FUNCT_1:52; ::_thesis: ( g is continuous & g " is continuous )
then A12: g " = g " by A11, TOPS_2:def_4;
thus g is continuous by A4, A9, Th13; ::_thesis: g " is continuous
g " = (f ") | (f .: A) by A3, A9, A6, A12, RFUNCT_2:17;
hence g " is continuous by A5, A7, Th13; ::_thesis: verum
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
let T1, T2 be non empty TopSpace; ::_thesis: 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
let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for A, B being Subset of T1 st A is_a_component_of B holds
f .: A is_a_component_of f .: B )
assume A1: f is being_homeomorphism ; ::_thesis: for A, B being Subset of T1 st A is_a_component_of B holds
f .: A is_a_component_of f .: B
let A, B be Subset of T1; ::_thesis: ( A is_a_component_of B implies f .: A is_a_component_of f .: B )
given A1 being Subset of (T1 | B) such that A2: A1 = A and
A3: A1 is a_component ; :: according to CONNSP_1:def_6 ::_thesis: f .: A is_a_component_of f .: B
A4: [#] (T2 | (f .: B)) = f .: B by PRE_TOPC:def_5;
A5: dom f = the carrier of T1 by FUNCT_2:def_1;
A6: [#] (T1 | B) = B by PRE_TOPC:def_5;
then reconsider A2 = f .: A as Subset of (T2 | (f .: B)) by A2, A4, RELAT_1:123;
percases ( B is empty or not B is empty ) ;
supposeA7: B is empty ; ::_thesis: f .: A is_a_component_of f .: B
then f .: B = {} ;
then A8: A2 = {} by A4, XBOOLE_1:3;
{} T2 = f .: B by A7;
hence f .: A is_a_component_of f .: B by A8, JORDAN1K:6; ::_thesis: verum
end;
suppose not B is empty ; ::_thesis: f .: A is_a_component_of f .: B
then reconsider S1 = T1 | B, S2 = T2 | (f .: B) as non empty TopSpace by A5;
take A2 ; :: according to CONNSP_1:def_6 ::_thesis: ( A2 = f .: A & A2 is a_component )
thus A2 = f .: A ; ::_thesis: A2 is a_component
reconsider fB = f | B as Function of S1,S2 by Th12;
fB .: A = A2 by A2, A6, RELAT_1:129;
hence A2 is a_component by A1, A2, A3, Th11, Th14; ::_thesis: verum
end;
end;
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
let S be Subset of (TOP-REAL 2); ::_thesis: for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds
f .: S is Jordan
let f be Homeomorphism of TOP-REAL 2; ::_thesis: ( S is Jordan implies f .: S is Jordan )
set s = the Element of S ` ;
assume A1: S ` <> {} ; :: according to SPRECT_1:def_3 ::_thesis: ( for b1, b2 being Element of K6( the carrier of (TOP-REAL 2)) holds
( not S ` = b1 \/ b2 or not b1 misses b2 or not (Cl b1) \ b1 = (Cl b2) \ b2 or not b1 is_a_component_of S ` or not b2 is_a_component_of S ` ) or f .: S is Jordan )
then the Element of S ` in S ` ;
then reconsider s = the Element of S ` as Element of (TOP-REAL 2) ;
given A1, A2 being Subset of (TOP-REAL 2) such that A2: S ` = A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) ; ::_thesis: f .: S is Jordan
A6: not s in S by A1, XBOOLE_0:def_5;
hereby :: according to SPRECT_1:def_3 ::_thesis: ex b1, b2 being Element of K6( the carrier of (TOP-REAL 2)) st
( (f .: S) ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & b1 is_a_component_of (f .: S) ` & b2 is_a_component_of (f .: S) ` )
assume (f .: S) ` = {} ; ::_thesis: contradiction
then f .: S = the carrier of (TOP-REAL 2) by Th9;
then ex s9 being Element of (TOP-REAL 2) st
( s9 in S & f . s = f . s9 ) by FUNCT_2:65;
hence contradiction by A6, FUNCT_2:56; ::_thesis: verum
end;
take B1 = f .: A1; ::_thesis: ex b1 being Element of K6( the carrier of (TOP-REAL 2)) st
( (f .: S) ` = B1 \/ b1 & B1 misses b1 & (Cl B1) \ B1 = (Cl b1) \ b1 & B1 is_a_component_of (f .: S) ` & b1 is_a_component_of (f .: S) ` )
take B2 = f .: A2; ::_thesis: ( (f .: S) ` = B1 \/ B2 & B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
f .: (A1 \/ A2) = B1 \/ B2 by RELAT_1:120;
hence (f .: S) ` = B1 \/ B2 by A2, JORDAN1K:5; ::_thesis: ( B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
thus B1 misses B2 by A3, FUNCT_1:66; ::_thesis: ( (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
thus (Cl B1) \ B1 = (f .: (Cl A1)) \ B1 by TOPS_2:60
.= f .: ((Cl A2) \ A2) by A4, FUNCT_1:64
.= (f .: (Cl A2)) \ B2 by FUNCT_1:64
.= (Cl B2) \ B2 by TOPS_2:60 ; ::_thesis: ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
f .: (S `) = (f .: S) ` by JORDAN1K:5;
hence ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) by A5, Th15; ::_thesis: verum
end;
*