:: JORDAN1B semantic presentation

registration

cluster -> non horizontal non vertical Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

registration

let T be non empty TopSpace;
cluster non empty a_union_of_components of T;
existence

proof end;

end;

theorem :: JORDAN1B:1

for T being non empty TopSpace
for A being non empty a_union_of_components of T st A is connected holds
A is_a_component_of T

proof end;

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

proof end;

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:
thus (len (Gauge E,0)) -' 1 = ((2 |^ 0) + 3) -' 1 by JORDAN8:def 1
.= (1 + 3) -' 1 by NEWTON:9
.= 3 by BINARITH:39 ; :: thesis:

end;

theorem :: JORDAN1B:17

for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being 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 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 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 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 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 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 Th26: :: JORDAN1B:26

for C being Simple_closed_curve
for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg |[r,(S-bound C)]|,|[r,(N-bound C)]| meets Upper_Arc C

proof end;

theorem Th27: :: JORDAN1B:27

for C being Simple_closed_curve
for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg |[r,(S-bound C)]|,|[r,(N-bound C)]| meets Lower_Arc C

proof end;

theorem Th28: :: JORDAN1B:28

for n being Nat
for C being Simple_closed_curve
for i being 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 Nat
for C being Simple_closed_curve
for i being 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 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 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 Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being 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

proof end;

theorem :: JORDAN1B:34

for n being 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

proof end;

theorem Th36: :: JORDAN1B:36

for G being Go-board
for j being 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 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 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 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 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 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 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 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 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 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 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

proof end;

theorem :: JORDAN1B:44

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st ex i, j being 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;