:: by Andrzej Trybulec

::

:: Received October 29, 1995

:: Copyright (c) 1995-2018 Association of Mizar Users

theorem Th1: :: GOBOARD9:1

for GX being TopSpace

for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds

A1 misses A2

for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds

A1 misses A2

proof end;

theorem Th2: :: GOBOARD9:2

for GX being TopSpace

for A, B being Subset of GX

for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

for A, B being Subset of GX

for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

proof end;

theorem Th3: :: GOBOARD9:3

for GX being non empty TopSpace

for A, B being non empty Subset of GX st A c= B & A is connected holds

ex C being Subset of GX st

( C is_a_component_of B & A c= C )

for A, B being non empty Subset of GX st A c= B & A is connected holds

ex C being Subset of GX st

( C is_a_component_of B & A c= C )

proof end;

theorem Th4: :: GOBOARD9:4

for GX being non empty TopSpace

for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds

B c= C

for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds

B c= C

proof end;

registration

existence

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is convex & not b_{1} is empty )

end;
ex b

( b

proof end;

::$CT

Lm1: for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds

GoB ff = GoB f

proof end;

registration

not for b_{1} being FinSequence holds b_{1} is constant
end;

cluster V1() V4( NAT ) Function-like non constant V28() FinSequence-like FinSubsequence-like for FinSequence;

existence not for b

proof end;

definition

let f be standard special_circular_sequence;

:: original: Rev

redefine func Rev f -> standard special_circular_sequence;

coherence

Rev f is standard special_circular_sequence

end;
:: original: Rev

redefine func Rev f -> standard special_circular_sequence;

coherence

Rev f is standard special_circular_sequence

proof end;

theorem Th8: :: GOBOARD9:9

for f being non constant standard special_circular_sequence

for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds

left_cell (f,i) = right_cell ((Rev f),j)

for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds

left_cell (f,i) = right_cell ((Rev f),j)

proof end;

theorem Th9: :: GOBOARD9:10

for f being non constant standard special_circular_sequence

for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds

left_cell ((Rev f),i) = right_cell (f,j)

for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds

left_cell ((Rev f),i) = right_cell (f,j)

proof end;

theorem Th10: :: GOBOARD9:11

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

for k being Nat st 1 <= k & k + 1 <= len f holds

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

proof end;

theorem Th14: :: GOBOARD9:15

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) <> {}

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) <> {}

proof end;

theorem Th15: :: GOBOARD9:16

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) <> {}

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) <> {}

proof end;

theorem Th16: :: GOBOARD9:17

for i, j being Nat

for G being Go-board st i <= len G & j <= width G holds

Int (cell (G,i,j)) is convex

for G being Go-board st i <= len G & j <= width G holds

Int (cell (G,i,j)) is convex

proof end;

::$CT

theorem Th17: :: GOBOARD9:19

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) is convex

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) is convex

proof end;

theorem Th18: :: GOBOARD9:20

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) is convex

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) is convex

proof end;

definition

let f be non constant standard special_circular_sequence;

A1: 1 + 1 < len f by GOBOARD7:34, XXREAL_0:2;

then A2: Int (left_cell (f,1)) <> {} by Th14;

A3: Int (right_cell (f,1)) <> {} by A1, Th15;

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b_{1} )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st b_{1} is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b_{1} & b_{2} is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b_{2} holds

b_{1} = b_{2}
by A2, Th1, XBOOLE_1:67;

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b_{1} )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st b_{1} is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b_{1} & b_{2} is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b_{2} holds

b_{1} = b_{2}
by A3, Th1, XBOOLE_1:67;

end;
A1: 1 + 1 < len f by GOBOARD7:34, XXREAL_0:2;

then A2: Int (left_cell (f,1)) <> {} by Th14;

A3: Int (right_cell (f,1)) <> {} by A1, Th15;

func LeftComp f -> Subset of (TOP-REAL 2) means :Def1: :: GOBOARD9:def 1

( it is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= it );

existence ( it is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= it );

ex b

( b

proof end;

uniqueness for b

b

func RightComp f -> Subset of (TOP-REAL 2) means :Def2: :: GOBOARD9:def 2

( it is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= it );

existence ( it is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= it );

ex b

( b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :

for f being non constant standard special_circular_sequence

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = LeftComp f iff ( b_{2} is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b_{2} ) );

for f being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :

for f being non constant standard special_circular_sequence

for b_{2} being Subset of (TOP-REAL 2) holds

( b_{2} = RightComp f iff ( b_{2} is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b_{2} ) );

for f being non constant standard special_circular_sequence

for b

( b

theorem Th19: :: GOBOARD9:21

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) c= LeftComp f

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) c= LeftComp f

proof end;

theorem :: GOBOARD9:22

theorem :: GOBOARD9:25

for f being non constant standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) c= RightComp f

for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) c= RightComp f

proof end;