:: Gauges and Cages. { P } art { II }
:: by Artur Korni{\l}owicz and Robert Milewski
::
:: Received November 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
1 = (2 * 0 ) + 1
;
then Lm1:
1 div 2 = 0
by NAT_D:def 1;
2 = (2 * 1) + 0
;
then Lm2:
2 div 2 = 1
by NAT_D:def 1;
Lm3:
for x, A, B, C, D being set holds
( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) )
Lm4:
for A, B, C, D being set holds union {A,B,C,D} = ((A \/ B) \/ C) \/ D
theorem Th1: :: JORDAN1D:1
theorem Th2: :: JORDAN1D:2
theorem :: JORDAN1D:3
canceled;
theorem :: JORDAN1D:4
canceled;
theorem :: JORDAN1D:5
canceled;
theorem :: JORDAN1D:6
canceled;
Lm10:
for m, i being Element of NAT
for x being real number st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
Lm11:
for m being Element of NAT st 2 <= m holds
1 <= (2 * m) -' 2
Lm12:
for m being Element of NAT st 1 <= m holds
1 <= (2 * m) -' 1
Lm13:
for m, i being Element of NAT st m < (2 |^ i) + 3 holds
(2 * m) -' 2 < (2 |^ (i + 1)) + 3
theorem Th7: :: JORDAN1D:7
for
m,
i,
a,
b being
Element of
NAT for
D being non
empty Subset of
(TOP-REAL 2) st 2
<= m &
m < len (Gauge D,i) & 1
<= a &
a <= len (Gauge D,i) & 1
<= b &
b <= len (Gauge D,(i + 1)) holds
((Gauge D,i) * m,a) `1 = ((Gauge D,(i + 1)) * ((2 * m) -' 2),b) `1
theorem Th8: :: JORDAN1D:8
for
n,
i,
a,
b being
Element of
NAT for
D being non
empty Subset of
(TOP-REAL 2) st 2
<= n &
n < len (Gauge D,i) & 1
<= a &
a <= len (Gauge D,i) & 1
<= b &
b <= len (Gauge D,(i + 1)) holds
((Gauge D,i) * a,n) `2 = ((Gauge D,(i + 1)) * b,((2 * n) -' 2)) `2
Lm15:
for m, i being Element of NAT
for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge D,i) holds
(2 * m) -' 1 < len (Gauge D,(i + 1))
theorem Th9: :: JORDAN1D:9
for
m,
i,
n being
Element of
NAT for
D being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 2
<= m &
m + 1
< len (Gauge D,i) & 2
<= n &
n + 1
< len (Gauge D,i) holds
cell (Gauge D,i),
m,
n = (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
theorem :: JORDAN1D:10
for
m,
i,
n being
Element of
NAT for
D being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
k being
Element of
NAT st 2
<= m &
m + 1
< len (Gauge D,i) & 2
<= n &
n + 1
< len (Gauge D,i) holds
cell (Gauge D,i),
m,
n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
theorem Th11: :: JORDAN1D:11
theorem :: JORDAN1D:12
theorem Th13: :: JORDAN1D:13
theorem :: JORDAN1D:14
theorem Th15: :: JORDAN1D:15
theorem :: JORDAN1D:16
theorem Th17: :: JORDAN1D:17
theorem :: JORDAN1D:18
theorem Th19: :: JORDAN1D:19
theorem :: JORDAN1D:20
theorem Th21: :: JORDAN1D:21
theorem :: JORDAN1D:22
theorem Th23: :: JORDAN1D:23
theorem :: JORDAN1D:24
theorem Th25: :: JORDAN1D:25
theorem :: JORDAN1D:26
theorem :: JORDAN1D:27
theorem Th28: :: JORDAN1D:28
theorem :: JORDAN1D:29
theorem :: JORDAN1D:30
theorem Th31: :: JORDAN1D:31
theorem :: JORDAN1D:32
theorem :: JORDAN1D:33
theorem Th34: :: JORDAN1D:34
theorem :: JORDAN1D:35
theorem :: JORDAN1D:36