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;
:: deftheorem defines Center JORDAN1A:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
canceled;
theorem Th17:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
begin
theorem
theorem
theorem
theorem Th52:
theorem Th53:
theorem Th54:
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
theorem Th55:
theorem Th56:
Lm3:
now
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:8;
hence
1
<= Center (Gauge D,n)
;
Center (Gauge D,n) <= len (Gauge D,n)
0 < len (Gauge D,n)
by JORDAN8:13;
then
(len (Gauge D,n)) div 2
< len (Gauge D,n)
by INT_1:83;
hence
Center (Gauge D,n) <= len (Gauge D,n)
by NAT_1:13;
verum
end;
Lm4:
now
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:8;
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:37;
verum
end;
Lm5:
now
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:8;
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:37;
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 Th57:
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
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:56
;
verum
end;
Lm12:
now
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:56
;
verum
end;
Lm13:
now
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:56
.=
(N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
Lm14:
now
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:56
.=
(E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
theorem
theorem
theorem Th61:
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
theorem
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 Th68:
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
theorem
theorem
begin
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
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 Th76:
theorem Th77:
theorem Th78:
theorem Th79:
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 Th80:
theorem Th81:
theorem Th82:
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))
theorem Th83:
theorem Th84:
theorem Th85:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem Th99:
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
theorem Th106:
theorem
theorem
theorem
theorem