environ vocabulary PRE_TOPC, SQUARE_1, RELAT_2, CONNSP_1, SETFAM_1, TARSKI, BOOLE, CONNSP_3, SEQM_3, GOBOARD5, MATRIX_1, EUCLID, TOPREAL1, SUBSET_1, ARYTM_3, GOBOARD2, TREES_1, ARYTM_1, FINSEQ_1, MCART_1, GOBOARD1, METRIC_1, TOPS_1, PCOMPS_1, RELAT_1, FUNCT_1, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, TOPREAL1, GOBOARD1, ORDINAL1, XREAL_0, REAL_1, NAT_1, SQUARE_1, BINARITH, STRUCT_0, PRE_TOPC, FINSEQ_1, MATRIX_1, METRIC_1, TOPS_1, CONNSP_1, PCOMPS_1, EUCLID, GOBOARD2, GOBOARD5, CONNSP_3; constructors REAL_1, SQUARE_1, BINARITH, TOPS_1, CONNSP_1, PCOMPS_1, GOBOARD2, GOBOARD9, CONNSP_3, MEMBERED; clusters STRUCT_0, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, EUCLID, TOPREAL1, XREAL_0, ARYTM_3, GOBOARD1, MEMBERED, ZFMISC_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve i,j,k for Nat, r,s,r1,r2,s1,s2,sb,tb for Real, x for set, GX for non empty TopSpace; theorem :: GOBRD11:1 for A being Subset of GX, p being Point of GX st p in A & A is connected holds A c= skl p; theorem :: GOBRD11:2 for A,B,C being Subset of GX st C is_a_component_of GX & A c= C & B is connected & Cl A meets Cl B holds B c= C; reserve GZ for non empty TopSpace; theorem :: GOBRD11:3 for A,B being Subset of GZ st A is_a_component_of GZ & B is_a_component_of GZ holds A \/ B is a_union_of_components of GZ; theorem :: GOBRD11:4 for B1,B2,V being Subset of GX holds Down(B1 \/ B2,V)=Down(B1,V) \/ Down(B2,V); theorem :: GOBRD11:5 for B1,B2,V being Subset of GX holds Down(B1 /\ B2,V)=Down(B1,V) /\ Down(B2,V); reserve f for non constant standard special_circular_sequence, G for non empty-yielding Matrix of TOP-REAL 2; theorem :: GOBRD11:6 (L~f)` <> {}; definition let f; cluster (L~f)` -> non empty; end; theorem :: GOBRD11:7 for f holds the carrier of TOP-REAL 2 = union {cell(GoB f,i,j):i<=len GoB f & j<=width GoB f}; theorem :: GOBRD11:8 for P1,P2 being Subset of TOP-REAL 2 st P1={ |[r,s]| : s <= s1 } & P2={ |[r2,s2]| : s2 > s1 } holds P1=P2`; theorem :: GOBRD11:9 for P1,P2 being Subset of TOP-REAL 2 st P1={ |[r,s]| : s >= s1 } & P2={ |[r2,s2]| : s2 < s1 } holds P1=P2`; theorem :: GOBRD11:10 for P1,P2 being Subset of TOP-REAL 2 st P1={ |[s,r]| : s >= s1 } & P2={ |[s2,r2]| : s2 < s1 } holds P1=P2`; theorem :: GOBRD11:11 for P1,P2 being Subset of TOP-REAL 2 st P1={ |[s,r]| : s <= s1 } & P2={ |[s2,r2]| : s2 > s1 } holds P1=P2`; theorem :: GOBRD11:12 for P being Subset of TOP-REAL 2, s1 st P= { |[r,s]| : s <= s1 } holds P is closed; theorem :: GOBRD11:13 for P being Subset of TOP-REAL 2,s1 st P={ |[r,s]| : s1 <= s } holds P is closed; theorem :: GOBRD11:14 for P being Subset of TOP-REAL 2, s1 st P= { |[s,r]| : s <= s1 } holds P is closed; theorem :: GOBRD11:15 for P being Subset of TOP-REAL 2,s1 st P={ |[s,r]| : s1 <= s } holds P is closed; theorem :: GOBRD11:16 for G being Matrix of TOP-REAL 2 holds h_strip(G,j) is closed; theorem :: GOBRD11:17 for G being Matrix of TOP-REAL 2 holds v_strip(G,j) is closed; theorem :: GOBRD11:18 G is X_equal-in-line implies v_strip(G,0) = { |[r,s]| : r <= G*(1,1)`1 }; theorem :: GOBRD11:19 G is X_equal-in-line implies v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r }; theorem :: GOBRD11:20 G is X_equal-in-line & 1 <= i & i < len G implies v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }; theorem :: GOBRD11:21 G is Y_equal-in-column implies h_strip(G,0) = { |[r,s]| : s <= G*(1,1)`2 }; theorem :: GOBRD11:22 G is Y_equal-in-column implies h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s }; theorem :: GOBRD11:23 G is Y_equal-in-column & 1 <= j & j < width G implies h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }; reserve G for non empty-yielding X_equal-in-line Y_equal-in-column Matrix of TOP-REAL 2; theorem :: GOBRD11:24 cell(G,0,0) = { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 }; theorem :: GOBRD11:25 cell(G,0,width G) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s }; theorem :: GOBRD11:26 1 <= j & j < width G implies cell(G,0,j) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }; theorem :: GOBRD11:27 cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2 }; theorem :: GOBRD11:28 cell(G,len G,width G) = { |[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s }; theorem :: GOBRD11:29 1 <= j & j < width G implies cell(G,len G,j) = { |[r,s]| : G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }; theorem :: GOBRD11:30 1 <= i & i < len G implies cell(G,i,0) = { |[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G* (1,1)`2 }; theorem :: GOBRD11:31 1 <= i & i < len G implies cell(G,i,width G) = { |[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s }; theorem :: GOBRD11:32 1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }; theorem :: GOBRD11:33 for G being Matrix of TOP-REAL 2 holds cell(G,i,j) is closed; theorem :: GOBRD11:34 for G being non empty-yielding Matrix of TOP-REAL 2 holds 1<=len G & 1<=width G; theorem :: GOBRD11:35 for G being Go-board holds i<=len G & j<=width G implies cell(G,i,j)=Cl Int cell(G,i,j);