:: JORDAN24 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let n be Nat;
let A be Subset of (TOP-REAL n);
let a, b be Point of (TOP-REAL n);
pred a,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 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]|;

theorem Th1: :: JORDAN24:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C
proof end;

definition
let M be non empty MetrStruct ;
let f be Function of (TopSpaceMetr M),(TopSpaceMetr M);
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 (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 isometric M4(the carrier of (TopSpaceMetr M),the carrier of (TopSpaceMetr M));
existence
ex b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b1 is isometric
proof end;
end;

registration
let M be non empty MetrSpace;
cluster isometric -> continuous M4(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 end;
end;

registration
let M be non empty MetrSpace;
cluster isometric -> being_homeomorphism M4(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 being_homeomorphism
proof 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 ) * <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))]|
proof 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 ) * <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
proof 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 ) * <i> )),a)),(Im (Rotate ((p `1 ) + ((p `2 ) * <i> )),a))]| );

theorem Th2: :: JORDAN24:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real st 0 <= a & a < 2 * PI holds
for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds
f is isometric
proof end;

theorem Th3: :: JORDAN24:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th4: :: JORDAN24:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2)
for A being Real st 0 <= A & A < 2 * PI & p1,p2 realize-max-dist-in P holds
(Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
proof end;

theorem Th5: :: JORDAN24:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number
for r being Real holds Rotate z,(- r) = Rotate z,((2 * PI ) - r)
proof end;

theorem Th6: :: JORDAN24:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real holds Rotate (- r) = Rotate ((2 * PI ) - r)
proof end;

theorem :: JORDAN24:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 );

theorem :: JORDAN24:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_homeomorphism iff f is closed )
proof end;

theorem Th9: :: JORDAN24:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of X holds
( A ` = {} iff A = X )
proof end;

theorem Th10: :: JORDAN24:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is_homeomorphism holds
for A being Subset of T1 st A is connected holds
f .: A is connected
proof end;

theorem Th11: :: JORDAN24:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is_homeomorphism holds
for A being Subset of T1 st A is_a_component_of T1 holds
f .: A is_a_component_of T2
proof end;

theorem Th12: :: JORDAN24:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is_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_homeomorphism
proof end;

theorem Th15: :: JORDAN24:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;