:: by Robert Milewski , Andrzej Trybulec , Artur Korni{\l}owicz

::

:: Received October 6, 2000

:: Copyright (c) 2000-2019 Association of Mizar Users

theorem :: JORDAN1B:2

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

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 Th3: :: JORDAN1B:3

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

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:4

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)

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

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

for p, q being Point of (TOP-REAL 2) st p <> q & LSeg (p,q) is vertical holds

<*p,q*> is being_S-Seq

<*p,q*> is being_S-Seq

proof end;

theorem :: JORDAN1B:8

for p, q being Point of (TOP-REAL 2) st p <> q & LSeg (p,q) is horizontal holds

<*p,q*> is being_S-Seq

<*p,q*> is being_S-Seq

proof end;

theorem Th9: :: JORDAN1B:9

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

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:10

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 Th9, SPRECT_2:21;

for v being Point of (TOP-REAL 2) holds Rotate (p,v) is_in_the_area_of p by Th9, SPRECT_2:21;

Lm1: now :: thesis: for E being non empty Subset of (TOP-REAL 2) holds (len (Gauge (E,0))) -' 1 = 3

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:4

.= 3 by NAT_D:34 ; :: thesis: verum

end;
thus (len (Gauge (E,0))) -' 1 = ((2 |^ 0) + 3) -' 1 by JORDAN8:def 1

.= (1 + 3) -' 1 by NEWTON:4

.= 3 by NAT_D:34 ; :: thesis: verum

theorem :: JORDAN1B:16

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

for n being Nat holds Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

proof end;

theorem Th17: :: JORDAN1B:17

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 Th18: :: JORDAN1B:18

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:19

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:20

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 Th21: :: JORDAN1B:21

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

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:22

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

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 Th23: :: JORDAN1B:23

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

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:24

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

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 Th25: :: JORDAN1B:25

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

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 Th26: :: JORDAN1B:26

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

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:27

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

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:28

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

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 Th29: :: JORDAN1B:29

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

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 Th30: :: JORDAN1B:30

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 Lower_Arc (L~ (Cage (C,n)))

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 Lower_Arc (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN1B:31

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

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:32

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 Lower_Arc (L~ (Cage (C,n)))

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 Th35: :: JORDAN1B:35

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

for j, n being Nat st j <= width (Gauge (C,n)) holds

cell ((Gauge (C,n)),0,j) c= UBD C

proof end;

theorem Th36: :: JORDAN1B:36

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

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 i, j, n 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, j, n 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 i, j, n 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, j, n 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 Th37: :: JORDAN1B:37

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j, n 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

for i, j, n 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 Th38: :: JORDAN1B:38

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j, n 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

for i, j, n 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 Th39: :: JORDAN1B:39

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j, n 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))

for i, j, n 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 Th40: :: JORDAN1B:40

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i, j, n 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 < len (Gauge (C,n))

for i, j, n 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 < len (Gauge (C,n))

proof end;

theorem :: JORDAN1B:41

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

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;