:: Properties of the Upper and Lower Sequence on the Cage
:: by Robert Milewski
::
:: Received August 1, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem :: JORDAN15:1
theorem :: JORDAN15:2
theorem Th3: :: JORDAN15:3
theorem Th4: :: JORDAN15:4
theorem :: JORDAN15:5
canceled;
theorem :: JORDAN15:6
canceled;
theorem Th7: :: JORDAN15:7
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
Element of
NAT st 1
<= i &
i <= len G & 1
<= j &
j <= j1 &
j1 <= k1 &
k1 <= k &
k <= width G holds
LSeg (G * i,j1),
(G * i,k1) c= LSeg (G * i,j),
(G * i,k)
theorem Th8: :: JORDAN15:8
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
Element of
NAT st 1
<= i &
i <= width G & 1
<= j &
j <= j1 &
j1 <= k1 &
k1 <= k &
k <= len G holds
LSeg (G * j1,i),
(G * k1,i) c= LSeg (G * j,i),
(G * k,i)
theorem :: JORDAN15:9
theorem :: JORDAN15:10
theorem Th11: :: JORDAN15:11
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Lower_Seq C,n) holds
ex
j1 being
Element of
NAT st
(
j <= j1 &
j1 <= k &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
theorem :: JORDAN15:12
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
k in L~ (Upper_Seq C,n) holds
ex
k1 being
Element of
NAT st
(
j <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k1)} )
theorem Th13: :: JORDAN15:13
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Lower_Seq C,n) &
(Gauge C,n) * i,
k in L~ (Upper_Seq C,n) holds
ex
j1,
k1 being
Element of
NAT st
(
j <= j1 &
j1 <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k1)} )
theorem :: JORDAN15:14
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Lower_Seq C,n) holds
ex
j1 being
Element of
NAT st
(
j <= j1 &
j1 <= k &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j1,i)} )
theorem Th15: :: JORDAN15:15
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * k,
i in L~ (Upper_Seq C,n) holds
ex
k1 being
Element of
NAT st
(
j <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k1,i)} )
theorem Th16: :: JORDAN15:16
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Lower_Seq C,n) &
(Gauge C,n) * k,
i in L~ (Upper_Seq C,n) holds
ex
j1,
k1 being
Element of
NAT st
(
j <= j1 &
j1 <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j1,i)} &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k1,i)} )
theorem :: JORDAN15:17
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Upper_Seq C,n) holds
ex
j1 being
Element of
NAT st
(
j <= j1 &
j1 <= k &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,j1)} )
theorem :: JORDAN15:18
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
k in L~ (Lower_Seq C,n) holds
ex
k1 being
Element of
NAT st
(
j <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,k1)} )
theorem :: JORDAN15:19
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 &
j <= k &
k <= width (Gauge C,n) &
(Gauge C,n) * i,
j in L~ (Upper_Seq C,n) &
(Gauge C,n) * i,
k in L~ (Lower_Seq C,n) holds
ex
j1,
k1 being
Element of
NAT st
(
j <= j1 &
j1 <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,j1)} &
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,k1)} )
theorem Th20: :: JORDAN15:20
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Upper_Seq C,n) holds
ex
j1 being
Element of
NAT st
(
j <= j1 &
j1 <= k &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j1,i)} )
theorem :: JORDAN15:21
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * k,
i in L~ (Lower_Seq C,n) holds
ex
k1 being
Element of
NAT st
(
j <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k1,i)} )
theorem Th22: :: JORDAN15:22
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
<= j &
j <= k &
k <= len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * k,
i in L~ (Lower_Seq C,n) holds
ex
j1,
k1 being
Element of
NAT st
(
j <= j1 &
j1 <= k1 &
k1 <= k &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j1,i)} &
(LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k1,i)} )
theorem Th23: :: JORDAN15:23
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) &
(Gauge C,n) * i,
k in L~ (Upper_Seq C,n) &
(Gauge C,n) * i,
j in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th24: :: JORDAN15:24
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) &
(Gauge C,n) * i,
k in L~ (Upper_Seq C,n) &
(Gauge C,n) * i,
j in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Upper_Arc C
theorem Th25: :: JORDAN15:25
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 &
(Gauge C,n) * i,
k in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * i,
j in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th26: :: JORDAN15:26
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 &
(Gauge C,n) * i,
k in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * i,
j in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Upper_Arc C
theorem :: JORDAN15:27
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)) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Lower_Arc (L~ (Cage C,(n + 1))) 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 :: JORDAN15:28
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)) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Lower_Arc (L~ (Cage C,(n + 1))) 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 Th29: :: JORDAN15:29
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
< j &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * k,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * j,
i in L~ (Lower_Seq C,n) holds
j <> k
theorem Th30: :: JORDAN15:30
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k,i)} &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j,i)} holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th31: :: JORDAN15:31
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k,i)} &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j,i)} holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem Th32: :: JORDAN15:32
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * k,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * j,
i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th33: :: JORDAN15:33
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * k,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * j,
i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem Th34: :: JORDAN15:34
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
n > 0 &
(Gauge C,n) * k,
i in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * j,
i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th35: :: JORDAN15:35
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
n > 0 &
(Gauge C,n) * k,
i in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * j,
i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem :: JORDAN15:36
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 < len (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * k,
(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * j,
(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),
((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
theorem :: JORDAN15:37
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 < len (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * k,
(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * j,
(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),
((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Upper_Arc C
theorem Th38: :: JORDAN15:38
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j,i)} &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k,i)} holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th39: :: JORDAN15:39
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j,i)} &
(LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k,i)} holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem Th40: :: JORDAN15:40
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * k,
i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th41: :: JORDAN15:41
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
(Gauge C,n) * j,
i in L~ (Upper_Seq C,n) &
(Gauge C,n) * k,
i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem Th42: :: JORDAN15:42
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
n > 0 &
(Gauge C,n) * j,
i in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * k,
i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Lower_Arc C
theorem Th43: :: JORDAN15:43
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
NAT st 1
< j &
j <= k &
k < len (Gauge C,n) & 1
<= i &
i <= width (Gauge C,n) &
n > 0 &
(Gauge C,n) * j,
i in Upper_Arc (L~ (Cage C,n)) &
(Gauge C,n) * k,
i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),
((Gauge C,n) * k,i) meets Upper_Arc C
theorem :: JORDAN15:44
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 < len (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * j,
(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * k,
(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),
((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
theorem :: JORDAN15:45
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 < len (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * j,
(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * k,
(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),
((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Upper_Arc C
theorem Th46: :: JORDAN15:46
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i1 &
i1 <= i2 &
i2 < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
theorem Th47: :: JORDAN15:47
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i1 &
i1 <= i2 &
i2 < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
theorem Th48: :: JORDAN15:48
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i2 &
i2 <= i1 &
i1 < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
theorem Th49: :: JORDAN15:49
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i2 &
i2 <= i1 &
i1 < len (Gauge C,n) & 1
<= j &
j <= k &
k <= width (Gauge C,n) &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} &
((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
theorem Th50: :: JORDAN15:50
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i1 &
i1 < len (Gauge C,(n + 1)) & 1
< i2 &
i2 < len (Gauge C,(n + 1)) & 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * i1,
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * i2,
j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Upper_Arc C
theorem Th51: :: JORDAN15:51
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
NAT st 1
< i1 &
i1 < len (Gauge C,(n + 1)) & 1
< i2 &
i2 < len (Gauge C,(n + 1)) & 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * i1,
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * i2,
j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Lower_Arc C
theorem :: JORDAN15:52
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)) & 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * i,
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) \/ (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k),((Gauge C,(n + 1)) * i,k)) meets Upper_Arc C
theorem :: JORDAN15:53
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)) & 1
<= j &
j <= k &
k <= width (Gauge C,(n + 1)) &
(Gauge C,(n + 1)) * i,
k in Upper_Arc (L~ (Cage C,(n + 1))) &
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) \/ (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k),((Gauge C,(n + 1)) * i,k)) meets Lower_Arc C