:: JORDAN24 semantic presentation

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
let c₃, c₄ be Point of (TOP-REAL c₁);
pred c₃,c₄ realize-max-dist-in c₂ means :Def1: :: JORDAN24:def 1
( a₃ in a₂ & a₄ in a₂ & ( for b₁, b₂ being Point of (TOP-REAL a₁) st b₁ in a₂ & b₂ in a₂ holds
dist a₃,a₄ >= dist b₁,b₂ ) );

end;

:: deftheorem Def1 defines realize-max-dist-in JORDAN24:def 1 :

set c₁ = - 1;

set c₂ = 1;

set c₃ = |[(- 1),0]|;

set c₄ = |[1,0]|;

theorem Th1: :: JORDAN24:1

for b₁ being Simple_closed_curve ex b₂, b₃ being Point of (TOP-REAL 2) st b₂,b₃ realize-max-dist-in b₁

proof end;

definition

let c₅ be non empty MetrStruct ;
let c₆ be Function of (TopSpaceMetr c₅),(TopSpaceMetr c₅);
attr a₂ is isometric means :Def2: :: JORDAN24:def 2
ex b₁ being isometric Function of a₁,a₁ st b₁ = a₂;

end;

:: deftheorem Def2 defines isometric JORDAN24:def 2 :

registration

let c₅ be non empty MetrStruct ;
cluster isometric M4(the carrier of (TopSpaceMetr a₁),the carrier of (TopSpaceMetr a₁));
existence

proof end;

end;

registration

let c₅ be non empty MetrSpace;
cluster isometric -> continuous M4(the carrier of (TopSpaceMetr a₁),the carrier of (TopSpaceMetr a₁));
coherence

proof end;

end;

registration

let c₅ be non empty MetrSpace;
cluster isometric -> being_homeomorphism M4(the carrier of (TopSpaceMetr a₁),the carrier of (TopSpaceMetr a₁));
coherence

proof end;

end;

definition

let c₅ be Real;
func Rotate c₁ -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def3: :: JORDAN24:def 3
for b₁ being Point of (TOP-REAL 2) holds a₂ . b₁ = |[(Re (Rotate ((b₁ `1 ) + ((b₁ `2 ) * <i> )),a₁)),(Im (Rotate ((b₁ `1 ) + ((b₁ `2 ) * <i> )),a₁))]|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Rotate JORDAN24:def 3 :

theorem Th2: :: JORDAN24:2

for b₁ being Real st 0 <= b₁ & b₁ < 2 * PI holds
for b₂ being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st b₂ = Rotate b₁ holds
b₂ is isometric

proof end;

theorem Th3: :: JORDAN24:3

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Subset of (TOP-REAL 2)
for b₄, b₅, b₆ being real number st b₁,b₂ realize-max-dist-in b₃ holds
(AffineMap b₄,b₅,b₄,b₆) . b₁,(AffineMap b₄,b₅,b₄,b₆) . b₂ realize-max-dist-in (AffineMap b₄,b₅,b₄,b₆) .: b₃

proof end;

theorem Th4: :: JORDAN24:4

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Subset of (TOP-REAL 2)
for b₄ being Real st 0 <= b₄ & b₄ < 2 * PI & b₁,b₂ realize-max-dist-in b₃ holds
(Rotate b₄) . b₁,(Rotate b₄) . b₂ realize-max-dist-in (Rotate b₄) .: b₃

proof end;

theorem Th5: :: JORDAN24:5

for b₁ being complex number
for b₂ being Real holds Rotate b₁,(- b₂) = Rotate b₁,((2 * PI ) - b₂)

proof end;

theorem Th6: :: JORDAN24:6

for b₁ being Real holds Rotate (- b₁) = Rotate ((2 * PI ) - b₁)

proof end;

theorem Th7: :: JORDAN24:7

for b₁ being Simple_closed_curve ex b₂ being Homeomorphism of TOP-REAL 2 st |[(- 1),0]|,|[1,0]| realize-max-dist-in b₂ .: b₁

proof end;

definition

let c₅, c₆ be TopStruct ;
let c₇ be Function of c₅,c₆;
attr a₃ is closed means :: JORDAN24:def 4
for b₁ being Subset of a₁ st b₁ is closed holds
a₃ .: b₁ is closed;

end;

:: deftheorem Def4 defines closed JORDAN24:def 4 :

theorem Th8: :: JORDAN24:8

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂ st b₃ is one-to-one & b₃ is onto holds
( b₃ is_homeomorphism iff b₃ is closed )

proof end;

theorem Th9: :: JORDAN24:9

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ ` = {} iff b₂ = b₁ )

proof end;

theorem Th10: :: JORDAN24:10

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
for b₄ being Subset of b₁ st b₄ is connected holds
b₃ .: b₄ is connected

proof end;

theorem Th11: :: JORDAN24:11

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
for b₄ being Subset of b₁ st b₄ is_a_component_of b₁ holds
b₃ .: b₄ is_a_component_of b₂

proof end;

theorem Th12: :: JORDAN24:12

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ holds b₃ | b₄ is Function of (b₁ | b₄),(b₂ | (b₃ .: b₄))

proof end;

theorem Th13: :: JORDAN24:13

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is continuous holds
for b₄ being Subset of b₁
for b₅ being Function of (b₁ | b₄),(b₂ | (b₃ .: b₄)) st b₅ = b₃ | b₄ holds
b₅ is continuous

proof end;

theorem Th14: :: JORDAN24:14

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
for b₄ being Subset of b₁
for b₅ being Function of (b₁ | b₄),(b₂ | (b₃ .: b₄)) st b₅ = b₃ | b₄ holds
b₅ is_homeomorphism

proof end;

theorem Th15: :: JORDAN24:15

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
for b₄, b₅ being Subset of b₁ st b₄ is_a_component_of b₅ holds
b₃ .: b₄ is_a_component_of b₃ .: b₅

proof end;

theorem Th16: :: JORDAN24:16

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Homeomorphism of TOP-REAL 2 st b₁ is Jordan holds
b₂ .: b₁ is Jordan

proof end;