begin
theorem Th1:
theorem
theorem
theorem Th4:
theorem Th5:
:: deftheorem defines SpanStart JORDAN14:def 1 :
for C being Simple_closed_curve
for n being Element of NAT holds SpanStart C,n = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n);
theorem
canceled;
theorem Th7:
theorem Th8:
for
C being
Simple_closed_curve for
n,
k being
Element of
NAT st
n is_sufficiently_large_for C & 1
<= k &
k + 1
<= len (Span C,n) holds
(
right_cell (Span C,n),
k,
(Gauge C,n) misses C &
left_cell (Span C,n),
k,
(Gauge C,n) meets C )
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
for
C being
Simple_closed_curve for
i,
j,
k,
n being
Element of
NAT st
n is_sufficiently_large_for C & 1
<= k &
k <= len (Span C,n) &
[i,j] in Indices (Gauge C,n) &
(Span C,n) /. k = (Gauge C,n) * i,
j holds
i < len (Gauge C,n)
theorem Th25:
theorem Th26:
for
C being
Simple_closed_curve for
i,
j,
k,
n being
Element of
NAT st
n is_sufficiently_large_for C & 1
<= k &
k <= len (Span C,n) &
[i,j] in Indices (Gauge C,n) &
(Span C,n) /. k = (Gauge C,n) * i,
j holds
j < width (Gauge C,n)
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem