:: JORDAN19 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let C be Simple_closed_curve;
func Upper_Appr C -> SetSequence of the carrier of (TOP-REAL 2) means :Def1: :: JORDAN19:def 1
for i being Nat holds it . i = Upper_Arc (L~ (Cage C,i));
existence
ex b1 being SetSequence of the carrier of (TOP-REAL 2) st
for i being Nat holds b1 . i = Upper_Arc (L~ (Cage C,i))
proof end;
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds b1 . i = Upper_Arc (L~ (Cage C,i)) ) & ( for i being Nat holds b2 . i = Upper_Arc (L~ (Cage C,i)) ) holds
b1 = b2
proof end;
func Lower_Appr C -> SetSequence of the carrier of (TOP-REAL 2) means :Def2: :: JORDAN19:def 2
for i being Nat holds it . i = Lower_Arc (L~ (Cage C,i));
existence
ex b1 being SetSequence of the carrier of (TOP-REAL 2) st
for i being Nat holds b1 . i = Lower_Arc (L~ (Cage C,i))
proof end;
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds b1 . i = Lower_Arc (L~ (Cage C,i)) ) & ( for i being Nat holds b2 . i = Lower_Arc (L~ (Cage C,i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Upper_Appr JORDAN19:def 1 :
for C being Simple_closed_curve
for b2 being SetSequence of the carrier of (TOP-REAL 2) holds
( b2 = Upper_Appr C iff for i being Nat holds b2 . i = Upper_Arc (L~ (Cage C,i)) );

:: deftheorem Def2 defines Lower_Appr JORDAN19:def 2 :
for C being Simple_closed_curve
for b2 being SetSequence of the carrier of (TOP-REAL 2) holds
( b2 = Lower_Appr C iff for i being Nat holds b2 . i = Lower_Arc (L~ (Cage C,i)) );

definition
let C be Simple_closed_curve;
func North_Arc C -> Subset of (TOP-REAL 2) equals :: JORDAN19:def 3
 Lim_inf (Upper_Appr C);
coherence
Lim_inf (Upper_Appr C) is Subset of (TOP-REAL 2) ;
func South_Arc C -> Subset of (TOP-REAL 2) equals :: JORDAN19:def 4
 Lim_inf (Lower_Appr C);
coherence
Lim_inf (Lower_Appr C) is Subset of (TOP-REAL 2) ;
end;

:: deftheorem defines North_Arc JORDAN19:def 3 :
for C being Simple_closed_curve holds North_Arc C = Lim_inf (Upper_Appr C);

:: deftheorem defines South_Arc JORDAN19:def 4 :
for C being Simple_closed_curve holds South_Arc C = Lim_inf (Lower_Appr C);

Lm1: now
let G be Go-board; :: thesis: for j being Nat st 1 <= j & j <= width G holds
[(Center G),j] in Indices G
let j be Nat; :: thesis: ( 1 <= j & j <= width G implies [(Center G),j] in Indices G )
assume A1: ( 1 <= j & j <= width G ) ; :: thesis: [(Center G),j] in Indices G
0 + 1 <= ((len G) div 2) + 1 by XREAL_1:8;
then A2: 0 + 1 <= Center G by JORDAN1A:def 1;
Center G <= len G by JORDAN1B:14;
hence [(Center G),j] in Indices G by A1, A2, GOBOARD7:10; :: thesis: verum
end;

Lm2: now
let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [i,(width (Gauge D,n))] in Indices (Gauge D,n) holds
((Gauge D,n) * i,(width (Gauge D,n))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge D,n)) - 2))
let n, i be Nat; :: thesis: ( [i,(width (Gauge D,n))] in Indices (Gauge D,n) implies ((Gauge D,n) * i,(width (Gauge D,n))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge D,n)) - 2)) )
set a = N-bound D;
set s = S-bound D;
set w = W-bound D;
set e = E-bound D;
set G = Gauge D,n;
assume [i,(width (Gauge D,n))] in Indices (Gauge D,n) ; :: thesis: ((Gauge D,n) * i,(width (Gauge D,n))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge D,n)) - 2))
hence ((Gauge D,n) * i,(width (Gauge D,n))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge D,n)) - 2)))]| `2 by JORDAN8:def 1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge D,n)) - 2)) by EUCLID:56 ;
:: thesis: verum
end;

theorem Th1: :: JORDAN19:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m & n <> 0 holds
(n + 1) / n >= (m + 1) / m
proof end;

theorem Th2: :: JORDAN19:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge E,n) holds
LSeg ((Gauge E,n) * (Center (Gauge E,n)),(width (Gauge E,n))),((Gauge E,n) * (Center (Gauge E,n)),j) c= LSeg ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))),((Gauge E,n) * (Center (Gauge E,n)),j)
proof end;

theorem Th3: :: JORDAN19:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n)
proof end;

theorem Th4: :: JORDAN19:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
for i, j being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets Upper_Arc (L~ (Cage C,n))
proof end;

theorem :: JORDAN19:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being Nat st (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_Arc (L~ (Cage C,(n + 1)))
proof end;

theorem Th6: :: JORDAN19:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge C,n & not dist (f /. k),(f /. (k + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds
dist (f /. k),(f /. (k + 1)) = ((E-bound C) - (W-bound C)) / (2 |^ n)
proof end;

theorem :: JORDAN19:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being symmetric triangle MetrStruct
for r being real number
for p, q, x being Element of M st p in Ball x,r & q in Ball x,r holds
dist p,q < 2 * r
proof end;

theorem Th8: :: JORDAN19:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p' being Point of (Euclid n) st p = p' holds
for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p',r meets A )
proof end;

theorem :: JORDAN19:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound C < N-bound (L~ (Cage C,n))
proof end;

theorem Th10: :: JORDAN19:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound C < E-bound (L~ (Cage C,n))
proof end;

theorem :: JORDAN19:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage C,n)) < S-bound C
proof end;

theorem Th12: :: JORDAN19:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage C,n)) < W-bound C
proof end;

theorem Th13: :: JORDAN19:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= k & k <= j & j <= width (Gauge C,n) & (LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j) meets Upper_Arc C
proof end;

theorem Th14: :: JORDAN19:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= k & k <= j & j <= width (Gauge C,n) & (LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,k),((Gauge C,n) * i,j) meets Lower_Arc C
proof end;

theorem :: JORDAN19:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem :: JORDAN19:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th17: :: JORDAN19:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j in L~ (Upper_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem Th18: :: JORDAN19:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j in L~ (Upper_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th19: :: JORDAN19:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (Gauge C,n) * i,k in Lower_Arc (L~ (Cage C,n)) & (Gauge C,n) * i,j in Upper_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem Th20: :: JORDAN19:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (Gauge C,n) * i,k in Lower_Arc (L~ (Cage C,n)) & (Gauge C,n) * i,j in Upper_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th21: :: JORDAN19:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i1,j)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i2,k)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
proof end;

theorem Th22: :: JORDAN19:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i1,j)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i2,k)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
proof end;

theorem Th23: :: JORDAN19:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i1,j)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i2,k)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
proof end;

theorem Th24: :: JORDAN19:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i1,j)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i2,k)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
proof end;

theorem Th25: :: JORDAN19:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge C,(n + 1)) & 1 < i2 & i2 < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i1,k in Lower_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * i2,j in Upper_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Lower_Arc C
proof end;

theorem Th26: :: JORDAN19:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge C,(n + 1)) & 1 < i2 & i2 < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i1,k in Lower_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * i2,j in Upper_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Upper_Arc C
proof end;

theorem Th27: :: JORDAN19:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds
not p in South_Arc C
proof end;

theorem :: JORDAN19:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C holds
not p in South_Arc C
proof end;