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
:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b2 being Element of NAT holds
( b2 = ApproxIndex C iff ( b2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= b2 ) ) );
theorem Th1:
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 ) ) );
theorem Th2:
theorem Th3:
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 ) ) );
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem
theorem
begin
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem