:: Properties of the Internal Approximation of {J}ordan's Curve
:: by Robert Milewski
::
:: Received June 27, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

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

theorem :: JORDAN14:2
for f being non constant standard special_circular_sequence holds
( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )
proofend;

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 &amp; k + 1 <= len f &amp; f is_sequence_on G holds
left_cell (f,k,G) is closed
proofend;

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 &amp; i + 1 <= len G &amp; 1 <= j &amp; j + 1 <= width G holds
( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 &amp; p `1 < (G * ((i + 1),j)) `1 &amp; (G * (i,j)) `2 < p `2 &amp; p `2 < (G * (i,(j + 1))) `2 ) )
proofend;

theorem Th5: :: JORDAN14:5
for f being non constant standard special_circular_sequence holds BDD (L~ f) is connected
proofend;

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 Th6: :: JORDAN14:6
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
proofend;

theorem Th7: :: JORDAN14:7
for C being Simple_closed_curve
for n, k being Element of NAT st n is_sufficiently_large_for C &amp; 1 <= k &amp; k + 1 <= len (Span (C,n)) holds
( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C &amp; left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )
proofend;

theorem Th8: :: JORDAN14:8
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))
proofend;

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:32;
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 meets LeftComp (Span (C,n))
proofend;

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 misses RightComp (Span (C,n))
proofend;

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 c= LeftComp (Span (C,n))
proofend;

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= UBD (L~ (Span (C,n)))
proofend;

theorem Th13: :: JORDAN14:13
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
proofend;

theorem Th14: :: JORDAN14:14
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)))
proofend;

theorem :: JORDAN14:15
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
proofend;

theorem Th16: :: JORDAN14:16
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))
proofend;

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 misses BDD (L~ (Span (C,n)))
proofend;

theorem :: 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 RightComp (Span (C,n))
proofend;

theorem Th19: :: JORDAN14:19
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 &amp; P is_outside_component_of C holds
P misses L~ (Span (C,n))
proofend;

theorem Th20: :: JORDAN14:20
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))
proofend;

theorem Th21: :: JORDAN14:21
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
proofend;

theorem Th22: :: JORDAN14:22
for C being Simple_closed_curve
for i, j, k, n being Element of NAT st n is_sufficiently_large_for C &amp; 1 <= k &amp; k <= len (Span (C,n)) &amp; [i,j] in Indices (Gauge (C,n)) &amp; (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i > 1
proofend;

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 &amp; 1 <= k &amp; k <= len (Span (C,n)) &amp; [i,j] in Indices (Gauge (C,n)) &amp; (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i < len (Gauge (C,n))
proofend;

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 &amp; 1 <= k &amp; k <= len (Span (C,n)) &amp; [i,j] in Indices (Gauge (C,n)) &amp; (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j > 1
proofend;

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 &amp; 1 <= k &amp; k <= len (Span (C,n)) &amp; [i,j] in Indices (Gauge (C,n)) &amp; (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j < width (Gauge (C,n))
proofend;

theorem :: JORDAN14:26
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))
proofend;

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

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 n <= m &amp; n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
proofend;

theorem Th29: :: JORDAN14:29
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 &amp; f is special &amp; i <= len G &amp; j <= width G holds
(cell (G,i,j)) \ (L~ f) is connected
proofend;

theorem Th30: :: JORDAN14:30
for C being Simple_closed_curve
for n, k being Element of NAT st n is_sufficiently_large_for C &amp; Y-SpanStart (C,n) <= k &amp; 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)))
proofend;

theorem Th31: :: JORDAN14:31
for C being Subset of (TOP-REAL 2)
for n, m, i being Element of NAT st m <= n &amp; 1 < i &amp; i + 1 < len (Gauge (C,m)) holds
(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
proofend;

theorem Th32: :: JORDAN14:32
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C &amp; n <= m holds
RightComp (Span (C,n)) meets RightComp (Span (C,m))
proofend;

theorem Th33: :: JORDAN14:33
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G &amp; f is special holds
for i, j being Element of NAT st i <= len G &amp; j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
proofend;

theorem Th34: :: JORDAN14:34
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C &amp; n <= m holds
L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))
proofend;

theorem Th35: :: JORDAN14:35
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C &amp; n <= m holds
RightComp (Span (C,n)) c= RightComp (Span (C,m))
proofend;

theorem :: JORDAN14:36
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C &amp; n <= m holds
LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
proofend;