environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, GOBOARD1, XXREAL_0, TREES_1, ARYTM_3, FINSEQ_1, RELAT_1, MCART_1, XBOOLE_0, GRAPH_2, ORDINAL4, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, TOPREAL1, JORDAN9, FINSEQ_5, PSCOMP_1, PARTFUN1, TARSKI, CARD_1, FINSEQ_4, PRE_TOPC, RLTOPSP1, ARYTM_1, JORDAN1E, FINSEQ_6, RFINSEQ, JORDAN3, FUNCT_1, GOBOARD5, GOBOARD9, CONNSP_1, TOPREAL2, JORDAN8, SPPOL_2, NAT_1, GROUP_2, MATRIX_1, SPRECT_2, ZFMISC_1, JORDAN6, GOBOARD2, JORDAN2C, JORDAN1A, XXREAL_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E;
definitions TARSKI, GOBOARD5, XBOOLE_0;
theorems JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_1, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, JORDAN5B, JORDAN3, GOBRD13, INT_1, JORDAN9, JORDAN2C, SUBSET_1, CONNSP_1, ZFMISC_1, JGRAPH_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3, FINSEQ_3, RELAT_1, COMPTS_1, FUNCT_1, TOPREAL5, JORDAN10, GRAPH_2, GOBOARD2, CARD_1, CARD_2, ENUMSET1, SPRECT_4, JORDAN1B, SPRECT_5, JORDAN1E, PARTFUN2, JORDAN1F, TDLAT_1, JORDAN1G, GOBOARD3, JORDAN1H, TOPREAL8, GOBRD14, JORDAN1D, JORDAN1I, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, EUCLID, PRE_TOPC, ORDINAL1, PARTFUN1, MATRIX_0, XREAL_0, NAT_D, RLTOPSP1;
schemes NAT_1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1G, CARD_1, FUNCT_1, EUCLID, JORDAN2C, INT_1, ORDINAL1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, RFINSEQ, TOPS_1, CONNSP_1, MATRIX_1, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, RELSET_1, CONVEX1, DOMAIN_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorem Th52:
for
G being
Go-board for
f being
S-Sequence_in_R2 for
p being
Point of
(TOP-REAL 2) for
k being
Nat st 1
<= k &
k < p .. f &
f is_sequence_on G &
p in rng f holds
(
left_cell (
(R_Cut (f,p)),
k,
G)
= left_cell (
f,
k,
G) &
right_cell (
(R_Cut (f,p)),
k,
G)
= right_cell (
f,
k,
G) )
theorem Th57:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
k <= width (Gauge (C,n)) &
(Gauge (C,n)) * (
i,
k)
in L~ (Upper_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
in L~ (Lower_Seq (C,n)) holds
j <> k
theorem Th58:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Lower_Arc C
theorem Th59:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Upper_Arc C
theorem Th60:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Lower_Arc C
theorem Th61:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Upper_Arc C
theorem
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
j being
Nat st
(Gauge (C,(n + 1))) * (
(Center (Gauge (C,(n + 1)))),
j)
in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1
<= j &
j <= width (Gauge (C,(n + 1))) holds
LSeg (
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)))
meets Lower_Arc (L~ (Cage (C,(n + 1))))
theorem
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 1
<= j &
j <= k &
k <= width (Gauge (C,(n + 1))) &
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} &
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds
LSeg (
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))
meets Lower_Arc C
theorem
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 1
<= j &
j <= k &
k <= width (Gauge (C,(n + 1))) &
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} &
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds
LSeg (
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))
meets Upper_Arc C