environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, PSCOMP_1, TOPREAL1, JORDAN9, FINSEQ_4, XXREAL_0, PARTFUN1, ARYTM_3, FUNCT_1, GOBOARD5, PRE_TOPC, RELAT_1, FINSEQ_6, FINSEQ_1, MATRIX_1, GOBOARD2, ARYTM_1, XBOOLE_0, JORDAN8, TREES_1, GOBOARD1, MCART_1, COMPLEX1, CARD_1, RLTOPSP1, TARSKI, SPRECT_2, GOBOARD9, JORDAN2C, TOPS_1, REAL_1, JORDAN5D, CONNSP_1, TOPREAL2, JORDAN1A, JORDAN6, JORDAN1E, SEQ_4, XXREAL_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, FUNCT_1, NAT_D, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, FINSEQ_6, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, TOPREAL2, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN5D, JORDAN1A, JORDAN1E, XXREAL_0;
definitions TARSKI;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5, JORDAN4, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_2, REVROT_1, TOPREAL1, GOBRD13, JORDAN9, JORDAN2C, ABSVALUE, GOBOARD1, TARSKI, TOPREAL3, FINSEQ_3, UNIFORM1, FUNCT_1, JORDAN1B, SPRECT_5, JORDAN5D, JORDAN1E, JORDAN1F, JORDAN1G, JORDAN1H, TOPREAL8, GOBRD14, JORDAN1D, GOBOARD6, SPRECT_1, XBOOLE_0, XBOOLE_1, XREAL_1, JORDAN6, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3;
schemes ;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, GOBOARD2, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, FUNCT_1, EUCLID, JORDAN2C, XREAL_0, NAT_1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, TOPS_1, CONNSP_1, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN6, JORDAN5D, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1;
expansions ;
theorem
for
i,
k being
Nat for
C being non
empty being_simple_closed_curve compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
p being
Point of
(TOP-REAL 2) st
p `1 = ((W-bound C) + (E-bound C)) / 2 &
i > 0 & 1
<= k &
k <= width (Gauge (C,i)) &
(Gauge (C,i)) * (
(Center (Gauge (C,i))),
k)
in Upper_Arc (L~ (Cage (C,i))) &
p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex
j being
Nat st
( 1
<= j &
j <= width (Gauge (C,i)) &
p = (Gauge (C,i)) * (
(Center (Gauge (C,i))),
j) )