environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID, RCOMP_1, SPPOL_1, GOBOARD1, STRUCT_0, JORDAN2C, TOPREAL1, REAL_1, XXREAL_0, CARD_1, METRIC_1, TARSKI, XXREAL_2, ARYTM_3, XBOOLE_0, COMPLEX1, RELAT_2, CONNSP_1, FINSEQ_1, TREES_1, CARD_3, FUNCOP_1, XXREAL_1, RELAT_1, MCART_1, MATRIX_1, ARYTM_1, SQUARE_1, JORDAN8, NEWTON, PSCOMP_1, INT_1, POWER, GOBOARD9, RLTOPSP1, GOBOARD2, PARTFUN1, TOPS_1, JORDAN1, FINSEQ_6, SPRECT_1, SEQ_4, FINSEQ_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, SQUARE_1, NAT_1, INT_1, INT_2, NEWTON, POWER, MATRIX_0, NAT_D, MATRIX_1, FUNCT_4, SEQ_4, METRIC_1, TBSP_1, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_6, STRUCT_0, RCOMP_1, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, SPRECT_1, SPRECT_2, JORDAN2C, JORDAN8, TOPREAL6;
definitions TARSKI, JORDAN2C, SPRECT_1, XBOOLE_0;
theorems ABSVALUE, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, EUCLID, FINSEQ_1, FUNCT_1, FUNCT_2, GOBOARD5, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11, GOBRD12, INT_1, JORDAN2C, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC, PRE_FF, PSCOMP_1, RCOMP_1, RELAT_1, SEQ_4, SPRECT_1, SPRECT_3, SPRECT_4, SQUARE_1, SPPOL_2, SUBSET_1, TARSKI, TBSP_1, TDLAT_1, TOPREAL1, TOPREAL3, TOPREAL6, TOPS_1, SPRECT_2, REVROT_1, FINSEQ_6, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, NEWTON, XXREAL_0, FINSEQ_2, MATRIX_0, XXREAL_1, NAT_D, RLTOPSP1;
schemes ;
registrations SUBSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_1, MONOID_0, EUCLID, GOBOARD2, GOBRD11, SPRECT_1, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, FUNCT_1, FINSEQ_1, PSCOMP_1, RELSET_1, JORDAN5A, NEWTON, SQUARE_1, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, NEWTON, POWER, NAT_D, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6, JORDAN8, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, BINOP_2, MATRIX_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities JORDAN2C, XBOOLE_0, SQUARE_1, SUBSET_1, EUCLID;
expansions TARSKI, JORDAN2C, XBOOLE_0;
Lm1:
the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:22;
theorem Th3:
for
i,
j being
Nat for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j < width G holds
cell (
G,
i,
j)
= product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
theorem
for
i,
j being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
i <= j holds
for
a,
b being
Nat st 2
<= a &
a <= (len (Gauge (C,i))) - 1 & 2
<= b &
b <= (len (Gauge (C,i))) - 1 holds
ex
c,
d being
Nat st
( 2
<= c &
c <= (len (Gauge (C,j))) - 1 & 2
<= d &
d <= (len (Gauge (C,j))) - 1 &
[c,d] in Indices (Gauge (C,j)) &
(Gauge (C,i)) * (
a,
b)
= (Gauge (C,j)) * (
c,
d) &
c = 2
+ ((2 |^ (j -' i)) * (a -' 2)) &
d = 2
+ ((2 |^ (j -' i)) * (b -' 2)) )
theorem Th9:
for
i,
j,
n being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
[i,j] in Indices (Gauge (C,n)) &
[i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,(j + 1))))
= ((N-bound C) - (S-bound C)) / (2 |^ n)
theorem Th10:
for
i,
j,
n being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
[i,j] in Indices (Gauge (C,n)) &
[(i + 1),j] in Indices (Gauge (C,n)) holds
dist (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * ((i + 1),j)))
= ((E-bound C) - (W-bound C)) / (2 |^ n)
theorem
for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
r,
t being
Real st
r > 0 &
t > 0 holds
ex
n being
Nat st
( 1
< n &
dist (
((Gauge (C,n)) * (1,1)),
((Gauge (C,n)) * (1,2)))
< r &
dist (
((Gauge (C,n)) * (1,1)),
((Gauge (C,n)) * (2,1)))
< t )