begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem
theorem
theorem Th6:
theorem Th7:
begin
definition
let n be
Element of
NAT ;
A1:
[:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] = the
carrier of
[:(TOP-REAL n),(TOP-REAL n):]
by BORSUK_1:def 5;
func Eucl_dist n -> RealMap of
[:(TOP-REAL n),(TOP-REAL n):] means :
Def1:
for
p,
q being
Point of holds
it . p,
q = |.(p - q).|;
existence
ex b1 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st
for p, q being Point of holds b1 . p,q = |.(p - q).|
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of holds b1 . p,q = |.(p - q).| ) & ( for p, q being Point of holds b2 . p,q = |.(p - q).| ) holds
b1 = b2
end;
:: deftheorem Def1 defines Eucl_dist JORDAN_A:def 1 :
:: deftheorem defines continuous JORDAN_A:def 2 :
Lm1:
for X, Y being TopSpace holds TopStruct(# the carrier of [:X,Y:],the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):]
begin
theorem Th8:
begin
theorem Th9:
for
C being
Simple_closed_curve for
p,
q being
Point of st
LE p,
q,
C &
LE q,
E-max C,
C &
p <> q holds
Segment p,
q,
C = Segment (Upper_Arc C),
(W-min C),
(E-max C),
p,
q
theorem Th10:
theorem Th11:
theorem Th12:
for
C being
Simple_closed_curve for
p,
q being
Point of st
LE p,
q,
C &
LE E-max C,
p,
C holds
Segment p,
q,
C = Segment (Lower_Arc C),
(E-max C),
(W-min C),
p,
q
theorem Th13:
for
C being
Simple_closed_curve for
p,
q being
Point of st
LE p,
E-max C,
C &
LE E-max C,
q,
C holds
Segment p,
q,
C = (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) \/ (L_Segment (Lower_Arc C),(E-max C),(W-min C),q)
theorem Th14:
for
C being
Simple_closed_curve for
p being
Point of st
LE p,
E-max C,
C holds
Segment p,
(W-min C),
C = (R_Segment (Upper_Arc C),(W-min C),(E-max C),p) \/ (L_Segment (Lower_Arc C),(E-max C),(W-min C),(W-min C))
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
definition
let C be
Simple_closed_curve;
mode Segmentation of
C -> FinSequence of
means :
Def3:
(
it /. 1
= W-min C &
it is
one-to-one & 8
<= len it &
rng it c= C & ( for
i being
Element of
NAT st 1
<= i &
i < len it holds
LE it /. i,
it /. (i + 1),
C ) & ( for
i being
Element of
NAT st 1
<= i &
i + 1
< len it holds
(Segment (it /. i),(it /. (i + 1)),C) /\ (Segment (it /. (i + 1)),(it /. (i + 2)),C) = {(it /. (i + 1))} ) &
(Segment (it /. (len it)),(it /. 1),C) /\ (Segment (it /. 1),(it /. 2),C) = {(it /. 1)} &
(Segment (it /. ((len it) -' 1)),(it /. (len it)),C) /\ (Segment (it /. (len it)),(it /. 1),C) = {(it /. (len it))} &
Segment (it /. ((len it) -' 1)),
(it /. (len it)),
C misses Segment (it /. 1),
(it /. 2),
C & ( for
i,
j being
Element of
NAT st 1
<= i &
i < j &
j < len it & not
i,
j are_adjacent1 holds
Segment (it /. i),
(it /. (i + 1)),
C misses Segment (it /. j),
(it /. (j + 1)),
C ) & ( for
i being
Element of
NAT st 1
< i &
i + 1
< len it holds
Segment (it /. (len it)),
(it /. 1),
C misses Segment (it /. i),
(it /. (i + 1)),
C ) );
existence
ex b1 being FinSequence of st
( b1 /. 1 = W-min C & b1 is one-to-one & 8 <= len b1 & rng b1 c= C & ( for i being Element of NAT st 1 <= i & i < len b1 holds
LE b1 /. i,b1 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b1 holds
(Segment (b1 /. i),(b1 /. (i + 1)),C) /\ (Segment (b1 /. (i + 1)),(b1 /. (i + 2)),C) = {(b1 /. (i + 1))} ) & (Segment (b1 /. (len b1)),(b1 /. 1),C) /\ (Segment (b1 /. 1),(b1 /. 2),C) = {(b1 /. 1)} & (Segment (b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C) /\ (Segment (b1 /. (len b1)),(b1 /. 1),C) = {(b1 /. (len b1))} & Segment (b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C misses Segment (b1 /. 1),(b1 /. 2),C & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b1 & not i,j are_adjacent1 holds
Segment (b1 /. i),(b1 /. (i + 1)),C misses Segment (b1 /. j),(b1 /. (j + 1)),C ) & ( for i being Element of NAT st 1 < i & i + 1 < len b1 holds
Segment (b1 /. (len b1)),(b1 /. 1),C misses Segment (b1 /. i),(b1 /. (i + 1)),C ) )
end;
:: deftheorem Def3 defines Segmentation JORDAN_A:def 3 :
for
C being
Simple_closed_curve for
b2 being
FinSequence of holds
(
b2 is
Segmentation of
C iff (
b2 /. 1
= W-min C &
b2 is
one-to-one & 8
<= len b2 &
rng b2 c= C & ( for
i being
Element of
NAT st 1
<= i &
i < len b2 holds
LE b2 /. i,
b2 /. (i + 1),
C ) & ( for
i being
Element of
NAT st 1
<= i &
i + 1
< len b2 holds
(Segment (b2 /. i),(b2 /. (i + 1)),C) /\ (Segment (b2 /. (i + 1)),(b2 /. (i + 2)),C) = {(b2 /. (i + 1))} ) &
(Segment (b2 /. (len b2)),(b2 /. 1),C) /\ (Segment (b2 /. 1),(b2 /. 2),C) = {(b2 /. 1)} &
(Segment (b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C) /\ (Segment (b2 /. (len b2)),(b2 /. 1),C) = {(b2 /. (len b2))} &
Segment (b2 /. ((len b2) -' 1)),
(b2 /. (len b2)),
C misses Segment (b2 /. 1),
(b2 /. 2),
C & ( for
i,
j being
Element of
NAT st 1
<= i &
i < j &
j < len b2 & not
i,
j are_adjacent1 holds
Segment (b2 /. i),
(b2 /. (i + 1)),
C misses Segment (b2 /. j),
(b2 /. (j + 1)),
C ) & ( for
i being
Element of
NAT st 1
< i &
i + 1
< len b2 holds
Segment (b2 /. (len b2)),
(b2 /. 1),
C misses Segment (b2 /. i),
(b2 /. (i + 1)),
C ) ) );
theorem Th22:
begin
:: deftheorem Def4 defines Segm JORDAN_A:def 4 :
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
begin
:: deftheorem Def5 defines diameter JORDAN_A:def 5 :
:: deftheorem Def6 defines diameter JORDAN_A:def 6 :
theorem
theorem Th34:
theorem
begin
definition
let C be
Simple_closed_curve;
let S be
Segmentation of
C;
func S-Gap S -> Real means :
Def7:
ex
S1,
S2 being non
empty finite Subset of st
(
S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } &
S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } &
it = min (min S1),
(min S2) );
existence
ex b1 being Real ex S1, S2 being non empty finite Subset of st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min (min S1),(min S2) )
correctness
uniqueness
for b1, b2 being Real st ex S1, S2 being non empty finite Subset of st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min (min S1),(min S2) ) & ex S1, S2 being non empty finite Subset of st
( S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b2 = min (min S1),(min S2) ) holds
b1 = b2;
;
end;
:: deftheorem Def7 defines S-Gap JORDAN_A:def 7 :
for
C being
Simple_closed_curve for
S being
Segmentation of
C for
b3 being
Real holds
(
b3 = S-Gap S iff ex
S1,
S2 being non
empty finite Subset of st
(
S1 = { (dist_min (Segm S,i),(Segm S,j)) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } &
S2 = { (dist_min (Segm S,(len S)),(Segm S,k)) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } &
b3 = min (min S1),
(min S2) ) );
theorem Th36:
theorem