The abstract of the Mizar article:

Some Topological Properties of Cells in $R^2$

by

Yatsuka Nakamura, and

Andrzej Trybulec

Received July 22, 1996

MML identifier: GOBRD11

[ Mizar article, MML identifier index ]

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);