:: On the Upper and Lower Approximations of the Curve
:: by Robert Milewski
::
:: Received September 27, 2003
:: Copyright (c) 2003 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
Element of
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 Element of NAT holds b1 . i = Upper_Arc (L~ (Cage C,i))
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds b1 . i = Upper_Arc (L~ (Cage C,i)) ) & ( for i being Element of NAT holds b2 . i = Upper_Arc (L~ (Cage C,i)) ) holds
b1 = b2
func Lower_Appr C -> SetSequence of the
carrier of
(TOP-REAL 2) means :
Def2:
:: JORDAN19:def 2
for
i being
Element of
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 Element of NAT holds b1 . i = Lower_Arc (L~ (Cage C,i))
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds b1 . i = Lower_Arc (L~ (Cage C,i)) ) & ( for i being Element of NAT holds b2 . i = Lower_Arc (L~ (Cage C,i)) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Upper_Appr JORDAN19:def 1 :
:: deftheorem Def2 defines Lower_Appr JORDAN19:def 2 :
:: deftheorem defines North_Arc JORDAN19:def 3 :
:: deftheorem defines South_Arc JORDAN19:def 4 :
Lm2:
now
let D be non
empty Subset of
(TOP-REAL 2);
:: thesis: for n, i being Element of 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
Element of
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
theorem Th2: :: JORDAN19:2
for
n being
Element of
NAT for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
m,
j being
Element of
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)
theorem Th3: :: JORDAN19:3
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j being
Element of
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)
theorem Th4: :: JORDAN19:4
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
i,
j being
Element of
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))
theorem :: JORDAN19:5
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
j being
Element of
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)))
theorem Th6: :: JORDAN19:6
theorem :: JORDAN19:7
theorem :: JORDAN19:8
canceled;
theorem :: JORDAN19:9
theorem Th10: :: JORDAN19:10
theorem :: JORDAN19:11
theorem Th12: :: JORDAN19:12
theorem Th13: :: JORDAN19:13
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th14: :: JORDAN19:14
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem :: JORDAN19:15
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem :: JORDAN19:16
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th17: :: JORDAN19:17
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th18: :: JORDAN19:18
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th19: :: JORDAN19:19
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th20: :: JORDAN19:20
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
theorem Th21: :: JORDAN19:21
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th22: :: JORDAN19:22
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th23: :: JORDAN19:23
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th24: :: JORDAN19:24
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th25: :: JORDAN19:25
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th26: :: JORDAN19:26
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
theorem Th27: :: JORDAN19:27
theorem :: JORDAN19:28