:: Left and Right Component of the Complement of a Special Closed Curve
:: by Andrzej Trybulec
::
:: Copyright (c) 1995-2019 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 ());
existence
ex b1 being Subset of () st
( b1 is convex & not b1 is empty )
proof end;
end;

theorem :: GOBOARD9:5
canceled;

::$CT theorem Th5: :: GOBOARD9:6 for P, Q being convex Subset of () holds P /\ Q is convex proof end; theorem Th6: :: GOBOARD9:7 for f being FinSequence of () holds Rev () = X_axis (Rev f) proof end; theorem Th7: :: GOBOARD9:8 for f being FinSequence of () holds Rev () = Y_axis (Rev f) proof end; Lm1: for f, ff being non empty FinSequence of () st ff = Rev f holds GoB ff = GoB f proof end; registration existence not for b1 being FinSequence holds b1 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 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 ;
then A2: Int (left_cell (f,1)) <> {} by Th14;
A3: Int (right_cell (f,1)) <> {} by ;
func LeftComp f -> Subset of () means :Def1: :: GOBOARD9:def 1
( it is_a_component_of (L~ f)  & Int (left_cell (f,1)) c= it );
existence
ex b1 being Subset of () st
( b1 is_a_component_of (L~ f)  & Int (left_cell (f,1)) c= b1 )
proof end;
uniqueness
for b1, b2 being Subset of () st b1 is_a_component_of (L~ f)  & Int (left_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f)  & Int (left_cell (f,1)) c= b2 holds
b1 = b2
by ;
func RightComp f -> Subset of () means :Def2: :: GOBOARD9:def 2
( it is_a_component_of (L~ f)  & Int (right_cell (f,1)) c= it );
existence
ex b1 being Subset of () st
( b1 is_a_component_of (L~ f)  & Int (right_cell (f,1)) c= b1 )
proof end;
uniqueness
for b1, b2 being Subset of () st b1 is_a_component_of (L~ f)  & Int (right_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f)  & Int (right_cell (f,1)) c= b2 holds
b1 = b2
by ;
end;

:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :
for f being non constant standard special_circular_sequence
for b2 being Subset of () holds
( b2 = LeftComp f iff ( b2 is_a_component_of (L~ f)  & Int (left_cell (f,1)) c= b2 ) );

:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :
for f being non constant standard special_circular_sequence
for b2 being Subset of () holds
( b2 = RightComp f iff ( b2 is_a_component_of (L~ f)  & Int (right_cell (f,1)) c= b2 ) );

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;