:: Left and Right Component of the Complement of a Special Closed Curve
:: by Andrzej Trybulec
::
:: Received October 29, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

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 K6( the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st
( b1 is convex & not b1 is empty )
proof end;
end;

theorem :: GOBOARD9:5
canceled;

theorem Th6: :: GOBOARD9:6
for P, Q being convex Subset of (TOP-REAL 2) holds P /\ Q is convex
proof end;

theorem Th7: :: GOBOARD9:7
for f being FinSequence of (TOP-REAL 2) holds Rev (X_axis f) = X_axis (Rev f)
proof end;

theorem Th8: :: 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 V13() V16( NAT ) Function-like non constant V26() FinSequence-like FinSubsequence-like for set ;
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
Rev f is standard special_circular_sequence
proof end;
end;

theorem Th9: :: GOBOARD9:9
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)
proof end;

theorem Th10: :: GOBOARD9:10
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell ((Rev f),i) = right_cell (f,j)
proof end;

theorem Th11: :: GOBOARD9:11
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
proof end;

theorem Th12: :: GOBOARD9:12
for j being Element of NAT
for G being Go-board st j <= width G holds
Int (h_strip (G,j)) is convex
proof end;

theorem Th13: :: GOBOARD9:13
for i being Element of NAT
for G being Go-board st i <= len G holds
Int (v_strip (G,i)) is convex
proof end;

theorem Th14: :: GOBOARD9:14
for i, j being Element of NAT
for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) <> {}
proof end;

theorem Th15: :: GOBOARD9:15
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) <> {}
proof end;

theorem Th16: :: GOBOARD9:16
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) <> {}
proof end;

theorem Th17: :: GOBOARD9:17
for i, j being Element of 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;

theorem Th19: :: GOBOARD9:19
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) is convex
proof end;

theorem Th20: :: GOBOARD9:20
for f being non constant standard special_circular_sequence
for k being Element of 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 Th15;
A3: Int (right_cell (f,1)) <> {} by A1, Th16;
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 b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) 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 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 b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) 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 A3, Th1, XBOOLE_1:67;
end;

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

theorem Th21: :: GOBOARD9:21
for f being non constant standard special_circular_sequence
for k being Element of 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 Th23: :: 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 Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) c= RightComp f
proof end;