:: The First Part of Jordan's Theorem for Special Polygons
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


Lm1: for f being non constant standard special_circular_sequence holds (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `))
proof end;

Lm2: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:22;

theorem Th1: :: GOBRD12:1
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= (L~ f) ` by GOBOARD7:12, SUBSET_1:23;

theorem Th2: :: GOBRD12:2
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `)
proof end;

theorem Th3: :: GOBRD12:3
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) )
proof end;

Lm3: for f being non constant standard special_circular_sequence holds
( Cl (Down ((LeftComp f),((L~ f) `))) is connected & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((LeftComp f),((L~ f) `)) is a_component )
proof end;

Lm4: for f being non constant standard special_circular_sequence holds
( Cl (Down ((RightComp f),((L~ f) `))) is connected & Down ((RightComp f),((L~ f) `)) = RightComp f & Down ((RightComp f),((L~ f) `)) is a_component )
proof end;

theorem Th4: :: GOBRD12:4
for f being non constant standard special_circular_sequence holds (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
proof end;

theorem Th5: :: GOBRD12:5
for f being non constant standard special_circular_sequence holds
( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f )
proof end;

Lm5: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds
Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f)
proof end;

Lm6: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds
Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f)
proof end;

theorem Th6: :: GOBRD12:6
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent holds
( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )
proof end;

theorem Th7: :: GOBRD12:7
for f being non constant standard special_circular_sequence
for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Nat st
( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) & ( for i, k1, k2 being Nat st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds
( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds
for i being Nat st i in dom F1 holds
Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f)
proof end;

theorem Th8: :: GOBRD12:8
for f being non constant standard special_circular_sequence ex i, j being Nat st
( i <= len (GoB f) & j <= width (GoB f) & Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) )
proof end;

theorem Th9: :: GOBRD12:9
for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f)
proof end;

:: WP: Jordan Curve Theorem for special polygons
theorem :: GOBRD12:10
for f being non constant standard special_circular_sequence holds (L~ f) ` = (LeftComp f) \/ (RightComp f)
proof end;