environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, FINSEQ_1, MATRIX_1, GOBOARD1, RELAT_1, PARTFUN1, ARYTM_3, COMPLEX1, ARYTM_1, XBOOLE_0, RFINSEQ, XXREAL_0, PRE_TOPC, EUCLID, GOBOARD5, TOPREAL1, GOBOARD2, TREES_1, MCART_1, CARD_1, NAT_1, FUNCT_1, ORDINAL4, RCOMP_1, SPPOL_1, PSCOMP_1, NEWTON, STRUCT_0, ZFMISC_1, INCSP_1, JORDAN8, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, NEWTON, RFINSEQ, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5, XXREAL_0;
definitions GOBOARD1, GOBOARD5, TOPREAL1, XBOOLE_0, SEQM_3;
theorems ZFMISC_1, NAT_1, FINSEQ_1, MATRIX_0, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, PSCOMP_1, SPRECT_1, FINSEQ_5, GOBOARD5, SPRECT_2, ABSVALUE, UNIFORM1, SUBSET_1, GOBRD11, GOBOARD2, SPRECT_3, JORDAN5D, XBOOLE_0, XCMPLX_1, XREAL_1, NEWTON, XXREAL_0, PARTFUN1, NAT_D, SEQM_3;
schemes MATRIX_0;
registrations RELAT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, SPRECT_1, NEWTON, VALUED_0, ORDINAL1;
constructors HIDDEN, NEWTON, RFINSEQ, NAT_D, COMPTS_1, GOBOARD2, SPPOL_1, GOBOARD5, PSCOMP_1, GOBOARD1, RELSET_1, REAL_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions GOBOARD1, XBOOLE_0;
theorem
for
G being
Go-board for
p being
Point of
(TOP-REAL 2) for
f being non
empty FinSequence of
(TOP-REAL 2) st
f is_sequence_on G & ex
i,
j being
Nat st
(
[i,j] in Indices G &
p = G * (
i,
j) ) & ( for
i1,
j1,
i2,
j2 being
Nat st
[i1,j1] in Indices G &
[i2,j2] in Indices G &
f /. (len f) = G * (
i1,
j1) &
p = G * (
i2,
j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
f ^ <*p*> is_sequence_on G
definition
let C be
Subset of
(TOP-REAL 2);
let n be
natural Number ;
deffunc H1(
natural Number ,
natural Number )
-> Element of the
carrier of
(TOP-REAL 2) =
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ($1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ($2 - 2)))]|;
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) & len b2 = (2 |^ n) + 3 & len b2 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) holds
b1 = b2
end;