environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, GOBOARD5, JORDAN2C, TOPREAL1, GOBOARD9, CONNSP_1, SUBSET_1, GOBOARD1, FINSEQ_1, EUCLID, XXREAL_0, ARYTM_3, RCOMP_1, MATRIX_1, PARTFUN1, RELAT_1, ARYTM_1, PRE_TOPC, TREES_1, TOPS_1, MCART_1, REAL_1, RELAT_2, TOPREAL2, JORDAN8, JORDAN1H, JORDAN11, TARSKI, RLTOPSP1, JORDAN13, XBOOLE_0, CARD_1, GOBRD13, ORDINAL4, STRUCT_0, PSCOMP_1, SPPOL_1, NEWTON, COMPLEX1, JORDAN14, CONVEX1, XXREAL_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, PARTFUN1, FINSEQ_1, SEQM_3, STRUCT_0, MATRIX_0, PRE_TOPC, TOPREAL2, TOPS_1, COMPTS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, GOBRD13, JORDAN1H, JORDAN11, JORDAN13, XXREAL_0;
definitions TARSKI;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, PSCOMP_1, FINSEQ_5, GOBOARD7, TOPREAL1, JORDAN5B, GOBOARD5, GOBOARD9, SUBSET_1, GOBRD11, SPRECT_3, GOBOARD6, TOPS_1, JORDAN8, GOBRD13, SPRECT_4, CONNSP_1, XBOOLE_0, XBOOLE_1, NEWTON, GOBRD14, TOPREAL6, INT_1, JORDAN2C, PRE_TOPC, JORDAN9, JORDAN1H, TSEP_1, GOBRD12, JORDAN1A, JORDAN1C, JORDAN11, JORDAN13, XREAL_1, XXREAL_0, CARD_1, MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3;
schemes NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, TOPREAL1, TOPREAL2, TOPREAL5, SPRECT_2, SPRECT_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD14, EUCLID, RLTOPSP1, JORDAN1, XREAL_0, NAT_1, NEWTON;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPREAL4, JORDAN1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, JORDAN1H, JORDAN11, JORDAN13, CONVEX1, RELSET_1, GOBRD13;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions TARSKI;
theorem Th7:
for
C being
Simple_closed_curve for
n,
k being
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 Th23:
for
C being
Simple_closed_curve for
i,
j,
k,
n being
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:
for
C being
Simple_closed_curve for
i,
j,
k,
n being
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))