:: Properties of the External Approximation of Jordan's Curve
:: by Artur Korni{\l}owicz
::
:: Received June 24, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: JORDAN10:1
for
k,
n,
i,
j being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage C,n) &
[i,j] in Indices (Gauge C,n) &
[i,(j + 1)] in Indices (Gauge C,n) &
(Cage C,n) /. k = (Gauge C,n) * i,
j &
(Cage C,n) /. (k + 1) = (Gauge C,n) * i,
(j + 1) holds
i < len (Gauge C,n)
theorem Th2: :: JORDAN10:2
for
k,
n,
i,
j being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage C,n) &
[i,j] in Indices (Gauge C,n) &
[i,(j + 1)] in Indices (Gauge C,n) &
(Cage C,n) /. k = (Gauge C,n) * i,
(j + 1) &
(Cage C,n) /. (k + 1) = (Gauge C,n) * i,
j holds
i > 1
theorem Th3: :: JORDAN10:3
for
k,
n,
i,
j being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage C,n) &
[i,j] in Indices (Gauge C,n) &
[(i + 1),j] in Indices (Gauge C,n) &
(Cage C,n) /. k = (Gauge C,n) * i,
j &
(Cage C,n) /. (k + 1) = (Gauge C,n) * (i + 1),
j holds
j > 1
theorem Th4: :: JORDAN10:4
for
k,
n,
i,
j being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k + 1
<= len (Cage C,n) &
[i,j] in Indices (Gauge C,n) &
[(i + 1),j] in Indices (Gauge C,n) &
(Cage C,n) /. k = (Gauge C,n) * (i + 1),
j &
(Cage C,n) /. (k + 1) = (Gauge C,n) * i,
j holds
j < width (Gauge C,n)
theorem Th5: :: JORDAN10:5
theorem Th6: :: JORDAN10:6
theorem Th7: :: JORDAN10:7
theorem Th8: :: JORDAN10:8
theorem Th9: :: JORDAN10:9
theorem Th10: :: JORDAN10:10
theorem Th11: :: JORDAN10:11
theorem Th12: :: JORDAN10:12
theorem Th13: :: JORDAN10:13
:: deftheorem defines UBD-Family JORDAN10:def 1 :
:: deftheorem defines BDD-Family JORDAN10:def 2 :
theorem Th14: :: JORDAN10:14
theorem Th15: :: JORDAN10:15
theorem Th16: :: JORDAN10:16
theorem Th17: :: JORDAN10:17
theorem Th18: :: JORDAN10:18
theorem Th19: :: JORDAN10:19
theorem Th20: :: JORDAN10:20
theorem :: JORDAN10:21