:: by Robert Milewski

::

:: Received June 27, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

theorem Th1: :: JORDAN14:1

for f being non constant standard special_circular_sequence holds

( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f )

( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f )

proof end;

theorem :: JORDAN14:2

for f being non constant standard special_circular_sequence holds

( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )

( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )

proof end;

theorem :: JORDAN14:3

for G being Go-board

for f being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

left_cell (f,k,G) is closed

for f being FinSequence of (TOP-REAL 2)

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

left_cell (f,k,G) is closed

proof end;

theorem Th4: :: JORDAN14:4

for G being Go-board

for p being Point of (TOP-REAL 2)

for i, j being Nat st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds

( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )

for p being Point of (TOP-REAL 2)

for i, j being Nat st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds

( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )

proof end;

registration
end;

definition

let C be Simple_closed_curve;

let n be Nat;

(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is Point of (TOP-REAL 2) ;

end;
let n be Nat;

func SpanStart (C,n) -> Point of (TOP-REAL 2) equals :: JORDAN14:def 1

(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));

coherence (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));

(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is Point of (TOP-REAL 2) ;

:: deftheorem defines SpanStart JORDAN14:def 1 :

for C being Simple_closed_curve

for n being Nat holds SpanStart (C,n) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));

for C being Simple_closed_curve

for n being Nat holds SpanStart (C,n) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));

theorem Th6: :: JORDAN14:6

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

SpanStart (C,n) in BDD C

for n being Nat st n is_sufficiently_large_for C holds

SpanStart (C,n) in BDD C

proof end;

theorem Th7: :: JORDAN14:7

for C being Simple_closed_curve

for n, k being Nat st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds

( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )

for n, k being Nat st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds

( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )

proof end;

theorem Th8: :: JORDAN14:8

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

C misses L~ (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

C misses L~ (Span (C,n))

proof end;

registration

let C be Simple_closed_curve;

let n be Nat;

coherence

Cl (RightComp (Span (C,n))) is compact by GOBRD14:32;

end;
let n be Nat;

coherence

Cl (RightComp (Span (C,n))) is compact by GOBRD14:32;

theorem Th9: :: JORDAN14:9

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

C meets LeftComp (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

C meets LeftComp (Span (C,n))

proof end;

theorem Th10: :: JORDAN14:10

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

C misses RightComp (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

C misses RightComp (Span (C,n))

proof end;

theorem Th11: :: JORDAN14:11

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

C c= LeftComp (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

C c= LeftComp (Span (C,n))

proof end;

theorem Th12: :: JORDAN14:12

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

C c= UBD (L~ (Span (C,n)))

for n being Nat st n is_sufficiently_large_for C holds

C c= UBD (L~ (Span (C,n)))

proof end;

theorem Th13: :: JORDAN14:13

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

BDD (L~ (Span (C,n))) c= BDD C

for n being Nat st n is_sufficiently_large_for C holds

BDD (L~ (Span (C,n))) c= BDD C

proof end;

theorem Th14: :: JORDAN14:14

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

UBD C c= UBD (L~ (Span (C,n)))

for n being Nat st n is_sufficiently_large_for C holds

UBD C c= UBD (L~ (Span (C,n)))

proof end;

theorem :: JORDAN14:15

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

RightComp (Span (C,n)) c= BDD C

for n being Nat st n is_sufficiently_large_for C holds

RightComp (Span (C,n)) c= BDD C

proof end;

theorem Th16: :: JORDAN14:16

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

UBD C c= LeftComp (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

UBD C c= LeftComp (Span (C,n))

proof end;

theorem Th17: :: JORDAN14:17

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses BDD (L~ (Span (C,n)))

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses BDD (L~ (Span (C,n)))

proof end;

theorem :: JORDAN14:18

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses RightComp (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses RightComp (Span (C,n))

proof end;

theorem Th19: :: JORDAN14:19

for C being Simple_closed_curve

for P being Subset of (TOP-REAL 2)

for n being Nat st n is_sufficiently_large_for C & P is_outside_component_of C holds

P misses L~ (Span (C,n))

for P being Subset of (TOP-REAL 2)

for n being Nat st n is_sufficiently_large_for C & P is_outside_component_of C holds

P misses L~ (Span (C,n))

proof end;

theorem Th20: :: JORDAN14:20

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses L~ (Span (C,n))

for n being Nat st n is_sufficiently_large_for C holds

UBD C misses L~ (Span (C,n))

proof end;

theorem Th21: :: JORDAN14:21

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

L~ (Span (C,n)) c= BDD C

for n being Nat st n is_sufficiently_large_for C holds

L~ (Span (C,n)) c= BDD C

proof end;

theorem Th22: :: JORDAN14:22

for C being Simple_closed_curve

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

i > 1

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

i > 1

proof end;

theorem Th23: :: JORDAN14:23

for C being Simple_closed_curve

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

i < len (Gauge (C,n))

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

i < len (Gauge (C,n))

proof end;

theorem Th24: :: JORDAN14:24

for C being Simple_closed_curve

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

j > 1

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

j > 1

proof end;

theorem Th25: :: JORDAN14:25

for C being Simple_closed_curve

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

j < width (Gauge (C,n))

for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds

j < width (Gauge (C,n))

proof end;

theorem :: JORDAN14:26

for C being Simple_closed_curve

for n being Nat st n is_sufficiently_large_for C holds

Y-SpanStart (C,n) < width (Gauge (C,n))

for n being Nat st n is_sufficiently_large_for C holds

Y-SpanStart (C,n) < width (Gauge (C,n))

proof end;

theorem Th27: :: JORDAN14:27

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

for n, m being Nat st m >= n & n >= 1 holds

X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2

for n, m being Nat st m >= n & n >= 1 holds

X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2

proof end;

theorem Th28: :: JORDAN14:28

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

for n, m being Nat st n <= m & n is_sufficiently_large_for C holds

m is_sufficiently_large_for C

for n, m being Nat st n <= m & n is_sufficiently_large_for C holds

m is_sufficiently_large_for C

proof end;

theorem Th29: :: JORDAN14:29

for G being Go-board

for f being FinSequence of (TOP-REAL 2)

for i, j being Nat st f is_sequence_on G & f is special & i <= len G & j <= width G holds

(cell (G,i,j)) \ (L~ f) is connected

for f being FinSequence of (TOP-REAL 2)

for i, j being Nat st f is_sequence_on G & f is special & i <= len G & j <= width G holds

(cell (G,i,j)) \ (L~ f) is connected

proof end;

theorem Th30: :: JORDAN14:30

for C being Simple_closed_curve

for n, k being Nat st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds

(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))

for n, k being Nat st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds

(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))

proof end;

theorem Th31: :: JORDAN14:31

for C being Subset of (TOP-REAL 2)

for n, m, i being Nat st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds

(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))

for n, m, i being Nat st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds

(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))

proof end;

theorem Th32: :: JORDAN14:32

for C being Simple_closed_curve

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

RightComp (Span (C,n)) meets RightComp (Span (C,m))

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

RightComp (Span (C,n)) meets RightComp (Span (C,m))

proof end;

theorem Th33: :: JORDAN14:33

for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds

for i, j being Nat st i <= len G & j <= width G holds

Int (cell (G,i,j)) c= (L~ f) ` by JORDAN9:14, SUBSET_1:23;

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds

for i, j being Nat st i <= len G & j <= width G holds

Int (cell (G,i,j)) c= (L~ f) ` by JORDAN9:14, SUBSET_1:23;

theorem Th34: :: JORDAN14:34

for C being Simple_closed_curve

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))

proof end;

theorem Th35: :: JORDAN14:35

for C being Simple_closed_curve

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

RightComp (Span (C,n)) c= RightComp (Span (C,m))

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

RightComp (Span (C,n)) c= RightComp (Span (C,m))

proof end;

theorem :: JORDAN14:36

for C being Simple_closed_curve

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

LeftComp (Span (C,m)) c= LeftComp (Span (C,n))

for n, m being Nat st n is_sufficiently_large_for C & n <= m holds

LeftComp (Span (C,m)) c= LeftComp (Span (C,n))

proof end;