:: Left and Right Component of the Complement of a Special Closed Curve
:: by Andrzej Trybulec
::
:: Received October 29, 1995
:: Copyright (c) 1995-2021 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

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

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 )

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

proof end;

registration

cluster non empty convex for Element of K16( the carrier of (TOP-REAL 2));

existence
ex b₁ being Subset of (TOP-REAL 2) st
( b₁ is convex & not b₁ is empty )

proof end;

end;

theorem :: GOBOARD9:5

canceled;

::$CT

theorem Th5: :: GOBOARD9:6

for P, Q being convex Subset of (TOP-REAL 2) holds P /\ Q is convex

proof end;

theorem Th6: :: GOBOARD9:7

for f being FinSequence of (TOP-REAL 2) holds Rev (X_axis f) = X_axis (Rev f)

proof end;

theorem Th7: :: GOBOARD9:8

for f being FinSequence of (TOP-REAL 2) holds Rev (Y_axis f) = Y_axis (Rev f)

proof end;

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

proof end;

registration

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

existence
not for b₁ being FinSequence holds b₁ is constant

proof end;

end;

registration

let f be non constant FinSequence;

cluster Rev f -> non constant ;

coherence
not Rev f is constant

proof end;

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

proof end;

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)

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)

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

proof end;

theorem Th11: :: GOBOARD9:12

for j being Nat
for G being Go-board st j <= width G holds
Int (h_strip (G,j)) is convex

proof end;

theorem Th12: :: GOBOARD9:13

for i being Nat
for G being Go-board st i <= len G holds
Int (v_strip (G,i)) is convex

proof end;

theorem Th13: :: GOBOARD9:14

for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) <> {}

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

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

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

proof end;

theorem :: GOBOARD9:18

canceled;

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

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

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;

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
ex b₁ being Subset of (TOP-REAL 2) st
( b₁ is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b₁ )

proof end;

uniqueness
for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b<sub>1</sub> & b<sub>2</sub> is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b₂ holds
b₁ = b₂ by A2, Th1, XBOOLE_1:67;

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
ex b₁ being Subset of (TOP-REAL 2) st
( b₁ is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b₁ )

proof end;

uniqueness
for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b<sub>1</sub> & b<sub>2</sub> is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b₂ holds
b₁ = b₂ by A3, Th1, XBOOLE_1:67;

end;

:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :
for f being non constant standard special_circular_sequence
for b₂ being Subset of (TOP-REAL 2) holds
( b₂ = LeftComp f iff ( b₂ is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b₂ ) );

:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :
for f being non constant standard special_circular_sequence
for b₂ being Subset of (TOP-REAL 2) holds
( b₂ = RightComp f iff ( b₂ is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= 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

proof end;

theorem :: GOBOARD9:22

for f being non constant standard special_circular_sequence holds GoB (Rev f) = GoB f by Lm1;

theorem Th21: :: GOBOARD9:23

for f being non constant standard special_circular_sequence holds RightComp f = LeftComp (Rev f)

proof end;

theorem :: GOBOARD9:24

for f being non constant standard special_circular_sequence holds RightComp (Rev f) = LeftComp f

proof end;

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

proof end;