:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received October 22, 1998

:: Copyright (c) 1998-2016 Association of Mizar Users

theorem :: SPRECT_3:1

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)

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 Th3: :: SPRECT_3:3

for n being Nat

for p, q being Point of (TOP-REAL n)

for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds

p = q

for p, q being Point of (TOP-REAL n)

for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds

p = q

proof end;

theorem Th4: :: SPRECT_3:4

for n being Nat

for p, q being Point of (TOP-REAL n)

for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

for p, q being Point of (TOP-REAL n)

for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

proof end;

theorem Th6: :: SPRECT_3:6

for n being Nat

for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds

q = r

for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds

q = r

proof end;

theorem Th7: :: SPRECT_3:7

for A being non empty Subset of (TOP-REAL 2)

for p being Element of (Euclid 2)

for r being Real st A = Ball (p,r) holds

A is connected

for p being Element of (Euclid 2)

for r being Real st A = Ball (p,r) holds

A is connected

proof end;

theorem :: SPRECT_3:9

for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) holds

p `2 = r `2

p `2 = r `2

proof end;

theorem :: SPRECT_3:10

for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & LSeg (q,r) is horizontal holds

(LSeg (p,q)) /\ (LSeg (q,r)) = {q}

(LSeg (p,q)) /\ (LSeg (q,r)) = {q}

proof end;

theorem :: SPRECT_3:11

for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (s,r) is vertical & r in LSeg (p,q) holds

(LSeg (p,q)) /\ (LSeg (s,r)) = {r}

(LSeg (p,q)) /\ (LSeg (s,r)) = {r}

proof end;

theorem :: SPRECT_3:12

for i, j, k being 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

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:13

for i, j, k being 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

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 Th15: :: SPRECT_3:15

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

proof end;

registration

let C be Subset of (TOP-REAL 2);

coherence

LSeg ((NW-corner C),(NE-corner C)) is horizontal

end;
coherence

LSeg ((NW-corner C),(NE-corner C)) is horizontal

proof end;

theorem :: SPRECT_3:16

for g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) 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

for p being Point of (TOP-REAL 2) 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:17

for j being Nat

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2) 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)

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2) 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:18

for i, j being Nat

for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds

L~ (mid (h,i,j)) c= L~ h

for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds

L~ (mid (h,i,j)) c= L~ h

proof end;

theorem :: SPRECT_3:19

for i, j being Nat st 1 <= i & i < j holds

for f being FinSequence of (TOP-REAL 2) st j <= len f holds

L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))

for f being FinSequence of (TOP-REAL 2) st j <= len f holds

L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))

proof end;

theorem :: SPRECT_3:20

for i, j being Nat

for f being FinSequence of (TOP-REAL 2) st 1 <= i & i < j & j <= len f holds

L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))

for f being FinSequence of (TOP-REAL 2) 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:21

for f, g being FinSequence of (TOP-REAL 2) 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

f ^ g is being_S-Seq

proof end;

theorem :: SPRECT_3:22

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

(R_Cut (f,p)) /. 1 = f /. 1

for p being Point of (TOP-REAL 2) st p in L~ f holds

(R_Cut (f,p)) /. 1 = f /. 1

proof end;

theorem :: SPRECT_3:23

for j being Nat

for f being S-Sequence_in_R2

for p, q being Point of (TOP-REAL 2) 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)

for f being S-Sequence_in_R2

for p, q being Point of (TOP-REAL 2) 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;

theorem Th24: :: SPRECT_3:24

for f being non constant standard special_circular_sequence holds

( LeftComp f is open & RightComp f is open )

( LeftComp f is open & RightComp f is open )

proof end;

registration

let f be non constant standard special_circular_sequence;

coherence

( not L~ f is vertical & not L~ f is horizontal )

LeftComp f is being_Region

RightComp f is being_Region

end;
coherence

( not L~ f is vertical & not L~ f is horizontal )

proof end;

coherence LeftComp f is being_Region

proof end;

coherence RightComp f is being_Region

proof end;

theorem Th28: :: SPRECT_3:28

for f being non constant standard special_circular_sequence ex i being Nat st

( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )

( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )

proof end;

theorem Th29: :: SPRECT_3:29

for i being 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)) )

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:30

for i, j being 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

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:31

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))

LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))

proof end;

theorem Th32: :: SPRECT_3:32

for f being rectangular FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) 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) )

for p being Point of (TOP-REAL 2) 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

ex b_{1} being special_circular_sequence st b_{1} is rectangular
end;

cluster V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) non empty Function-like V28() FinSequence-like FinSubsequence-like V241( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular for FinSequence of the U1 of (TOP-REAL 2);

existence ex b

proof end;

theorem Th33: :: SPRECT_3:33

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

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 Th35: :: SPRECT_3:35

for f being rectangular special_circular_sequence holds L~ f = { p where p is Point of (TOP-REAL 2) : ( ( 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 Th36: :: SPRECT_3:36

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

proof end;

theorem Th37: :: SPRECT_3:37

for f being rectangular special_circular_sequence holds

( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )

( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) : ( 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

ex b_{1} being rectangular special_circular_sequence st b_{1} is clockwise_oriented
end;

cluster V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) non empty non trivial V16() Function-like non constant V28() FinSequence-like FinSubsequence-like V241( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);

existence ex b

proof end;

registration

for b_{1} being rectangular special_circular_sequence holds b_{1} is clockwise_oriented
end;

cluster non empty V241( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular -> rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);

coherence for b

proof end;

theorem :: SPRECT_3:38

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)

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:39

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)

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 Th40: :: SPRECT_3:40

for f being rectangular special_circular_sequence

for p being Point of (TOP-REAL 2) 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

for p being Point of (TOP-REAL 2) 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:41

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

LeftComp (SpStSeq (L~ f)) c= LeftComp f

proof end;

theorem Th42: :: SPRECT_3:42

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) holds

( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )

for p, q being Point of (TOP-REAL 2) 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 Th43: :: SPRECT_3:43

for f being rectangular FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) 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

for p being Point of (TOP-REAL 2) 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 Th44: :: SPRECT_3:44

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2)

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

for p, q being Point of (TOP-REAL 2)

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 Th45: :: SPRECT_3:45

for i being Nat

for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds

<*(g /. i)*> is_in_the_area_of f

for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds

<*(g /. i)*> is_in_the_area_of f

proof end;

theorem Th46: :: SPRECT_3:46

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds

<*p*> is_in_the_area_of f

for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds

<*p*> is_in_the_area_of f

proof end;

theorem Th47: :: SPRECT_3:47

for f being rectangular FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st not q in L~ f & <*p,q*> is_in_the_area_of f holds

(LSeg (p,q)) /\ (L~ f) c= {p}

for p, q being Point of (TOP-REAL 2) 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:48

for f being rectangular FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds

(LSeg (p,q)) /\ (L~ f) = {p}

for p, q being Point of (TOP-REAL 2) 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 Th49: :: SPRECT_3:49

for i, j being 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

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:50

for g being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds

<*((1 / 2) * (p + q))*> is_in_the_area_of g

for p, q being Point of (TOP-REAL 2) 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:52

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) 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

for p being Point of (TOP-REAL 2) 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:53

for f being non constant standard special_circular_sequence

for g being FinSequence of (TOP-REAL 2) holds

( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )

for g being FinSequence of (TOP-REAL 2) holds

( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )

proof end;

theorem :: SPRECT_3:54

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

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:55

for i, j being 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))

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:56

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) 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

for p being Point of (TOP-REAL 2) 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;