:: Preparing the Internal Approximations of Simple Closed Curves :: by Andrzej Trybulec :: :: Received May 21, 2002 :: Copyright (c) 2002-2012 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))) proofend; 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 proofend; 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 ex b1 being Element of NAT st ( b1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds j >= b1 ) ) proofend; uniqueness for b1, b2 being Element of NAT st b1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds j >= b1 ) & b2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds j >= b2 ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines ApproxIndex JORDAN11:def_1_:_ for C being being_simple_closed_curve Subset of (TOP-REAL 2) for b2 being Element of NAT holds ( b2 = ApproxIndex C iff ( b2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds j >= b2 ) ) ); theorem Th1: :: JORDAN11:1 for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds ApproxIndex C >= 1 proofend; 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 ex b1 being Element of NAT st ( b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) 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 >= b1 ) ) proofend; uniqueness for b1, b2 being Element of NAT st b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) 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 >= b1 ) & b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) 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 >= b2 ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Y-InitStart JORDAN11:def_2_:_ for C being being_simple_closed_curve Subset of (TOP-REAL 2) for b2 being Element of NAT holds ( b2 = Y-InitStart C iff ( b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) 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 >= b2 ) ) ); theorem Th2: :: JORDAN11:2 for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds Y-InitStart C > 1 proofend; 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))) proofend; 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 ex b1 being Element of NAT st ( b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= 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 >= b1 ) ) proofend; uniqueness for b1, b2 being Element of NAT st b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= 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 >= b1 ) & b2 <= width (Gauge (C,n)) & ( for k being Element of NAT st b2 <= 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 >= b2 ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Y-SpanStart JORDAN11:def_3_:_ for C being being_simple_closed_curve Subset of (TOP-REAL 2) for n being Element of 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 Element of NAT st b3 <= 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 >= b3 ) ) ); 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 proofend; 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 proofend; 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 proofend; 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)) ) proofend; 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)) proofend; 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)) proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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)) proofend; 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 ) proofend; 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 proofend; 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 proofend;