:: Gauges and CagesAndrzej Trybulec
:: by Artur Korni{\l}owicz, Robert Milewski, Adam Naumowicz and
::
:: Received September 12, 2000
:: Copyright (c) 2000 Association of Mizar Users
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 :: JORDAN1A:1
canceled;
theorem :: JORDAN1A:2
canceled;
theorem :: JORDAN1A:3
canceled;
theorem :: JORDAN1A:4
canceled;
theorem :: JORDAN1A:5
canceled;
theorem :: JORDAN1A:6
canceled;
theorem :: JORDAN1A:7
canceled;
theorem :: JORDAN1A:8
canceled;
theorem :: JORDAN1A:9
theorem :: JORDAN1A:10
theorem Th11: :: JORDAN1A:11
theorem Th12: :: JORDAN1A:12
theorem Th13: :: JORDAN1A:13
theorem Th14: :: JORDAN1A:14
theorem :: JORDAN1A:15
theorem :: JORDAN1A:16
canceled;
theorem Th17: :: JORDAN1A:17
theorem :: JORDAN1A:18
theorem :: JORDAN1A:19
theorem :: JORDAN1A:20
canceled;
theorem :: JORDAN1A:21
theorem :: JORDAN1A:22
theorem :: JORDAN1A:23
theorem :: JORDAN1A:24
theorem :: JORDAN1A:25
theorem :: JORDAN1A:26
canceled;
theorem :: JORDAN1A:27
canceled;
theorem :: JORDAN1A:28
canceled;
theorem :: JORDAN1A:29
canceled;
theorem :: JORDAN1A:30
canceled;
theorem :: JORDAN1A:31
canceled;
theorem :: JORDAN1A:32
canceled;
theorem :: JORDAN1A:33
canceled;
theorem :: JORDAN1A:34
canceled;
theorem :: JORDAN1A:35
canceled;
theorem :: JORDAN1A:36
canceled;
theorem :: JORDAN1A:37
theorem :: JORDAN1A:38
theorem Th39: :: JORDAN1A:39
theorem Th40: :: JORDAN1A:40
theorem Th41: :: JORDAN1A:41
theorem Th42: :: JORDAN1A:42
theorem Th43: :: JORDAN1A:43
theorem Th44: :: JORDAN1A:44
theorem Th45: :: JORDAN1A:45
theorem Th46: :: JORDAN1A:46
theorem Th47: :: JORDAN1A:47
theorem Th48: :: JORDAN1A:48
theorem :: JORDAN1A:49
theorem :: JORDAN1A:50
theorem :: JORDAN1A:51
theorem Th52: :: JORDAN1A:52
theorem Th53: :: JORDAN1A:53
theorem Th54: :: JORDAN1A:54
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: :: JORDAN1A:55
theorem Th56: :: JORDAN1A:56
Lm3:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( 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)
;
:: thesis: 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;
:: thesis: verum
end;
Lm4:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( 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) )
;
:: thesis: [(Center (Gauge D,n)),j] in Indices (Gauge D,n)A2:
len (Gauge D,n) = width (Gauge D,n)
by JORDAN8:def 1;
A3:
0 + 1
<= ((len (Gauge D,n)) div 2) + 1
by 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, A3, MATRIX_1:37;
:: thesis: verum
end;
Lm5:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( 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) )
;
:: thesis: [j,(Center (Gauge D,n))] in Indices (Gauge D,n)A2:
len (Gauge D,n) = width (Gauge D,n)
by JORDAN8:def 1;
A3:
0 + 1
<= ((len (Gauge D,n)) div 2) + 1
by 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, A3, MATRIX_1:37;
:: thesis: 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: :: JORDAN1A:57
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 :: JORDAN1A:58
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);
:: thesis: 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 ;
:: thesis: ( [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)
;
:: thesis: ((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
;
:: thesis: verum
end;
Lm12:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( [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)
;
:: thesis: ((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
;
:: thesis: verum
end;
Lm13:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( [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)
;
:: thesis: ((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
;
:: thesis: verum
end;
Lm14:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: 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 ;
:: thesis: ( [(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)
;
:: thesis: ((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
;
:: thesis: verum
end;
theorem :: JORDAN1A:59
theorem :: JORDAN1A:60
theorem Th61: :: JORDAN1A:61
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 :: JORDAN1A:62
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 :: JORDAN1A:63
theorem :: JORDAN1A:64
theorem :: JORDAN1A:65
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 :: JORDAN1A:66
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 :: JORDAN1A:67
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: :: JORDAN1A:68
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 :: JORDAN1A:69
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 :: JORDAN1A:70
theorem :: JORDAN1A:71
theorem Th72: :: JORDAN1A:72
theorem Th73: :: JORDAN1A:73
theorem Th74: :: JORDAN1A:74
theorem Th75: :: JORDAN1A:75
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: :: JORDAN1A:76
theorem Th77: :: JORDAN1A:77
theorem Th78: :: JORDAN1A:78
theorem Th79: :: JORDAN1A:79
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: :: JORDAN1A:80
theorem Th81: :: JORDAN1A:81
theorem Th82: :: JORDAN1A:82
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: :: JORDAN1A:83
theorem Th84: :: JORDAN1A:84
theorem Th85: :: JORDAN1A:85
theorem :: JORDAN1A:86
theorem :: JORDAN1A:87
theorem :: JORDAN1A:88
theorem :: JORDAN1A:89
theorem :: JORDAN1A:90
theorem :: JORDAN1A:91
theorem :: JORDAN1A:92
theorem :: JORDAN1A:93
theorem :: JORDAN1A:94
theorem Th95: :: JORDAN1A:95
theorem Th96: :: JORDAN1A:96
theorem Th97: :: JORDAN1A:97
theorem Th98: :: JORDAN1A:98
theorem Th99: :: JORDAN1A:99
theorem Th100: :: JORDAN1A:100
theorem Th101: :: JORDAN1A:101
theorem Th102: :: JORDAN1A:102
theorem Th103: :: JORDAN1A:103
theorem Th104: :: JORDAN1A:104
theorem Th105: :: JORDAN1A:105
theorem Th106: :: JORDAN1A:106
theorem :: JORDAN1A:107
theorem :: JORDAN1A:108
theorem :: JORDAN1A:109
theorem :: JORDAN1A:110