begin
begin
Lm1:
RealOrd is_reflexive_in REAL
Lm2:
RealOrd is_antisymmetric_in REAL
Lm3:
RealOrd is_transitive_in REAL
Lm4:
RealOrd is_connected_in REAL
begin
begin
begin
theorem Th37:
for
m,
n,
i,
j being
Element of
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
Element of
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,
n,
i,
j being
Element of
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
Element of
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) )
begin
begin
theorem
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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
Element of
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))