environ
vocabularies HIDDEN, NUMBERS, RELAT_2, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, TOPREAL1, XXREAL_0, ARYTM_3, FINSEQ_1, JORDAN9, MATRIX_1, JORDAN8, PARTFUN1, RELAT_1, TREES_1, GOBOARD1, GOBOARD5, ARYTM_1, CARD_1, XBOOLE_0, TARSKI, RLTOPSP1, PSCOMP_1, NEWTON, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1, REAL_1, CONNSP_1, STRUCT_0, JORDAN2C, CONNSP_3, XXREAL_2, SETFAM_1, ZFMISC_1, TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, PARTFUN1, FINSEQ_1, NEWTON, DOMAIN_1, STRUCT_0, METRIC_1, TBSP_1, WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1, MATRIX_0, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4, PSCOMP_1, GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, TOPREAL6, JORDAN9, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems CONNSP_1, CONNSP_3, EUCLID, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11, GOBRD13, GOBRD14, JGRAPH_1, JORDAN2C, JORDAN3, JORDAN6, JORDAN8, JORDAN9, NEWTON, NAT_1, PRE_TOPC, SETFAM_1, SPPOL_2, SPRECT_1, SPRECT_3, SPRECT_4, SUBSET_1, TARSKI, TOPREAL1, TOPREAL3, TOPREAL4, TOPREAL6, TOPS_1, WEIERSTR, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, MATRIX_0, XREAL_0, COMPTS_1, RLTOPSP1, NAT_D;
schemes NAT_1;
registrations SUBSET_1, RELSET_1, XXREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1, SPPOL_2, SPRECT_1, JORDAN2C, TOPREAL6, JORDAN8, FUNCT_1, NEWTON, ORDINAL1, XREAL_0, NAT_1;
constructors HIDDEN, REAL_1, NEWTON, TOPS_1, CONNSP_1, TBSP_1, TOPREAL4, PSCOMP_1, WEIERSTR, GOBOARD9, CONNSP_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, NAT_D, FUNCSDOM;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, SUBSET_1, PSCOMP_1, CONNSP_3;
expansions TARSKI, XBOOLE_0;
theorem Th1:
for
i,
j,
k,
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage (C,n)) &
[i,j] in Indices (Gauge (C,n)) &
[i,(j + 1)] in Indices (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
i,
j) &
(Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (
i,
(j + 1)) holds
i < len (Gauge (C,n))
theorem Th2:
for
i,
j,
k,
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage (C,n)) &
[i,j] in Indices (Gauge (C,n)) &
[i,(j + 1)] in Indices (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
i,
(j + 1)) &
(Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (
i,
j) holds
i > 1
theorem Th3:
for
i,
j,
k,
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage (C,n)) &
[i,j] in Indices (Gauge (C,n)) &
[(i + 1),j] in Indices (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
i,
j) &
(Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (
(i + 1),
j) holds
j > 1
theorem Th4:
for
i,
j,
k,
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage (C,n)) &
[i,j] in Indices (Gauge (C,n)) &
[(i + 1),j] in Indices (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
(i + 1),
j) &
(Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (
i,
j) holds
j < width (Gauge (C,n))