:: Some Topological Properties of Cells in $R^2$ :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received July 22, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin Lm1: sqrt 2 > 0 by SQUARE_1:25; theorem Th1: :: GOBRD11:1 for GX being non empty TopSpace for A being Subset of GX for p being Point of GX st p in A & A is connected holds A c= Component_of p proofend; theorem :: GOBRD11:2 for GX being non empty TopSpace for A, B, C being Subset of GX st C is a_component & A c= C & B is connected & Cl A meets Cl B holds B c= C proofend; theorem :: GOBRD11:3 for GZ being non empty TopSpace for A, B being Subset of GZ st A is a_component & B is a_component holds A \/ B is a_union_of_components of GZ proofend; theorem :: GOBRD11:4 for GX being non empty TopSpace for B1, B2, V being Subset of GX holds Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) proofend; theorem :: GOBRD11:5 for GX being non empty TopSpace for B1, B2, V being Subset of GX holds Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) proofend; theorem Th6: :: GOBRD11:6 for f being non constant standard special_circular_sequence holds (L~ f) ` <> {} proofend; registration let f be non constant standard special_circular_sequence; cluster(L~ f) ` -> non empty ; coherence not (L~ f) ` is empty by Th6; end; Lm2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; theorem :: GOBRD11:7 for f being non constant standard special_circular_sequence holds the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } proofend; Lm3: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2) proofend; Lm4: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2) proofend; Lm5: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2) proofend; Lm6: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2) proofend; Lm7: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2) proofend; Lm8: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2) proofend; Lm9: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2) proofend; Lm10: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2) proofend; theorem Th8: :: GOBRD11:8 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s <= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 > s1 } holds P1 = P2 ` proofend; theorem Th9: :: GOBRD11:9 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } holds P1 = P2 ` proofend; theorem Th10: :: GOBRD11:10 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s >= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 < s1 } holds P1 = P2 ` proofend; theorem Th11: :: GOBRD11:11 for s1 being Real for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } holds P1 = P2 ` proofend; theorem Th12: :: GOBRD11:12 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[r,s]| where r, s is Real : s <= s1 } holds P is closed proofend; theorem Th13: :: GOBRD11:13 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[r,s]| where r, s is Real : s1 <= s } holds P is closed proofend; theorem Th14: :: GOBRD11:14 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[s,r]| where s, r is Real : s <= s1 } holds P is closed proofend; theorem Th15: :: GOBRD11:15 for P being Subset of (TOP-REAL 2) for s1 being Real st P = { |[s,r]| where s, r is Real : s1 <= s } holds P is closed proofend; theorem Th16: :: GOBRD11:16 for j being Element of NAT for G being Matrix of (TOP-REAL 2) holds h_strip (G,j) is closed proofend; theorem Th17: :: GOBRD11:17 for j being Element of NAT for G being Matrix of (TOP-REAL 2) holds v_strip (G,j) is closed proofend; theorem Th18: :: GOBRD11:18 for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line holds v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } proofend; theorem Th19: :: GOBRD11:19 for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line holds v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } proofend; theorem Th20: :: GOBRD11:20 for i being Element of NAT for G being V21() Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G holds v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } proofend; theorem Th21: :: GOBRD11:21 for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column holds h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } proofend; theorem Th22: :: GOBRD11:22 for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column holds h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } proofend; theorem Th23: :: GOBRD11:23 for j being Element of NAT for G being V21() Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G holds h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proofend; theorem Th24: :: GOBRD11:24 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,0,0) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } proofend; theorem Th25: :: GOBRD11:25 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,0,(width G)) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s ) } proofend; theorem Th26: :: GOBRD11:26 for j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proofend; theorem Th27: :: GOBRD11:27 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,(len G),0) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } proofend; theorem Th28: :: GOBRD11:28 for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell (G,(len G),(width G)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,(width G))) `2 <= s ) } proofend; theorem Th29: :: GOBRD11:29 for j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= j & j < width G holds cell (G,(len G),j) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proofend; theorem Th30: :: GOBRD11:30 for i being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } proofend; theorem Th31: :: GOBRD11:31 for i being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G holds cell (G,i,(width G)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 <= s ) } proofend; theorem Th32: :: GOBRD11:32 for i, j being Element of NAT for G being V21() X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j < width G holds cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } proofend; theorem Th33: :: GOBRD11:33 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) holds cell (G,i,j) is closed proofend; theorem Th34: :: GOBRD11:34 for G being V21() Matrix of (TOP-REAL 2) holds ( 1 <= len G & 1 <= width G ) proofend; theorem :: GOBRD11:35 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds cell (G,i,j) = Cl (Int (cell (G,i,j))) proofend;