:: Some Properties of Cells and Arcs
:: by Robert Milewski , Andrzej Trybulec , Artur Korni{\l}owicz
::
:: Received October 6, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users


begin

theorem :: JORDAN1B:1
canceled;

theorem :: JORDAN1B:2
for f being FinSequence holds
( f is empty iff Rev f is empty )
proof end;

theorem :: JORDAN1B:3
for D being non empty set
for f being FinSequence of D
for i, j being Element of NAT st 1 <= i & i <= len f & 1 <= j & j <= len f holds
not mid (f,i,j) is empty
proof end;

theorem Th4: :: JORDAN1B:4
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st 1 <= len f & p in L~ f holds
(R_Cut (f,p)) . 1 = f . 1
proof end;

theorem :: JORDAN1B:5
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds
(L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len f)
proof end;

theorem :: JORDAN1B:6
for P being Simple_closed_curve holds W-max P <> E-max P
proof end;

theorem :: JORDAN1B:7
for i being Element of NAT
for D being non empty set
for f being FinSequence of D st 1 <= i & i < len f holds
(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))
proof end;

theorem :: JORDAN1B:8
for p, q being Point of (TOP-REAL 2) st p <> q & LSeg (p,q) is vertical holds
<*p,q*> is being_S-Seq
proof end;

theorem :: JORDAN1B:9
for p, q being Point of (TOP-REAL 2) st p <> q & LSeg (p,q) is horizontal holds
<*p,q*> is being_S-Seq
proof end;

theorem Th10: :: JORDAN1B:10
for p, q being FinSequence of (TOP-REAL 2)
for v being Point of (TOP-REAL 2) st p is_in_the_area_of q holds
Rotate (p,v) is_in_the_area_of q
proof end;

theorem :: JORDAN1B:11
for p being non trivial FinSequence of (TOP-REAL 2)
for v being Point of (TOP-REAL 2) holds Rotate (p,v) is_in_the_area_of p by Th10, SPRECT_2:25;

theorem Th12: :: JORDAN1B:12
for f being FinSequence holds Center f >= 1
proof end;

theorem :: JORDAN1B:13
for f being FinSequence st len f >= 1 holds
Center f <= len f
proof end;

theorem Th14: :: JORDAN1B:14
for G being Go-board holds Center G <= len G
proof end;

theorem Th15: :: JORDAN1B:15
for f being FinSequence st len f >= 2 holds
Center f > 1
proof end;

theorem Th16: :: JORDAN1B:16
for f being FinSequence st len f >= 3 holds
Center f < len f
proof end;

Lm1: now
let E be non empty Subset of (TOP-REAL 2); :: thesis: (len (Gauge (E,0))) -' 1 = 3
thus (len (Gauge (E,0))) -' 1 = ((2 |^ 0) + 3) -' 1 by JORDAN8:def 1
.= (1 + 3) -' 1 by NEWTON:9
.= 3 by NAT_D:34 ; :: thesis: verum
end;

theorem :: JORDAN1B:17
for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
proof end;

theorem Th18: :: JORDAN1B:18
for E being compact non horizontal non vertical Subset of (TOP-REAL 2) holds E c= cell ((Gauge (E,0)),2,2)
proof end;

theorem Th19: :: JORDAN1B:19
for E being compact non horizontal non vertical Subset of (TOP-REAL 2) holds not cell ((Gauge (E,0)),2,2) c= BDD E
proof end;

theorem :: JORDAN1B:20
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|
proof end;

theorem :: JORDAN1B:21
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) = |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|
proof end;

Lm2: for i, m being Element of NAT st i <= m & m <= i + 1 & not i = m holds
i = m -' 1
proof end;

theorem Th22: :: JORDAN1B:22
for G being Go-board
for j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,(len G),j) & p `1 = (G * (m,n)) `1 holds
len G = m
proof end;

theorem :: JORDAN1B:23
for G being Go-board
for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= i & i <= len G & 1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,j) & p `1 = (G * (m,n)) `1 & not i = m holds
i = m -' 1
proof end;

theorem Th24: :: JORDAN1B:24
for G being Go-board
for i, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,(width G)) & p `2 = (G * (m,n)) `2 holds
width G = n
proof end;

theorem :: JORDAN1B:25
for G being Go-board
for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell (G,i,j) & p `2 = (G * (m,n)) `2 & not j = n holds
j = n -' 1
proof end;

theorem :: JORDAN1B:26
canceled;

theorem :: JORDAN1B:27
canceled;

theorem Th28: :: JORDAN1B:28
for n being Element of NAT
for C being Simple_closed_curve
for i being Element of NAT st 1 < i & i < len (Gauge (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc C
proof end;

theorem Th29: :: JORDAN1B:29
for n being Element of NAT
for C being Simple_closed_curve
for i being Element of NAT st 1 < i & i < len (Gauge (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C
proof end;

theorem :: JORDAN1B:30
for n being Element of NAT
for C being Simple_closed_curve holds LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc C
proof end;

theorem :: JORDAN1B:31
for n being Element of NAT
for C being Simple_closed_curve holds LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Lower_Arc C
proof end;

theorem Th32: :: JORDAN1B:32
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i <= len (Gauge (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n)))
proof end;

theorem Th33: :: JORDAN1B:33
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i <= len (Gauge (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1B:34
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1B:35
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Lower_Arc (L~ (Cage (C,n)))
proof end;

theorem Th36: :: JORDAN1B:36
for G being Go-board
for j being Element of NAT st j <= width G holds
not cell (G,0,j) is Bounded
proof end;

theorem Th37: :: JORDAN1B:37
for G being Go-board
for i being Element of NAT st i <= width G holds
not cell (G,(len G),i) is Bounded
proof end;

theorem Th38: :: JORDAN1B:38
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Element of NAT st j <= width (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) c= UBD C
proof end;

theorem Th39: :: JORDAN1B:39
for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Element of NAT st j <= len (Gauge (E,n)) holds
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
proof end;

Lm3: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> 0
proof end;

Lm4: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> 0
proof end;

Lm5: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> len (Gauge (C,n))
proof end;

Lm6: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> width (Gauge (C,n))
proof end;

theorem Th40: :: JORDAN1B:40
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j > 1
proof end;

theorem Th41: :: JORDAN1B:41
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i > 1
proof end;

theorem Th42: :: JORDAN1B:42
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j + 1 < width (Gauge (C,n))
proof end;

theorem Th43: :: JORDAN1B:43
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i + 1 < len (Gauge (C,n))
proof end;

theorem :: JORDAN1B:44
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st ex i, j being Element of NAT st
( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C ) holds
n >= 1
proof end;