begin
:: 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:
:: 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 );
definition
let a be
Real;
func Rotate a -> Function of
(TOP-REAL 2),
(TOP-REAL 2) means :
Def3:
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
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) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]|
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) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) holds
b1 = b2
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) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| );
theorem Th2:
theorem Th3:
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
theorem Th4:
theorem Th5:
theorem Th6:
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
theorem
:: 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
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem