:: On Some Points of a Simple Closed Curve. {P}art {II}
:: by Artur Korni{\l}owicz and Adam Grabowski
::
:: Received October 6, 2004
:: Copyright (c) 2004 Association of Mizar Users
Lm1:
for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
theorem Th1: :: JORDAN22:1
theorem Th2: :: JORDAN22:2
theorem :: JORDAN22:3
theorem :: JORDAN22:4
Lm2:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm3:
for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds 1 <= len (Gauge R,n)
theorem Th5: :: JORDAN22:5
theorem Th6: :: JORDAN22:6
theorem Th7: :: JORDAN22:7
theorem Th8: :: JORDAN22:8
for
i,
m,
k,
j being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k &
[i,j] in Indices (Gauge C,k) &
[i,(j + 1)] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),
((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),
((Gauge C,k) * i,(j + 1))
theorem Th9: :: JORDAN22:9
for
m,
k being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k holds
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 1,2)
theorem Th10: :: JORDAN22:10
for
i,
m,
k,
j being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k &
[i,j] in Indices (Gauge C,k) &
[(i + 1),j] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),
((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),
((Gauge C,k) * (i + 1),j)
theorem Th11: :: JORDAN22:11
for
m,
k being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k holds
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 2,1)
theorem :: JORDAN22:12
for
C being
Simple_closed_curve for
i being
Element of
NAT for
r,
t being
real number st
r > 0 &
t > 0 holds
ex
n being
Element of
NAT st
(
i < n &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2) < r &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1) < t )
theorem Th13: :: JORDAN22:13
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = sup (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))
theorem Th14: :: JORDAN22:14
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))
theorem :: JORDAN22:15
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
UMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th13;
theorem :: JORDAN22:16
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
LMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th14;
theorem Th17: :: JORDAN22:17
theorem Th18: :: JORDAN22:18
theorem :: JORDAN22:19
canceled;
theorem :: JORDAN22:20
canceled;
theorem Th21: :: JORDAN22:21
theorem Th22: :: JORDAN22:22
theorem Th23: :: JORDAN22:23
theorem Th24: :: JORDAN22:24
theorem Th25: :: JORDAN22:25
theorem Th26: :: JORDAN22:26
theorem Th27: :: JORDAN22:27
theorem Th28: :: JORDAN22:28
theorem Th29: :: JORDAN22:29
theorem Th30: :: JORDAN22:30
theorem Th31: :: JORDAN22:31
theorem Th32: :: JORDAN22:32
theorem Th33: :: JORDAN22:33
theorem Th34: :: JORDAN22:34
theorem Th35: :: JORDAN22:35
theorem Th36: :: JORDAN22:36
theorem Th37: :: JORDAN22:37
theorem Th38: :: JORDAN22:38
theorem :: JORDAN22:39
theorem :: JORDAN22:40
theorem :: JORDAN22:41
theorem :: JORDAN22:42
theorem :: JORDAN22:43