begin
3 = (2 * 1) + 1
;
then Lm1:
3 div 2 = 1
by NAT_D:def 1;
1 = (2 * 0) + 1
;
then Lm2:
1 div 2 = 0
by NAT_D:def 1;
begin
begin
begin
theorem Th33:
for
m,
n,
i,
j being
Element of
NAT for
D being non
empty Subset of
(TOP-REAL 2) st
m <= n & 1
< i &
i < len (Gauge (D,m)) & 1
< j &
j < width (Gauge (D,m)) holds
for
i1,
j1 being
Element of
NAT st
i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 &
j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
(Gauge (D,m)) * (
i,
j)
= (Gauge (D,n)) * (
i1,
j1)
Lm3:
now for D being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )
let D be non
empty Subset of
(TOP-REAL 2);
for n being Element of NAT holds
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )let n be
Element of
NAT ;
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )set G =
Gauge (
D,
n);
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1
by XREAL_1:6;
hence
1
<= Center (Gauge (D,n))
;
Center (Gauge (D,n)) <= len (Gauge (D,n))
0 < len (Gauge (D,n))
by JORDAN8:10;
then
(len (Gauge (D,n))) div 2
< len (Gauge (D,n))
by INT_1:56;
hence
Center (Gauge (D,n)) <= len (Gauge (D,n))
by NAT_1:13;
verum
end;
Lm4:
now for D being non empty Subset of (TOP-REAL 2)
for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))let n,
j be
Element of
NAT ;
( 1 <= j & j <= len (Gauge (D,n)) implies [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) )set G =
Gauge (
D,
n);
assume A1:
( 1
<= j &
j <= len (Gauge (D,n)) )
;
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))A2:
(
len (Gauge (D,n)) = width (Gauge (D,n)) &
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1 )
by JORDAN8:def 1, XREAL_1:6;
Center (Gauge (D,n)) <= len (Gauge (D,n))
by Lm3;
hence
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))
by A1, A2, MATRIX_1:36;
verum
end;
Lm5:
now for D being non empty Subset of (TOP-REAL 2)
for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))let n,
j be
Element of
NAT ;
( 1 <= j & j <= len (Gauge (D,n)) implies [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) )set G =
Gauge (
D,
n);
assume A1:
( 1
<= j &
j <= len (Gauge (D,n)) )
;
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))A2:
(
len (Gauge (D,n)) = width (Gauge (D,n)) &
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1 )
by JORDAN8:def 1, XREAL_1:6;
Center (Gauge (D,n)) <= len (Gauge (D,n))
by Lm3;
hence
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))
by A1, A2, MATRIX_1:36;
verum
end;
Lm6:
for n being Element of NAT
for D being non empty Subset of (TOP-REAL 2)
for w being real number st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2
theorem Th36:
for
i,
n,
j,
m being
Element of
NAT for
D being non
empty Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (D,n)) & 1
<= j &
j <= len (Gauge (D,m)) & ( (
n > 0 &
m > 0 ) or (
n = 0 &
m = 0 ) ) holds
((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1
theorem
for
i,
n,
j,
m being
Element of
NAT for
D being non
empty Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (D,n)) & 1
<= j &
j <= len (Gauge (D,m)) & ( (
n > 0 &
m > 0 ) or (
n = 0 &
m = 0 ) ) holds
((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2
Lm11:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Element of NAT st [i,1] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Element of NAT st [i,1] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))let n,
i be
Element of
NAT ;
( [i,1] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[i,1] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (i,1)) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (1 - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))
by EUCLID:52
;
verum
end;
Lm12:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Element of NAT st [1,i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Element of NAT st [1,i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))let n,
i be
Element of
NAT ;
( [1,i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[1,i] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (1,i)) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))
by EUCLID:52
;
verum
end;
Lm13:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Element of NAT st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Element of NAT st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))let n,
i be
Element of
NAT ;
( [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[i,(len (Gauge (D,n)))] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))
by EUCLID:52
.=
(N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
Lm14:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Element of NAT st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Element of NAT st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))let n,
i be
Element of
NAT ;
( [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[(len (Gauge (D,n))),i] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))
by EUCLID:52
.=
(E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
theorem Th40:
for
i,
n,
j,
m being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (E,n)) & 1
<= j &
j <= len (Gauge (E,m)) &
m <= n holds
((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2
theorem
for
i,
n,
j,
m being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (E,n)) & 1
<= j &
j <= len (Gauge (E,m)) &
m <= n holds
((Gauge (E,n)) * ((len (Gauge (E,n))),i)) `1 <= ((Gauge (E,m)) * ((len (Gauge (E,m))),j)) `1
theorem
for
m,
n being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n holds
LSeg (
((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
theorem
for
m,
n,
j being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
theorem
for
m,
n,
j being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
theorem Th47:
for
m,
n,
i,
j being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 1
< i &
i + 1
< len (Gauge (E,m)) & 1
< j &
j + 1
< width (Gauge (E,m)) holds
for
i1,
j1 being
Element of
NAT st
((2 |^ (n -' m)) * (i - 2)) + 2
<= i1 &
i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 &
((2 |^ (n -' m)) * (j - 2)) + 2
<= j1 &
j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds
cell (
(Gauge (E,n)),
i1,
j1)
c= cell (
(Gauge (E,m)),
i,
j)
theorem
for
m,
n,
i,
j being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 3
<= i &
i < len (Gauge (E,m)) & 1
< j &
j + 1
< width (Gauge (E,m)) holds
for
i1,
j1 being
Element of
NAT st
i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 &
j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
cell (
(Gauge (E,n)),
(i1 -' 1),
j1)
c= cell (
(Gauge (E,m)),
(i -' 1),
j)
begin
Lm15:
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )
Lm16:
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )
Lm17:
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )
theorem Th58:
for
k,
n,
t being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k <= len (Cage (C,n)) & 1
<= t &
t <= len (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
t,
(width (Gauge (C,n)))) holds
(Cage (C,n)) /. k in N-most (L~ (Cage (C,n)))
theorem Th61:
for
k,
n,
t being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k <= len (Cage (C,n)) & 1
<= t &
t <= width (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
(len (Gauge (C,n))),
t) holds
(Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))