Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Left and Right Component of the Complement of a Special Closed Curve

**by****Andrzej Trybulec**- Received October 29, 1995
- MML identifier: GOBOARD9

- [ Mizar article, MML identifier index ]

environ vocabulary SEQM_3, GOBOARD5, PRE_TOPC, EUCLID, GOBOARD1, ARYTM_1, CONNSP_1, BOOLE, RELAT_1, SUBSET_1, RELAT_2, TOPREAL1, JORDAN1, FINSEQ_1, FINSEQ_5, FUNCT_1, MCART_1, GOBOARD2, CARD_1, MATRIX_1, ABSVALUE, FINSEQ_6, ARYTM, TREES_1, TOPS_1, ARYTM_3, GOBOARD9, FINSEQ_4, ORDINAL2; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, BINARITH, FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, JORDAN1, FINSEQ_5, FINSEQ_6, GOBOARD5; constructors SEQM_3, REAL_1, ABSVALUE, BINARITH, TOPS_1, CONNSP_1, GOBOARD2, JORDAN1, FINSEQ_5, GOBOARD5, FINSEQ_4, INT_1, MEMBERED; clusters STRUCT_0, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, FINSEQ_6, EUCLID, FINSEQ_1, TOPREAL1, INT_1, XREAL_0, MEMBERED, ARYTM_3; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve f for non constant standard special_circular_sequence, i,j,k,i1,i2,j1,j2 for Nat, r,s,r1,s1,r2,s2 for Real, a,b for natural number, p,q for Point of TOP-REAL 2, G for Go-board; theorem :: GOBOARD9:1 a -' a = 0; theorem :: GOBOARD9:2 a -' b <= a; theorem :: GOBOARD9:3 for GX being non empty TopSpace, A1,A2,B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B holds A1 = A2 or A1 misses A2; theorem :: GOBOARD9:4 for GX being non empty TopSpace, A,B being non empty Subset of GX, AA being Subset of GX|B st A = AA holds GX|A = GX|B|AA; theorem :: GOBOARD9:5 for GX being non empty TopSpace, A being non empty Subset of GX, B being non empty Subset of GX st A c= B & A is connected ex C being Subset of GX st C is_a_component_of B & A c= C; theorem :: GOBOARD9:6 for GX being non empty TopSpace, A,C,D being Subset of GX, B 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; theorem :: GOBOARD9:7 LSeg(p,q) is convex; theorem :: GOBOARD9:8 LSeg(p,q) is connected; definition cluster convex non empty Subset of TOP-REAL 2; end; theorem :: GOBOARD9:9 for P,Q being convex Subset of TOP-REAL 2 holds P /\ Q is convex; theorem :: GOBOARD9:10 for f being FinSequence of TOP-REAL 2 holds Rev X_axis f = X_axis Rev f; theorem :: GOBOARD9:11 for f being FinSequence of TOP-REAL 2 holds Rev Y_axis f = Y_axis Rev f; definition cluster non constant FinSequence; end; definition let f be non constant FinSequence; cluster Rev f -> non constant; end; definition let f be standard special_circular_sequence; redefine func Rev f -> standard special_circular_sequence; end; theorem :: GOBOARD9:12 i >= 1 & j >= 1 & i+j = len f implies left_cell(f,i) = right_cell(Rev f,j); theorem :: GOBOARD9:13 i >= 1 & j >= 1 & i+j = len f implies left_cell(Rev f,i) = right_cell(f,j); theorem :: GOBOARD9:14 1 <= k & k+1 <= len f implies ex i,j st i <= len GoB f & j <= width GoB f & cell(GoB f,i,j) = left_cell(f,k); theorem :: GOBOARD9:15 j <= width G implies Int h_strip(G,j) is convex; theorem :: GOBOARD9:16 i <= len G implies Int v_strip(G,i) is convex; theorem :: GOBOARD9:17 i <= len G & j <= width G implies Int cell(G,i,j) <> {}; theorem :: GOBOARD9:18 1 <= k & k+1 <= len f implies Int left_cell(f,k) <> {}; theorem :: GOBOARD9:19 1 <= k & k+1 <= len f implies Int right_cell(f,k) <> {}; theorem :: GOBOARD9:20 i <= len G & j <= width G implies Int cell(G,i,j) is convex; theorem :: GOBOARD9:21 i <= len G & j <= width G implies Int cell(G,i,j) is connected; theorem :: GOBOARD9:22 1 <= k & k+1 <= len f implies Int left_cell(f,k) is connected; theorem :: GOBOARD9:23 1 <= k & k+1 <= len f implies Int right_cell(f,k) is connected; definition let f; func LeftComp f -> Subset of TOP-REAL 2 means :: GOBOARD9:def 1 it is_a_component_of (L~f)` & Int left_cell(f,1) c= it; func RightComp f -> Subset of TOP-REAL 2 means :: GOBOARD9:def 2 it is_a_component_of (L~f)` & Int right_cell(f,1) c= it; end; theorem :: GOBOARD9:24 for k st 1 <= k & k+1 <= len f holds Int left_cell(f,k) c= LeftComp f; theorem :: GOBOARD9:25 GoB Rev f = GoB f; theorem :: GOBOARD9:26 RightComp f = LeftComp Rev f; theorem :: GOBOARD9:27 RightComp Rev f = LeftComp f; theorem :: GOBOARD9:28 for k st 1 <= k & k+1 <= len f holds Int right_cell(f,k) c= RightComp f;

Back to top