:: Upper and Lower Sequence on the Cage, Upper and Lower Arcs
:: by Robert Milewski
::
:: Received April 5, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: JORDAN1J:1
theorem Th2: :: JORDAN1J:2
theorem Th3: :: JORDAN1J:3
theorem Th4: :: JORDAN1J:4
theorem :: JORDAN1J:5
theorem :: JORDAN1J:6
theorem Th7: :: JORDAN1J:7
theorem :: JORDAN1J:8
theorem :: JORDAN1J:9
theorem :: JORDAN1J:10
theorem :: JORDAN1J:11
theorem Th12: :: JORDAN1J:12
theorem :: JORDAN1J:13
theorem :: JORDAN1J:14
theorem Th15: :: JORDAN1J:15
theorem Th16: :: JORDAN1J:16
theorem Th17: :: JORDAN1J:17
theorem Th18: :: JORDAN1J:18
theorem Th19: :: JORDAN1J:19
theorem Th20: :: JORDAN1J:20
theorem Th21: :: JORDAN1J:21
theorem Th22: :: JORDAN1J:22
theorem Th23: :: JORDAN1J:23
theorem Th24: :: JORDAN1J:24
theorem Th25: :: JORDAN1J:25
theorem Th26: :: JORDAN1J:26
theorem :: JORDAN1J:27
theorem :: JORDAN1J:28
theorem :: JORDAN1J:29
theorem :: JORDAN1J:30
theorem :: JORDAN1J:31
theorem :: JORDAN1J:32
theorem Th33: :: JORDAN1J:33
theorem :: JORDAN1J:34
theorem Th35: :: JORDAN1J:35
theorem Th36: :: JORDAN1J:36
theorem Th37: :: JORDAN1J:37
theorem Th38: :: JORDAN1J:38
theorem Th39: :: JORDAN1J:39
theorem Th40: :: JORDAN1J:40
theorem :: JORDAN1J:41
theorem :: JORDAN1J:42
theorem Th43: :: JORDAN1J:43
theorem Th44: :: JORDAN1J:44
theorem Th45: :: JORDAN1J:45
theorem Th46: :: JORDAN1J:46
theorem :: JORDAN1J:47
theorem :: JORDAN1J:48
theorem Th49: :: JORDAN1J:49
theorem Th50: :: JORDAN1J:50
theorem Th51: :: JORDAN1J:51
theorem Th52: :: JORDAN1J:52
for
G being
Go-board for
f being
S-Sequence_in_R2 for
p being
Point of
(TOP-REAL 2) for
k being
Element of
NAT st 1
<= k &
k < p .. f &
f is_sequence_on G &
p in rng f holds
(
left_cell (R_Cut f,p),
k,
G = left_cell f,
k,
G &
right_cell (R_Cut f,p),
k,
G = right_cell f,
k,
G )
theorem Th53: :: JORDAN1J:53
theorem Th54: :: JORDAN1J:54
theorem Th55: :: JORDAN1J:55
theorem Th56: :: JORDAN1J:56
theorem Th57: :: JORDAN1J:57
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
NAT st 1
< i &
i < len (Gauge C,n) & 1
<= j &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
k in L~ (Upper_Seq C,n) &
(Gauge C,n) * i,
j in L~ (Lower_Seq C,n) holds
j <> k
theorem Th58: :: JORDAN1J:58
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< i &
i < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th59: :: JORDAN1J:59
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< i &
i < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Upper_Arc C
theorem Th60: :: JORDAN1J:60
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< i &
i < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
n > 0 &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th61: :: JORDAN1J:61
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< i &
i < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
n > 0 &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Upper_Arc C
theorem :: JORDAN1J:62
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
j being
Element of
NAT st
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Upper_Arc (L~ (Cage C,(n + 1))) & 1
<= j &
j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),
((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
theorem :: JORDAN1J:63
for
n being
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
NAT st 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),
((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
theorem :: JORDAN1J:64
for
n being
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
NAT st 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),
((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Upper_Arc C
theorem :: JORDAN1J:65
theorem :: JORDAN1J:66
theorem :: JORDAN1J:67
theorem :: JORDAN1J:68