:: Some properties of special polygonal curves
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 22, 1998
:: Copyright (c) 1998 Association of Mizar Users

begin

theorem :: SPRECT_3:1

canceled;

theorem :: SPRECT_3:2

canceled;

theorem :: SPRECT_3:3

canceled;

theorem :: SPRECT_3:4

canceled;

theorem :: SPRECT_3:5

canceled;

theorem :: SPRECT_3:6

canceled;

theorem :: SPRECT_3:7

canceled;

theorem :: SPRECT_3:8

canceled;

theorem :: SPRECT_3:9

canceled;

theorem :: SPRECT_3:10

canceled;

theorem :: SPRECT_3:11

for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)

proof end;

theorem Th12: :: SPRECT_3:12

for a, b, c, d being set holds Indices (a,b ][ c,d) = {[1,1],[1,2],[2,1],[2,2]}

proof end;

begin

theorem Th13: :: SPRECT_3:13

for n being Element of NAT
for p, q being Point of
for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q

proof end;

theorem Th14: :: SPRECT_3:14

for n being Element of NAT
for p, q being Point of
for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds
p = q

proof end;

theorem :: SPRECT_3:15

for n being Element of NAT
for p, q being Point of st p = (1 / 2) * (p + q) holds
p = q

proof end;

theorem Th16: :: SPRECT_3:16

for n being Element of NAT
for p, q, r being Point of st q in LSeg p,r & r in LSeg p,q holds
q = r

proof end;

begin

theorem Th17: :: SPRECT_3:17

for A being non empty Subset of
for p being Element of
for r being Real st A = Ball p,r holds
A is connected

proof end;

theorem Th18: :: SPRECT_3:18

for A, B being Subset of st A is open & B is_a_component_of A holds
B is open

proof end;

theorem :: SPRECT_3:19

canceled;

theorem :: SPRECT_3:20

canceled;

theorem :: SPRECT_3:21

for p, q, r, s being Point of st LSeg p,q is horizontal & LSeg r,s is horizontal & LSeg p,q meets LSeg r,s holds
p `2 = r `2

proof end;

theorem :: SPRECT_3:22

for p, q, r being Point of st LSeg p,q is vertical & LSeg q,r is horizontal holds
(LSeg p,q) /\ (LSeg q,r) = {q}

proof end;

theorem :: SPRECT_3:23

for p, q, r, s being Point of st LSeg p,q is horizontal & LSeg s,r is vertical & r in LSeg p,q holds
(LSeg p,q) /\ (LSeg s,r) = {r}

proof end;

begin

theorem :: SPRECT_3:24

for j, k, i being Element of NAT
for G being Go-board st 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G holds
(G * i,j) `2 <= (G * i,k) `2

proof end;

theorem :: SPRECT_3:25

for j, i, k being Element of NAT
for G being Go-board st 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G holds
(G * i,j) `1 <= (G * k,j) `1

proof end;

theorem Th26: :: SPRECT_3:26

for C being Subset of holds LSeg (NW-corner C),(NE-corner C) c= L~ (SpStSeq C)

proof end;

theorem :: SPRECT_3:27

canceled;

theorem Th28: :: SPRECT_3:28

for C being non empty compact Subset of holds N-min C in LSeg (NW-corner C),(NE-corner C)

proof end;

theorem :: SPRECT_3:29

for C being Subset of holds LSeg (NW-corner C),(NE-corner C) is horizontal

proof end;

theorem :: SPRECT_3:30

canceled;

theorem :: SPRECT_3:31

for g being FinSequence of
for p being Point of st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg p,(g /. 1)) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq

proof end;

theorem :: SPRECT_3:32

canceled;

theorem :: SPRECT_3:33

for j being Element of NAT
for f being S-Sequence_in_R2
for p being Point of st 1 < j & j <= len f & p in L~ (mid f,1,j) holds
LE p,f /. j, L~ f,f /. 1,f /. (len f)

proof end;

theorem :: SPRECT_3:34

for i, j being Element of NAT
for h being FinSequence of st i in dom h & j in dom h holds
L~ (mid h,i,j) c= L~ h

proof end;

theorem :: SPRECT_3:35

for i, j being Element of NAT st 1 <= i & i < j holds
for f being FinSequence of st j <= len f holds
L~ (mid f,i,j) = (LSeg f,i) \/ (L~ (mid f,(i + 1),j))

proof end;

theorem :: SPRECT_3:36

for i, j being Element of NAT
for f being FinSequence of st 1 <= i & i < j & j <= len f holds
L~ (mid f,i,j) = (L~ (mid f,i,(j -' 1))) \/ (LSeg f,(j -' 1))

proof end;

theorem :: SPRECT_3:37

canceled;

theorem :: SPRECT_3:38

for f, g being FinSequence of st f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg (f /. (len f)),(g /. 1)) /\ (L~ f) = {(f /. (len f))} & (LSeg (f /. (len f)),(g /. 1)) /\ (L~ g) = {(g /. 1)} holds
f ^ g is being_S-Seq

proof end;

theorem :: SPRECT_3:39

for f being FinSequence of
for p being Point of st p in L~ f holds
(R_Cut f,p) /. 1 = f /. 1

proof end;

theorem :: SPRECT_3:40

for j being Element of NAT
for f being S-Sequence_in_R2
for p, q being Point of st 1 <= j & j < len f & p in LSeg f,j & q in LSeg (f /. j),p holds
LE q,p, L~ f,f /. 1,f /. (len f)

proof end;

begin

theorem Th41: :: SPRECT_3:41

for f being non constant standard special_circular_sequence holds
( LeftComp f is open & RightComp f is open )

proof end;

registration

let f be non constant standard special_circular_sequence;
cluster L~ f -> non horizontal non vertical ;
coherence
( not L~ f is vertical & not L~ f is horizontal )

proof end;

cluster LeftComp f -> being_Region ;
coherence
LeftComp f is being_Region

proof end;

cluster RightComp f -> being_Region ;
coherence
RightComp f is being_Region

proof end;

end;

theorem Th42: :: SPRECT_3:42

for f being non constant standard special_circular_sequence holds RightComp f misses L~ f

proof end;

theorem Th43: :: SPRECT_3:43

for f being non constant standard special_circular_sequence holds LeftComp f misses L~ f

proof end;

theorem Th44: :: SPRECT_3:44

for f being non constant standard special_circular_sequence holds i_w_n f < i_e_n f

proof end;

theorem Th45: :: SPRECT_3:45

for f being non constant standard special_circular_sequence ex i being Element of NAT st
( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * i,(width (GoB f)) )

proof end;

theorem Th46: :: SPRECT_3:46

for i being Element of NAT
for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * i,(width (GoB f)) & f /. 1 = N-min (L~ f) holds
( f /. 2 = (GoB f) * (i + 1),(width (GoB f)) & f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) )

proof end;

theorem :: SPRECT_3:47

for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid f,i,j) & not i = 1 holds
j = len f

proof end;

theorem :: SPRECT_3:48

for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f))

proof end;

begin

theorem Th49: :: SPRECT_3:49

for f being rectangular FinSequence of
for p being Point of holds
( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )

proof end;

registration

cluster rectangular FinSequence of the carrier of (TOP-REAL 2);
existence
ex b₁ being special_circular_sequence st b₁ is rectangular

proof end;

end;

theorem Th50: :: SPRECT_3:50

for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L~ f meets L~ g

proof end;

theorem Th51: :: SPRECT_3:51

for f being rectangular special_circular_sequence holds SpStSeq (L~ f) = f

proof end;

theorem Th52: :: SPRECT_3:52

for f being rectangular special_circular_sequence holds L~ f = { p where p is Point of : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }

proof end;

theorem Th53: :: SPRECT_3:53

for f being rectangular special_circular_sequence holds GoB f = (f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)

proof end;

theorem Th54: :: SPRECT_3:54

for f being rectangular special_circular_sequence holds
( LeftComp f = { p where p is Point of : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )

proof end;

registration

cluster rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2);
existence
ex b₁ being rectangular special_circular_sequence st b₁ is clockwise_oriented

proof end;

end;

registration

cluster rectangular -> rectangular clockwise_oriented FinSequence of the carrier of (TOP-REAL 2);
coherence
for b₁ being rectangular special_circular_sequence holds b₁ is clockwise_oriented

proof end;

end;

theorem :: SPRECT_3:55

for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point (L~ g),(g /. 1),(g /. (len g)),(L~ f) <> NW-corner (L~ f)

proof end;

theorem :: SPRECT_3:56

for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point (L~ g),(g /. 1),(g /. (len g)),(L~ f) <> SE-corner (L~ f)

proof end;

theorem Th57: :: SPRECT_3:57

for f being rectangular special_circular_sequence
for p being Point of st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f

proof end;

theorem :: SPRECT_3:58

for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp (SpStSeq (L~ f)) c= LeftComp f

proof end;

begin

theorem Th59: :: SPRECT_3:59

for f being FinSequence of
for p, q being Point of holds
( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

proof end;

theorem Th60: :: SPRECT_3:60

for f being rectangular FinSequence of
for p being Point of st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds
p in L~ f

proof end;

theorem Th61: :: SPRECT_3:61

for f being FinSequence of
for p, q being Point of
for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f

proof end;

theorem Th62: :: SPRECT_3:62

for i being Element of NAT
for f, g being FinSequence of st g is_in_the_area_of f & i in dom g holds
<*(g /. i)*> is_in_the_area_of f

proof end;

theorem Th63: :: SPRECT_3:63

for f, g being FinSequence of
for p being Point of st g is_in_the_area_of f & p in L~ g holds
<*p*> is_in_the_area_of f

proof end;

theorem Th64: :: SPRECT_3:64

for f being rectangular FinSequence of
for p, q being Point of st not q in L~ f & <*p,q*> is_in_the_area_of f holds
(LSeg p,q) /\ (L~ f) c= {p}

proof end;

theorem :: SPRECT_3:65

for f being rectangular FinSequence of
for p, q being Point of st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds
(LSeg p,q) /\ (L~ f) = {p}

proof end;

theorem Th66: :: SPRECT_3:66

for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
<*((GoB f) * i,j)*> is_in_the_area_of f

proof end;

theorem :: SPRECT_3:67

for g being FinSequence of
for p, q being Point of st <*p,q*> is_in_the_area_of g holds
<*((1 / 2) * (p + q))*> is_in_the_area_of g

proof end;

theorem :: SPRECT_3:68

for f, g being FinSequence of st g is_in_the_area_of f holds
Rev g is_in_the_area_of f

proof end;

theorem :: SPRECT_3:69

for f, g being FinSequence of
for p being Point of st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
R_Cut g,p is_in_the_area_of f

proof end;

theorem :: SPRECT_3:70

for f being non constant standard special_circular_sequence
for g being FinSequence of holds
( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )

proof end;

theorem :: SPRECT_3:71

for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L_Cut g,(Last_Point (L~ g),(g /. 1),(g /. (len g)),(L~ f)) is_in_the_area_of f

proof end;

theorem :: SPRECT_3:72

for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds
Int (cell (GoB f),i,j) misses L~ (SpStSeq (L~ f))

proof end;

theorem :: SPRECT_3:73

for f, g being FinSequence of
for p being Point of st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
L_Cut g,p is_in_the_area_of f

proof end;