:: Upper and Lower Sequence on the Cage. Part II
:: by Robert Milewski
::
:: Received September 28, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: JORDAN1G:1
theorem Th2: :: JORDAN1G:2
theorem Th3: :: JORDAN1G:3
theorem Th4: :: JORDAN1G:4
theorem Th5: :: JORDAN1G:5
theorem Th6: :: JORDAN1G:6
theorem Th7: :: JORDAN1G:7
theorem :: JORDAN1G:8
canceled;
theorem :: JORDAN1G:9
canceled;
theorem :: JORDAN1G:10
canceled;
theorem :: JORDAN1G:11
canceled;
theorem :: JORDAN1G:12
canceled;
theorem :: JORDAN1G:13
canceled;
theorem :: JORDAN1G:14
canceled;
theorem :: JORDAN1G:15
canceled;
theorem Th16: :: JORDAN1G:16
theorem :: JORDAN1G:17
theorem Th18: :: JORDAN1G:18
theorem :: JORDAN1G:19
theorem Th20: :: JORDAN1G:20
theorem :: JORDAN1G:21
theorem Th22: :: JORDAN1G:22
theorem :: JORDAN1G:23
theorem Th24: :: JORDAN1G:24
theorem Th25: :: JORDAN1G:25
theorem Th26: :: JORDAN1G:26
theorem Th27: :: JORDAN1G:27
theorem Th28: :: JORDAN1G:28
theorem Th29: :: JORDAN1G:29
theorem Th30: :: JORDAN1G:30
theorem Th31: :: JORDAN1G:31
theorem Th32: :: JORDAN1G:32
theorem Th33: :: JORDAN1G:33
theorem Th34: :: JORDAN1G:34
theorem Th35: :: JORDAN1G:35
theorem Th36: :: JORDAN1G:36
theorem Th37: :: JORDAN1G:37
theorem Th38: :: JORDAN1G:38
theorem Th39: :: JORDAN1G:39
theorem :: JORDAN1G:40
theorem Th41: :: JORDAN1G:41
theorem :: JORDAN1G:42
theorem Th43: :: JORDAN1G:43
theorem :: JORDAN1G:44
theorem Th45: :: JORDAN1G:45
theorem Th46: :: JORDAN1G:46
theorem Th47: :: JORDAN1G:47
theorem Th48: :: JORDAN1G:48
theorem Th49: :: JORDAN1G:49
theorem Th50: :: JORDAN1G:50
theorem Th51: :: JORDAN1G:51
theorem Th52: :: JORDAN1G:52
theorem :: JORDAN1G:53
theorem Th54: :: JORDAN1G:54
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j being
Element of
NAT st 1
<= i &
i <= len (Gauge C,n) & 1
<= j &
j <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,1),
((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n)
theorem Th55: :: JORDAN1G:55
theorem Th56: :: JORDAN1G:56
theorem Th57: :: JORDAN1G:57
theorem Th58: :: JORDAN1G:58
for
f being
S-Sequence_in_R2 for
Q being
closed Subset of
(TOP-REAL 2) st
L~ f meets Q & not
f /. 1
in Q &
First_Point (L~ f),
(f /. 1),
(f /. (len f)),
Q in rng f holds
(L~ (mid f,1,((First_Point (L~ f),(f /. 1),(f /. (len f)),Q) .. f))) /\ Q = {(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)}
theorem Th59: :: JORDAN1G:59
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
k being
Element of
NAT st 1
<= k &
k < (First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Upper_Seq C,n) holds
((Upper_Seq C,n) /. k) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
theorem Th60: :: JORDAN1G:60
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
k being
Nat st 1
<= k &
k < (First_Point (L~ (Rev (Lower_Seq C,n))),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Rev (Lower_Seq C,n)) holds
((Rev (Lower_Seq C,n)) /. k) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
theorem Th61: :: JORDAN1G:61
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
q being
Point of
(TOP-REAL 2) st
q in rng (mid (Upper_Seq C,n),2,((First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Upper_Seq C,n))) holds
q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
theorem Th62: :: JORDAN1G:62
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
(First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2 > (Last_Point (L~ (Lower_Seq C,n)),(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2
theorem Th63: :: JORDAN1G:63
theorem Th64: :: JORDAN1G:64
theorem :: JORDAN1G:65
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
i,
j being
Element of
NAT st 1
<= i &
i <= len (Gauge C,n) & 1
<= j &
j <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,1),
((Gauge C,n) * i,j) meets Lower_Arc (L~ (Cage C,n))