:: by Andrzej Trybulec

::

:: Received May 21, 2002

:: Copyright (c) 2002-2019 Association of Mizar Users

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

ex b_{1} being Element of NAT st

( b_{1} is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds

j >= b_{1} ) )

for b_{1}, b_{2} being Element of NAT st b_{1} is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds

j >= b_{1} ) & b_{2} is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds

j >= b_{2} ) holds

b_{1} = b_{2}

end;
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 ( it is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds

j >= it ) );

ex b

( b

j >= b

proof end;

uniqueness for b

j >= b

j >= b

b

proof end;

:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for b_{2} being Element of NAT holds

( b_{2} = ApproxIndex C iff ( b_{2} is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds

j >= b_{2} ) ) );

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for b

( b

j >= b

definition

let C be being_simple_closed_curve Subset of (TOP-REAL 2);

ex b_{1} being Element of NAT st

( b_{1} < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b_{1}) 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 >= b_{1} ) )

for b_{1}, b_{2} being Element of NAT st b_{1} < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b_{1}) 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 >= b_{1} ) & b_{2} < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b_{2}) 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 >= b_{2} ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( b

j >= b

proof end;

uniqueness for b

j >= b

j >= b

b

proof end;

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

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for b_{2} being Element of NAT holds

( b_{2} = Y-InitStart C iff ( b_{2} < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b_{2}) 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 >= b_{2} ) ) );

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for b

( b

j >= b

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

ex b_{1} being Element of NAT st

( b_{1} <= width (Gauge (C,n)) & ( for k being Nat st b_{1} <= 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 >= b_{1} ) )

for b_{1}, b_{2} being Element of NAT st b_{1} <= width (Gauge (C,n)) & ( for k being Nat st b_{1} <= 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 >= b_{1} ) & b_{2} <= width (Gauge (C,n)) & ( for k being Nat st b_{2} <= 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 >= b_{2} ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( b

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 >= b

proof end;

uniqueness for b

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 >= b

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 >= b

b

proof end;

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

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for n being Nat st n is_sufficiently_large_for C holds

for b_{3} being Element of NAT holds

( b_{3} = Y-SpanStart (C,n) iff ( b_{3} <= width (Gauge (C,n)) & ( for k being Nat st b_{3} <= 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 >= b_{3} ) ) );

for C being being_simple_closed_curve Subset of (TOP-REAL 2)

for n being Nat st n is_sufficiently_large_for C holds

for b

( b

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 >= b

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

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

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

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

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

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

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

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

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

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)

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

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 )

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

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

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

proof end;