:: Left and Right Component of the Complement of a Special Closed Curve
:: by Andrzej Trybulec
::
:: Received October 29, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem :: GOBOARD9:1
canceled;
theorem :: GOBOARD9:2
canceled;
theorem Th3: :: GOBOARD9:3
theorem Th4: :: GOBOARD9:4
theorem Th5: :: GOBOARD9:5
theorem Th6: :: GOBOARD9:6
theorem Th7: :: GOBOARD9:7
theorem Th8: :: GOBOARD9:8
theorem Th9: :: GOBOARD9:9
theorem Th10: :: GOBOARD9:10
theorem Th11: :: GOBOARD9:11
Lm1:
for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds
GoB ff = GoB f
theorem Th12: :: GOBOARD9:12
theorem Th13: :: GOBOARD9:13
theorem Th14: :: GOBOARD9:14
theorem Th15: :: GOBOARD9:15
theorem Th16: :: GOBOARD9:16
theorem Th17: :: GOBOARD9:17
theorem Th18: :: GOBOARD9:18
theorem Th19: :: GOBOARD9:19
theorem Th20: :: GOBOARD9:20
theorem Th21: :: GOBOARD9:21
theorem Th22: :: GOBOARD9:22
theorem Th23: :: GOBOARD9:23
definition
let f be non
constant standard special_circular_sequence;
A1:
1
+ 1
< len f
by GOBOARD7:36, XXREAL_0:2;
then A2:
Int (left_cell f,1) <> {}
by Th18;
A3:
Int (right_cell f,1) <> {}
by A1, Th19;
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 )
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, Th3, 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 )
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, Th3, XBOOLE_1:67;
end;
:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :
:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :
theorem Th24: :: GOBOARD9:24
theorem :: GOBOARD9:25
theorem Th26: :: GOBOARD9:26
theorem :: GOBOARD9:27
theorem :: GOBOARD9:28