:: On the Upper and Lower Approximations of the Curve :: by Robert Milewski :: :: Received September 27, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin 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))) proofend; 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 proofend; 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))) proofend; 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 proofend; 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 Element of 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 Element of 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_Element_of_NAT_st_1_<=_j_&_j_<=_width_G_holds_ [(Center_G),j]_in_Indices_G let G be Go-board; ::_thesis: for j being Element of NAT st 1 <= j & j <= width G holds [(Center G),j] in Indices G let j be Element of 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_1:36; ::_thesis: verum end; Lm2: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) 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 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:52 ; ::_thesis: verum end; theorem Th1: :: JORDAN19:1 for n, m being Element of NAT st n <= m & n <> 0 holds (n + 1) / n >= (m + 1) / m proofend; 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))) proofend; 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)) proofend; 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))) proofend; 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)))) proofend; theorem Th6: :: JORDAN19:6 for n being Element of 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 Element of 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) proofend; theorem :: JORDAN19:7 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 proofend; theorem :: JORDAN19:8 for n being Element of 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))) proofend; theorem Th9: :: JORDAN19:9 for n being Element of 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))) proofend; theorem :: JORDAN19:10 for n being Element of 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 proofend; theorem Th11: :: JORDAN19:11 for n being Element of 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 proofend; theorem Th12: :: JORDAN19:12 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 proofend; 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 Lower_Arc C proofend; theorem :: 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 <= 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 proofend; 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 Lower_Arc C proofend; theorem Th16: :: 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)) & (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 proofend; 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 Lower_Arc C proofend; 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)) & 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 proofend; 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 Lower_Arc C proofend; theorem Th20: :: JORDAN19:20 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 proofend; 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 Lower_Arc C proofend; 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 < 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 proofend; 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 Lower_Arc C proofend; 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 < 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 proofend; 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 Upper_Arc C proofend; 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 proofend; 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 proofend;