:: Preparing the Internal Approximations of Simple Closed Curves
:: by Andrzej Trybulec
::
:: Copyright (c) 2002-2021 Association of Mizar Users

Lm1: for i, j, k being Nat
for C being being_simple_closed_curve Subset of () st i > 0 & 1 <= j & j <= width (Gauge (C,i)) & k <= j & 1 <= k & k <= width (Gauge (C,i)) & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} holds
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i)))

proof end;

Lm2: for C being being_simple_closed_curve Subset of () ex n being Nat st n is_sufficiently_large_for C
proof end;

definition
let C be being_simple_closed_curve Subset of ();
func ApproxIndex C -> Element of NAT means :Def1: :: JORDAN11:def 1
( it is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= it ) );
existence
ex b1 being Element of NAT st
( b1 is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= b1 ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st b1 is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= b1 ) & b2 is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :
for C being being_simple_closed_curve Subset of ()
for b2 being Element of NAT holds
( b2 = ApproxIndex C iff ( b2 is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= b2 ) ) );

theorem Th1: :: JORDAN11:1
for C being being_simple_closed_curve Subset of () holds ApproxIndex C >= 1
proof end;

definition
let C be being_simple_closed_curve Subset of ();
func Y-InitStart C -> Element of NAT means :Def2: :: JORDAN11:def 2
( it < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),it) c= BDD C & ( for j being Nat st j < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),j) c= BDD C holds
j >= it ) );
existence
ex b1 being Element of NAT st
( b1 < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),b1) c= BDD C & ( for j being Nat st j < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),j) c= BDD C holds
j >= b1 ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st b1 < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),b1) c= BDD C & ( for j being Nat st j < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),j) c= BDD C holds
j >= b1 ) & b2 < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),b2) c= BDD C & ( for j being Nat st j < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),j) c= BDD C holds
j >= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Y-InitStart JORDAN11:def 2 :
for C being being_simple_closed_curve Subset of ()
for b2 being Element of NAT holds
( b2 = Y-InitStart C iff ( b2 < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),b2) c= BDD C & ( for j being Nat st j < width (Gauge (C,())) & cell ((Gauge (C,())),((X-SpanStart (C,())) -' 1),j) c= BDD C holds
j >= b2 ) ) );

theorem Th2: :: JORDAN11:2
for C being being_simple_closed_curve Subset of () holds Y-InitStart C > 1
proof end;

theorem Th3: :: JORDAN11:3
for C being being_simple_closed_curve Subset of () holds () + 1 < width (Gauge (C,()))
proof end;

definition
let C be being_simple_closed_curve Subset of ();
let n be Nat;
assume n is_sufficiently_large_for C ;
then A1: n >= ApproxIndex C by Def1;
set i1 = X-SpanStart (C,n);
func Y-SpanStart (C,n) -> Element of NAT means :Def3: :: JORDAN11:def 3
( it <= width (Gauge (C,n)) & ( for k being Nat st it <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= it ) );
existence
ex b1 being Element of NAT st
( b1 <= width (Gauge (C,n)) & ( for k being Nat st b1 <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st b1 <= width (Gauge (C,n)) & ( for k being Nat st b1 <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) & b2 <= width (Gauge (C,n)) & ( for k being Nat st b2 <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Y-SpanStart JORDAN11:def 3 :
for C being being_simple_closed_curve Subset of ()
for n being Nat st n is_sufficiently_large_for C holds
for b3 being Element of NAT holds
( b3 = Y-SpanStart (C,n) iff ( b3 <= width (Gauge (C,n)) & ( for k being Nat st b3 <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' ())) * (() -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b3 ) ) );

theorem Th4: :: JORDAN11:4
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' ())) * ((X-SpanStart (C,())) - 2)) + 2
proof end;

theorem Th5: :: JORDAN11:5
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) <= ((2 |^ (n -' ())) * (() -' 2)) + 2
proof end;

theorem Th6: :: JORDAN11:6
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C
proof end;

theorem Th7: :: JORDAN11:7
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
proof end;

theorem :: JORDAN11:8
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
proof end;

theorem :: JORDAN11:9
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
proof end;

theorem :: JORDAN11:10
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) meets C
proof end;

theorem :: JORDAN11:11
for n being Nat
for C being being_simple_closed_curve Subset of () st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C
proof end;

theorem Th12: :: JORDAN11:12
for C being being_simple_closed_curve Subset of ()
for D being Simple_closed_curve holds UBD C meets UBD D
proof end;

theorem Th13: :: JORDAN11:13
for C being being_simple_closed_curve Subset of ()
for p, q being Point of () st q in UBD C & p in BDD C holds
dist (q,C) < dist (q,p)
proof end;

theorem Th14: :: JORDAN11:14
for C being being_simple_closed_curve Subset of ()
for p being Point of () st not p in BDD C holds
dist (p,C) <= dist (p,(BDD C))
proof end;

theorem Th15: :: JORDAN11:15
for C being being_simple_closed_curve Subset of ()
for D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )
proof end;

theorem Th16: :: JORDAN11:16
for C being being_simple_closed_curve Subset of ()
for D being Simple_closed_curve st C c= BDD D holds
D c= UBD C
proof end;

theorem :: JORDAN11:17
for n being Nat
for C being being_simple_closed_curve Subset of () holds L~ (Cage (C,n)) c= UBD C
proof end;