:: On the Upper and Lower Approximations of the Curve
:: by Robert Milewski
::
:: Received September 27, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition
let C be Simple_closed_curve;
func Upper_Appr C -> SetSequence of the carrier of () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () equals :: JORDAN19:def 3
Lim_inf ();
coherence
Lim_inf () is Subset of ()
;
func South_Arc C -> Subset of () equals :: JORDAN19:def 4
Lim_inf ();
coherence
Lim_inf () is Subset of ()
;
end;

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

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

Lm1: now :: thesis: for G being Go-board
for j being Nat st 1 <= j & j <= width G holds
[(),j] in Indices G
let G be Go-board; :: thesis: for j being Nat st 1 <= j & j <= width G holds
[(),j] in Indices G

let j be Nat; :: thesis: ( 1 <= j & j <= width G implies [(),j] in Indices G )
assume that
A1: 1 <= j and
A2: j <= width G ; :: thesis: [(),j] in Indices G
0 + 1 <= ((len G) div 2) + 1 by XREAL_1:6;
then A3: 0 + 1 <= Center G by JORDAN1A:def 1;
Center G <= len G by JORDAN1B:13;
hence [(),j] in Indices G by ; :: thesis: verum
end;

Lm2: now :: thesis: for D being non empty Subset of ()
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 = () + (((() - ()) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))
let D be non empty Subset of (); :: 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 = () + (((() - ()) / (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 = () + (((() - ()) / (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 = () + (((() - ()) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))
hence ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) 2 = |[(() + (((() - ()) / (2 |^ n)) * (i - 2))),(() + (((() - ()) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)))]| 2 by JORDAN8:def 1
.= () + (((() - ()) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) by EUCLID:52 ;
:: thesis: verum
end;

theorem Th1: :: JORDAN19:1
for n, m being Nat st n <= m & n <> 0 holds
(n + 1) / n >= (m + 1) / m
proof end;

theorem Th2: :: JORDAN19:2
for n being Nat
for E being compact non horizontal non vertical Subset of ()
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
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
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
for C being connected compact non horizontal non vertical Subset of ()
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
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
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
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for f being FinSequence of ()
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))) = (() - ()) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n)
proof end;

theorem :: JORDAN19:7
for M being symmetric triangle MetrStruct
for r being Real
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 :: JORDAN19:8
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds N-bound C < N-bound (L~ (Cage (C,n)))
proof end;

theorem Th9: :: JORDAN19:9
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds E-bound C < E-bound (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN19:10
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds S-bound (L~ (Cage (C,n))) < S-bound C
proof end;

theorem Th11: :: JORDAN19:11
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds W-bound (L~ (Cage (C,n))) < W-bound C
proof end;

theorem Th12: :: JORDAN19:12
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 Th13: :: JORDAN19:13
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:14
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:15
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 Th16: :: JORDAN19:16
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 Th17: :: JORDAN19:17
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 Th18: :: JORDAN19:18
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 Th19: :: JORDAN19:19
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 Th20: :: JORDAN19:20
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 Th21: :: JORDAN19:21
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 Th22: :: JORDAN19:22
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 Th23: :: JORDAN19:23
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 Th24: :: JORDAN19:24
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 Th25: :: JORDAN19:25
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 Th26: :: JORDAN19:26
for C being Simple_closed_curve
for p being Point of () 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:27
for C being Simple_closed_curve
for p being Point of () st p `1 = (() + ()) / 2 & p in North_Arc C holds
not p in South_Arc C
proof end;