:: Some Topological Properties of Cells in $R^2$
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996 Association of Mizar Users

Lm1: sqrt 2 > 0
by SQUARE_1:93;

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

proof end;

theorem :: GOBRD11:2

for GX being non empty TopSpace
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

proof end;

theorem :: GOBRD11:3

for GZ being non empty TopSpace
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

proof end;

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)

proof end;

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)

proof end;

theorem Th6: :: GOBRD11:6

for f being non constant standard special_circular_sequence holds (L~ f) ` <> {}

proof end;

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:25;

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

proof end;

Lm3: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2)

proof end;

Lm4: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2)

proof end;

Lm5: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2)

proof end;

Lm6: for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2)

proof end;

Lm7: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2)

proof end;

Lm8: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2)

proof end;

Lm9: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2)

proof end;

Lm10: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2)

proof end;

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 `

proof end;

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 `

proof end;

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 `

proof end;

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 `

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th18: :: GOBRD11:18

for G being V9 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 }

proof end;

theorem Th19: :: GOBRD11:19

for G being V9 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 }

proof end;

theorem Th20: :: GOBRD11:20

for i being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th21: :: GOBRD11:21

for G being V9 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 }

proof end;

theorem Th22: :: GOBRD11:22

for G being V9 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 }

proof end;

theorem Th23: :: GOBRD11:23

for j being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th24: :: GOBRD11:24

for G being V9 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 ) }

proof end;

theorem Th25: :: GOBRD11:25

for G being V9 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 ) }

proof end;

theorem Th26: :: GOBRD11:26

for j being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th27: :: GOBRD11:27

for G being V9 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 ) }

proof end;

theorem Th28: :: GOBRD11:28

for G being V9 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 ) }

proof end;

theorem Th29: :: GOBRD11:29

for j being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th30: :: GOBRD11:30

for i being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th31: :: GOBRD11:31

for i being Element of NAT
for G being V9 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 ) }

proof end;

theorem Th32: :: GOBRD11:32

for i, j being Element of NAT
for G being V9 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 ) }

proof end;

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

proof end;

theorem Th34: :: GOBRD11:34

for G being V9 Matrix of (TOP-REAL 2) holds
( 1 <= len G & 1 <= width G )

proof end;

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

proof end;