:: Some Remarks on Clockwise Oriented Sequences on Go-boards
:: by Adam Naumowicz and Robert Milewski
::
:: Received March 1, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem :: JORDAN1I:1
canceled;
theorem :: JORDAN1I:2
canceled;
theorem Th3: :: JORDAN1I:3
theorem Th4: :: JORDAN1I:4
theorem Th5: :: JORDAN1I:5
theorem :: JORDAN1I:6
theorem Th7: :: JORDAN1I:7
theorem :: JORDAN1I:8
theorem :: JORDAN1I:9
theorem :: JORDAN1I:10
theorem Th11: :: JORDAN1I:11
theorem Th12: :: JORDAN1I:12
theorem Th13: :: JORDAN1I:13
theorem Th14: :: JORDAN1I:14
theorem Th15: :: JORDAN1I:15
theorem Th16: :: JORDAN1I:16
theorem Th17: :: JORDAN1I:17
theorem Th18: :: JORDAN1I:18
theorem Th19: :: JORDAN1I:19
theorem Th20: :: JORDAN1I:20
theorem Th21: :: JORDAN1I:21
theorem Th22: :: JORDAN1I:22
theorem Th23: :: JORDAN1I:23
theorem :: JORDAN1I:24
theorem Th25: :: JORDAN1I:25
theorem Th26: :: JORDAN1I:26
theorem :: JORDAN1I:27
theorem :: JORDAN1I:28
theorem :: JORDAN1I:29
theorem :: JORDAN1I:30
for
i,
k being
Element of
NAT for
C being non
empty being_simple_closed_curve compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
p being
Point of
(TOP-REAL 2) st
p `1 = ((W-bound C) + (E-bound C)) / 2 &
i > 0 & 1
<= k &
k <= width (Gauge C,i) &
(Gauge C,i) * (Center (Gauge C,i)),
k in Upper_Arc (L~ (Cage C,i)) &
p `2 = sup (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (Lower_Arc (L~ (Cage C,i))))) holds
ex
j being
Element of
NAT st
( 1
<= j &
j <= width (Gauge C,i) &
p = (Gauge C,i) * (Center (Gauge C,i)),
j )