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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, TOPREAL2, EUCLID, XXREAL_0, CARD_1, TREES_1, JORDAN8, RLTOPSP1, RELAT_1, JORDAN1A, XBOOLE_0, JORDAN6, TOPREAL1, JORDAN9, TARSKI, PRE_TOPC, GOBOARD9, JORDAN1H, ARYTM_3, FINSEQ_1, MATRIX_1, JORDAN1E, CONNSP_1, PSCOMP_1, INT_1, MCART_1, FUNCT_1, SEQ_4, SEQ_1, RCOMP_1, STRUCT_0, REAL_1, ZFMISC_1, RELAT_2, XXREAL_2, XXREAL_1, JORDAN10, JORDAN2C, SETFAM_1, GOBOARD5, ARYTM_1, NEWTON, METRIC_1, JORDAN11, MEASURE5, CONVEX1, FUNCT_7, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_D, NEWTON, XXREAL_2, SEQ_4, FUNCT_1, RELSET_1, FUNCT_2, NAT_1, FINSEQ_1, MATRIX_0, SEQ_1, RCOMP_1, STRUCT_0, PRE_TOPC, METRIC_1, METRIC_6, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD5, GOBOARD9, PSCOMP_1, JORDAN2C, JORDAN6, JORDAN8, JORDAN9, JORDAN10, JORDAN1A, JORDAN1E, JORDAN1H, TOPREAL6, JORDAN1K;
definitions TARSKI, XBOOLE_0, JORDAN1H;
theorems SEQ_4, JORDAN8, NEWTON, NAT_1, GOBOARD7, GOBOARD5, XBOOLE_0, XBOOLE_1, JORDAN2C, SUBSET_1, GOBOARD9, ZFMISC_1, EUCLID, JORDAN6, PSCOMP_1, SPRECT_1, TARSKI, TOPREAL3, SETFAM_1, RCOMP_1, RELAT_1, FUNCT_2, TOPREAL1, PRE_TOPC, JORDAN1A, ENUMSET1, FUNCT_1, JCT_MISC, JORDAN10, GOBRD14, JORDAN1B, JORDAN1C, JORDAN1F, JORDAN1G, JORDAN1H, JORDAN1I, JORDAN1J, PREPOWER, XREAL_1, JORDAN1K, METRIC_6, WEIERSTR, JORDAN9, XXREAL_0, JORDAN1, INT_1, MATRIX_0, XXREAL_2, NAT_D, RLTOPSP1, ORDINAL1;
schemes DOMAIN_1, FUNCT_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, COMPTS_1, TBSP_1, EUCLID, TOPREAL1, TOPREAL2, SPPOL_2, PSCOMP_1, TOPREAL5, SPRECT_2, JORDAN6, JORDAN2C, TOPREAL6, JORDAN8, JORDAN10, VALUED_0, XXREAL_2, JORDAN, RLTOPSP1, JORDAN1, JORDAN5A, NEWTON;
constructors HIDDEN, REAL_1, NAT_D, RCOMP_1, NEWTON, BINARITH, TOPS_1, CONNSP_1, TBSP_1, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, JORDAN1K, JORDAN8, JORDAN9, JORDAN10, JORDAN1A, JORDAN1E, JORDAN1H, SEQ_4, CONVEX1, GOBOARD1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, JORDAN1H, PSCOMP_1, SUBSET_1;
expansions TARSKI, XBOOLE_0, JORDAN1H;

Lm1: for i, j, k being 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 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 Nat st j is_sufficiently_large_for C holds
j >= it ) );

existence

proof end;

uniqueness

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

uniqueness

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 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 -' (ApproxIndex C))) * ((Y-InitStart C) -' 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 -' (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;

uniqueness

proof end;

end;

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

theorem Th4: :: JORDAN11:4

for n being 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 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 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 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 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 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 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 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;

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 p, q 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 Nat
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds L~ (Cage (C,n)) c= UBD C

proof end;