begin
Lm1: 2 -' 1 =
2 - 1
by XREAL_1:233
.=
1
;
Lm2:
for i, j, k being Element of NAT st i -' k <= j holds
i <= j + k
Lm3:
for i, j, k being Element of NAT st j + k <= i holds
k <= i -' j
::
deftheorem Def1 defines
Segment JORDAN7:def 1 :
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) holds
( ( q2 <> W-min P implies Segment (q1,q2,P) = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies Segment (q1,q2,P) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) );
theorem Th10:
for
P being non
empty compact Subset of
(TOP-REAL 2) for
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
LE q1,
q2,
P &
LE q2,
q3,
P & ( not
q1 = q2 or not
q1 = W-min P ) & ( not
q2 = q3 or not
q2 = W-min P ) holds
(Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}
theorem Th13:
for
P being non
empty compact Subset of
(TOP-REAL 2) for
q1,
q2,
q3,
q4 being
Point of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
LE q1,
q2,
P &
LE q2,
q3,
P &
LE q3,
q4,
P &
q1 <> q2 &
q2 <> q3 holds
Segment (
q1,
q2,
P)
misses Segment (
q3,
q4,
P)
theorem Th14:
for
P being non
empty compact Subset of
(TOP-REAL 2) for
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
LE q1,
q2,
P &
LE q2,
q3,
P &
q1 <> W-min P &
q2 <> q3 holds
Segment (
q1,
q2,
P)
misses Segment (
q3,
(W-min P),
P)
begin
Lm5:
0 in [.0,1.]
by XXREAL_1:1;
Lm6:
1 in [.0,1.]
by XXREAL_1:1;
theorem Th18:
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) for
g being
Function of
I[01],
(TOP-REAL 2) for
s1,
s2 being
Real st
P is_an_arc_of p1,
p2 &
g is
continuous &
g is
one-to-one &
rng g = P &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
0 <= s1 &
s1 <= 1 &
g . s2 = q2 &
0 <= s2 &
s2 <= 1 &
s1 <= s2 holds
LE q1,
q2,
P,
p1,
p2
theorem
for
P being non
empty compact Subset of
(TOP-REAL 2) for
e being
Real st
P is
being_simple_closed_curve &
e > 0 holds
ex
h being
FinSequence of the
carrier of
(TOP-REAL 2) st
(
h . 1
= W-min P &
h is
one-to-one & 8
<= len h &
rng h c= P & ( for
i being
Element of
NAT st 1
<= i &
i < len h holds
LE h /. i,
h /. (i + 1),
P ) & ( for
i being
Element of
NAT for
W being
Subset of
(Euclid 2) st 1
<= i &
i < len h &
W = Segment (
(h /. i),
(h /. (i + 1)),
P) holds
diameter W < e ) & ( for
W being
Subset of
(Euclid 2) st
W = Segment (
(h /. (len h)),
(h /. 1),
P) holds
diameter W < e ) & ( for
i being
Element of
NAT st 1
<= i &
i + 1
< len h holds
(Segment ((h /. i),(h /. (i + 1)),P)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),P)) = {(h /. (i + 1))} ) &
(Segment ((h /. (len h)),(h /. 1),P)) /\ (Segment ((h /. 1),(h /. 2),P)) = {(h /. 1)} &
(Segment ((h /. ((len h) -' 1)),(h /. (len h)),P)) /\ (Segment ((h /. (len h)),(h /. 1),P)) = {(h /. (len h))} &
Segment (
(h /. ((len h) -' 1)),
(h /. (len h)),
P)
misses Segment (
(h /. 1),
(h /. 2),
P) & ( for
i,
j being
Element of
NAT st 1
<= i &
i < j &
j < len h & not
i,
j are_adjacent1 holds
Segment (
(h /. i),
(h /. (i + 1)),
P)
misses Segment (
(h /. j),
(h /. (j + 1)),
P) ) & ( for
i being
Element of
NAT st 1
< i &
i + 1
< len h holds
Segment (
(h /. (len h)),
(h /. 1),
P)
misses Segment (
(h /. i),
(h /. (i + 1)),
P) ) )