:: Properties of the Internal Approximation of {J}ordan's Curve
:: by Robert Milewski
::
:: Received June 27, 2002
:: Copyright (c) 2002 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 )

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 )

proof end;

theorem :: JORDAN14:3

for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for k being Element of 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 Element of 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;

theorem Th5: :: JORDAN14:5

for f being non constant standard special_circular_sequence holds BDD (L~ f) is connected

proof end;

registration

let f be non constant standard special_circular_sequence;
cluster BDD (L~ f) -> connected ;
coherence
BDD (L~ f) is connected by Th5;

end;

definition

let C be Simple_closed_curve;
let n be Element of 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) is Point of (TOP-REAL 2) ;

end;

:: deftheorem defines SpanStart JORDAN14:def 1 :

for C being Simple_closed_curve
for n being Element of NAT holds SpanStart C,n = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n);

theorem :: JORDAN14:6

canceled;

theorem Th7: :: JORDAN14:7

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
SpanStart C,n in BDD C

proof end;

theorem Th8: :: JORDAN14:8

for C being Simple_closed_curve
for n, k being Element of 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 Th9: :: JORDAN14:9

for C being Simple_closed_curve
for n being Element of 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 Element of NAT ;
cluster Cl (RightComp (Span C,n)) -> compact ;
coherence
Cl (RightComp (Span C,n)) is compact by GOBRD14:42;

end;

theorem Th10: :: JORDAN14:10

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C meets LeftComp (Span C,n)

proof end;

theorem Th11: :: JORDAN14:11

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C misses RightComp (Span C,n)

proof end;

theorem Th12: :: JORDAN14:12

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C c= LeftComp (Span C,n)

proof end;

theorem Th13: :: JORDAN14:13

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C c= UBD (L~ (Span C,n))

proof end;

theorem Th14: :: JORDAN14:14

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
BDD (L~ (Span C,n)) c= BDD C

proof end;

theorem Th15: :: JORDAN14:15

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span C,n))

proof end;

theorem :: JORDAN14:16

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
RightComp (Span C,n) c= BDD C

proof end;

theorem Th17: :: JORDAN14:17

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span C,n)

proof end;

theorem Th18: :: JORDAN14:18

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses BDD (L~ (Span C,n))

proof end;

theorem :: JORDAN14:19

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses RightComp (Span C,n)

proof end;

theorem Th20: :: JORDAN14:20

for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span C,n)

proof end;

theorem Th21: :: JORDAN14:21

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses L~ (Span C,n)

proof end;

theorem Th22: :: JORDAN14:22

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
L~ (Span C,n) c= BDD C

proof end;

theorem Th23: :: JORDAN14:23

for C being Simple_closed_curve
for i, j, k, n being Element of 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 Th24: :: JORDAN14:24

for C being Simple_closed_curve
for i, j, k, n being Element of 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 Th25: :: JORDAN14:25

for C being Simple_closed_curve
for i, j, k, n being Element of 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 Th26: :: JORDAN14:26

for C being Simple_closed_curve
for i, j, k, n being Element of 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:27

for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
Y-SpanStart C,n < width (Gauge C,n)

proof end;

theorem Th28: :: JORDAN14:28

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Element of NAT st m >= n & n >= 1 holds
X-SpanStart C,m = ((2 |^ (m -' n)) * ((X-SpanStart C,n) - 2)) + 2

proof end;

theorem Th29: :: JORDAN14:29

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C

proof end;

theorem Th30: :: JORDAN14:30

for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for i, j being Element of 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 Th31: :: JORDAN14:31

for C being Simple_closed_curve
for n, k being Element of 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 Th32: :: JORDAN14:32

for C being Subset of (TOP-REAL 2)
for n, m, i being Element of 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 Th33: :: JORDAN14:33

for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span C,n) meets RightComp (Span C,m)

proof end;

theorem Th34: :: JORDAN14:34

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 Element of NAT st i <= len G & j <= width G holds
Int (cell G,i,j) c= (L~ f) `

proof end;

theorem Th35: :: JORDAN14:35

for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
L~ (Span C,m) c= Cl (LeftComp (Span C,n))

proof end;

theorem Th36: :: JORDAN14:36

for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span C,n) c= RightComp (Span C,m)

proof end;

theorem :: JORDAN14:37

for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
LeftComp (Span C,m) c= LeftComp (Span C,n)

proof end;