:: The First Part of Jordan's Theorem for Special Polygons
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996 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) ` ))
Lm2:
the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;
theorem :: GOBRD12:1
canceled;
theorem Th2: :: GOBRD12:2
theorem Th3: :: GOBRD12:3
theorem Th4: :: GOBRD12:4
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_of (TOP-REAL 2) | ((L~ f) ` ) )
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_of (TOP-REAL 2) | ((L~ f) ` ) )
theorem Th5: :: GOBRD12:5
theorem Th6: :: GOBRD12:6
Lm5:
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Element of 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)
Lm6:
for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Element of 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)
theorem Th7: :: GOBRD12:7
for
f being non
constant standard special_circular_sequence for
i1,
j1,
i2,
j2 being
Element of
NAT st
i1 <= len (GoB f) &
j1 <= width (GoB f) &
i2 <= len (GoB f) &
j2 <= width (GoB f) &
i1,
j1,
i2,
j2 are_adjacent2 holds
(
Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )
theorem Th8: :: GOBRD12:8
theorem Th9: :: GOBRD12:9
theorem Th10: :: GOBRD12:10
theorem :: GOBRD12:11