:: 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 (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 :: thesis: for G being Go-board
for j being Nat st 1 <= j & j <= width G holds
[(Center G),j] in Indices G
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 that
A1: 1 <= j and
A2: j <= width G ; :: thesis: [(Center G),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 [(Center G),j] in Indices G by A1, A2, A3, MATRIX_0:30; :: thesis: verum
end;

Lm2: now :: thesis: for D being non empty Subset of (TOP-REAL 2)
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 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: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 (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
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
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
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
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
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (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:27
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;