GOBRD12: The First Part of Jordan's Theorem for Special Polygons

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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, FUNCT_1, GOBOARD5, TOPREAL1, STRUCT_0, EUCLID, RELAT_1, XXREAL_0, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, TARSKI, XBOOLE_0, PRE_TOPC, CONNSP_3, RELAT_2, GOBOARD9, CONNSP_1, ARYTM_3, CARD_1, RLTOPSP1, PARTFUN1, MATRIX_1, ZFMISC_1, MCART_1, ARYTM_1, RCOMP_1, NAT_1, CONVEX1, CHORD;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, ORDINAL1, NUMBERS, DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, NAT_1, NAT_D, PRE_TOPC, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, TOPS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD2, GOBOARD5, GOBOARD9, CONNSP_3, GOBRD10, XXREAL_0;
definitions TARSKI;
theorems TARSKI, NAT_1, FINSEQ_1, SPPOL_1, GOBOARD7, GOBOARD8, GOBOARD9, PRE_TOPC, CONNSP_1, SUBSET_1, EUCLID, CONNSP_3, TOPREAL1, GOBOARD5, TOPREAL3, MATRIX_0, GOBRD10, GOBRD11, ZFMISC_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D, ORDINAL1;
schemes MATRIX_0;
registrations SUBSET_1, RELSET_1, XXREAL_0, NAT_1, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, GOBRD11, JORDAN1, XREAL_0, ORDINAL1;
constructors HIDDEN, DOMAIN_1, REAL_1, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3, GOBRD10, GOBOARD1, NAT_D, RELSET_1, CONVEX1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities CONNSP_3, STRUCT_0;
expansions TARSKI;

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;

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;