begin
Lm1:
for i, j, k being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st i > 0 & 1 <= j & j <= width (Gauge (C,i)) & k <= j & 1 <= k & k <= width (Gauge (C,i)) & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} holds
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i)))
Lm2:
for C being being_simple_closed_curve Subset of (TOP-REAL 2) ex n being Element of NAT st n is_sufficiently_large_for C
definition
let C be
being_simple_closed_curve Subset of
(TOP-REAL 2);
func Y-InitStart C -> Element of
NAT means :
Def2:
(
it < width (Gauge (C,(ApproxIndex C))) &
cell (
(Gauge (C,(ApproxIndex C))),
((X-SpanStart (C,(ApproxIndex C))) -' 1),
it)
c= BDD C & ( for
j being
Element of
NAT st
j < width (Gauge (C,(ApproxIndex C))) &
cell (
(Gauge (C,(ApproxIndex C))),
((X-SpanStart (C,(ApproxIndex C))) -' 1),
j)
c= BDD C holds
j >= it ) );
existence
ex b1 being Element of NAT st
( b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b1 ) )
uniqueness
for b1, b2 being Element of NAT st b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b1 ) & b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b2 ) holds
b1 = b2
end;
::
deftheorem Def2 defines
Y-InitStart JORDAN11:def 2 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b2 being Element of NAT holds
( b2 = Y-InitStart C iff ( b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b2 ) ) );
definition
let C be
being_simple_closed_curve Subset of
(TOP-REAL 2);
let n be
Element of
NAT ;
assume
n is_sufficiently_large_for C
;
then A1:
n >= ApproxIndex C
by Def1;
set i1 =
X-SpanStart (
C,
n);
func Y-SpanStart (
C,
n)
-> Element of
NAT means :
Def3:
(
it <= width (Gauge (C,n)) & ( for
k being
Element of
NAT st
it <= k &
k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
k)
c= BDD C ) & ( for
j being
Element of
NAT st
j <= width (Gauge (C,n)) & ( for
k being
Element of
NAT st
j <= k &
k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
k)
c= BDD C ) holds
j >= it ) );
existence
ex b1 being Element of NAT st
( b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) )
uniqueness
for b1, b2 being Element of NAT st b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) & b2 <= width (Gauge (C,n)) & ( for k being Element of NAT st b2 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b2 ) holds
b1 = b2
end;
::
deftheorem Def3 defines
Y-SpanStart JORDAN11:def 3 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C holds
for b3 being Element of NAT holds
( b3 = Y-SpanStart (C,n) iff ( b3 <= width (Gauge (C,n)) & ( for k being Element of NAT st b3 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b3 ) ) );
begin