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