JORDAN11: Preparing the Internal Approximations of Simple Closed Curves

:: Preparing the Internal Approximations of Simple Closed Curves
:: by Andrzej Trybulec
::
:: Received May 21, 2002
:: Copyright (c) 2002-2011 Association of Mizar Users

begin

Lm1: for i, j, k being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 (TOP-REAL 2) ex n being Element of NAT st n is_sufficiently_large_for C

proof end;

definition

let C be being_simple_closed_curve Subset of (TOP-REAL 2);
func ApproxIndex C -> Element of NAT means :Def1: :: JORDAN11:def 1
( it is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :

theorem Th1: :: JORDAN11:1

for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds ApproxIndex C >= 1

proof end;

definition

let C be being_simple_closed_curve Subset of (TOP-REAL 2);
func Y-InitStart C -> Element of NAT means :Def2: :: JORDAN11:def 2
( it < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it ) );
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines Y-InitStart JORDAN11:def 2 :

theorem Th2: :: JORDAN11:2

for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds Y-InitStart C > 1

proof end;

theorem Th3: :: JORDAN11:3

for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C)))

proof end;

definition

let C be being_simple_closed_curve Subset of (TOP-REAL 2);
let n be Element of 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 Element of NAT st it <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= it ) );
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines Y-SpanStart JORDAN11:def 3 :

theorem Th4: :: JORDAN11:4

for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2

proof end;

theorem Th5: :: JORDAN11:5

for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2

proof end;

theorem Th6: :: JORDAN11:6

for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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 Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) 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;

begin

theorem Th12: :: JORDAN11:12

for C being being_simple_closed_curve Subset of (TOP-REAL 2)
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 (TOP-REAL 2)
for q, p being Point of (TOP-REAL 2) 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 (TOP-REAL 2)
for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2)
for D being Simple_closed_curve st C c= BDD D holds
D c= UBD C

proof end;

theorem :: JORDAN11:17

for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds L~ (Cage (C,n)) c= UBD C

proof end;