:: JORDAN11 semantic presentation

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 -> 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 -> 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 A1: n is_sufficiently_large_for C ;
A2: n >= ApproxIndex C by A1, Def1;
set i1 = X-SpanStart C,n;
func Y-SpanStart C,n -> 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;