environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, RCOMP_1, SPPOL_1, EUCLID, GOBOARD1, PRE_TOPC, SETFAM_1, XBOOLE_0, RELAT_1, FINSEQ_1, TARSKI, FUNCOP_1, FUNCT_1, FUNCT_6, RLTOPSP1, PCOMPS_1, XXREAL_0, CARD_1, METRIC_1, ARYTM_3, ARYTM_1, FINSEQ_2, COMPLEX1, ZFMISC_1, RELAT_2, PARTFUN1, ORDERS_1, FINSET_1, PRE_POLY, ORDINAL2, GOBOARD2, NAT_1, MCART_1, GOBRD13, CARD_3, MATRIX_1, TREES_1, INCSP_1, STRUCT_0, GOBOARD5, CONNSP_1, TOPREAL1, GOBOARD9, TOPS_1, JORDAN3, RFINSEQ, FINSEQ_5, INT_1, NEWTON, JORDAN8, PSCOMP_1, JORDAN2C, FINSEQ_6, SPRECT_2, JORDAN9, JORDAN1H, CONVEX1, XXREAL_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SETFAM_1, ZFMISC_1, SUBSET_1, FINSEQ_6, GOBOARD5, ORDERS_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, FUNCT_1, NAT_1, INT_1, NAT_D, RELAT_1, RELAT_2, RELSET_1, PARTFUN1, NEWTON, FINSET_1, FINSEQ_1, SEQM_3, RVSUM_1, STRUCT_0, FUNCT_6, CARD_3, FUNCOP_1, FINSEQ_2, FINSEQ_5, RFINSEQ, MATRIX_0, MATRIX_1, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, SPRECT_2, TOPREAL1, GOBOARD1, GOBOARD2, JORDAN2C, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN8, GOBRD13, JORDAN9, PRE_POLY;
definitions TARSKI, RELAT_2, ORDERS_1, RELAT_1, XBOOLE_0, SEQM_3;
theorems JORDAN9, GOBOARD5, TOPREAL1, GOBOARD7, GOBOARD1, SPRECT_2, GOBOARD2, FINSEQ_4, ORDERS_1, CARD_1, FINSEQ_3, FUNCT_2, GOBRD13, PSCOMP_1, FINSEQ_1, FUNCT_1, MATRIX_0, RELAT_1, EUCLID, NAT_1, SUBSET_1, GOBRD11, JORDAN1D, ZFMISC_1, RELSET_1, FUNCT_7, TARSKI, CARD_3, FUNCT_6, JORDAN4, JORDAN8, TOPREAL3, GOBRD14, GOBOARD9, SPRECT_4, GOBRD12, SPPOL_2, PRE_TOPC, TOPS_1, SPRECT_3, JORDAN1A, TSEP_1, INT_1, NEWTON, JORDAN5B, JORDAN2C, TOPMETR, RVSUM_1, ABSVALUE, METRIC_1, JORDAN1B, SPRECT_1, FINSEQ_2, JORDAN10, SPPOL_1, CONNSP_1, REVROT_1, XBOOLE_0, XBOOLE_1, XREAL_0, PARTIT_2, XCMPLX_1, PARTFUN1, SETFAM_1, XREAL_1, NAT_2, XXREAL_0, PREPOWER, NAT_D, RLTOPSP1, PRE_POLY, FINSEQ_6, SEQM_3, SEQ_4, XTUPLE_0, RLVECT_1, RLVECT_4;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_6, GENEALG1, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_2, GOBOARD9, WAYBEL_2, SPRECT_1, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8, MATRIX_0, VALUED_0, RELSET_1, RLTOPSP1, PRE_POLY, SEQM_3, CARD_1, JORDAN1, JORDAN2C, NEWTON;
constructors HIDDEN, REAL_1, NEWTON, RFINSEQ, NAT_D, WSIERP_1, TOPS_1, CONNSP_1, TOPREAL4, GOBOARD2, PSCOMP_1, TRIANG_1, GOBOARD9, SPRECT_1, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, BINOP_2, RELSET_1, FUNCSDOM, CONVEX1, PCOMPS_1, SEQ_4, DOMAIN_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, EUCLID, VALUED_1, RLTOPSP1, ORDINAL1, CARD_1;
expansions TARSKI, RELAT_2, XBOOLE_0;
Lm1:
RealOrd is_reflexive_in REAL
;
Lm2:
RealOrd is_antisymmetric_in REAL
Lm3:
RealOrd is_transitive_in REAL
Lm4:
RealOrd is_connected_in REAL
theorem Th37:
for
m,
j,
i,
n being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 1
<= i &
i + 1
<= len (Gauge (C,n)) & 1
<= j &
j + 1
<= width (Gauge (C,n)) holds
ex
i1,
j1 being
Nat st
(
i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] &
j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] &
cell (
(Gauge (C,n)),
i,
j)
c= cell (
(Gauge (C,m)),
i1,
j1) )
theorem Th38:
for
m,
j,
i,
n being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 1
<= i &
i + 1
<= len (Gauge (C,n)) & 1
<= j &
j + 1
<= width (Gauge (C,n)) holds
ex
i1,
j1 being
Nat st
( 1
<= i1 &
i1 + 1
<= len (Gauge (C,m)) & 1
<= j1 &
j1 + 1
<= width (Gauge (C,m)) &
cell (
(Gauge (C,n)),
i,
j)
c= cell (
(Gauge (C,m)),
i1,
j1) )
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[i1,(j1 + 1)] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[(i1 + 1),j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
(i1 + 1),
j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
j1,
i2 being
Nat st
left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[(i2 + 1),j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
(i2 + 1),
j1) &
[i2,j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i2,
j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j2 being
Nat st
left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,(j2 + 1)] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
(j2 + 1)) &
[i1,j2] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
front_left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[i1,(j1 + 1)] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
front_left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[(i1 + 1),j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
(i1 + 1),
j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
j1,
i2 being
Nat st
front_left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[(i2 + 1),j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
(i2 + 1),
j1) &
[i2,j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i2,
j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j2 being
Nat st
front_left_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,(j2 + 1)] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
(j2 + 1)) &
[i1,j2] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
front_right_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[i1,(j1 + 1)] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j1 being
Nat st
front_right_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
j1) &
[(i1 + 1),j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
(i1 + 1),
j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
j1,
i2 being
Nat st
front_right_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[(i2 + 1),j1] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
(i2 + 1),
j1) &
[i2,j1] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i2,
j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n))
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on Gauge (
C,
n) &
len f > 1 holds
for
i1,
j2 being
Nat st
front_right_cell (
f,
((len f) -' 1),
(Gauge (C,n)))
meets C &
[i1,(j2 + 1)] in Indices (Gauge (C,n)) &
f /. ((len f) -' 1) = (Gauge (C,n)) * (
i1,
(j2 + 1)) &
[i1,j2] in Indices (Gauge (C,n)) &
f /. (len f) = (Gauge (C,n)) * (
i1,
j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))