begin
:: deftheorem Def1 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:
:: deftheorem Def2 defines isometric JORDAN24:def 2 :
definition
let a be
Real;
func Rotate a -> Function of
(TOP-REAL 2),
(TOP-REAL 2) means :
Def3:
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 (TOP-REAL 2),(TOP-REAL 2) 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))]|
uniqueness
for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) 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
end;
:: deftheorem Def3 defines Rotate JORDAN24:def 3 :
theorem Th2:
theorem Th3:
for
p1,
p2 being
Point of
for
P being
Subset of
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 :
theorem
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem