:: Gauges and Cages :: by Artur Korni{\l}owicz, Robert Milewski, Adam Naumowicz and :: :: Received September 12, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin 3 = (2 * 1) + 1 ; then Lm1: 3 div 2 = 1 by NAT_D:def_1; 1 = (2 * 0) + 1 ; then Lm2: 1 div 2 = 0 by NAT_D:def_1; definition let f be FinSequence; func Center f -> Element of NAT equals :: JORDAN1A:def 1 ((len f) div 2) + 1; coherence ((len f) div 2) + 1 is Element of NAT ; end; :: deftheorem defines Center JORDAN1A:def_1_:_ for f being FinSequence holds Center f = ((len f) div 2) + 1; theorem :: JORDAN1A:1 for f being FinSequence st len f is odd holds len f = (2 * (Center f)) - 1 proofend; theorem :: JORDAN1A:2 for f being FinSequence st len f is even holds len f = (2 * (Center f)) - 2 proofend; begin registration cluster non empty being_simple_closed_curve compact non horizontal non vertical for Element of K6( the U1 of (TOP-REAL 2)); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is compact & not b1 is vertical & not b1 is horizontal & b1 is being_simple_closed_curve & not b1 is empty ) proofend; end; theorem Th3: :: JORDAN1A:3 for D being non empty Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in N-most D holds p `2 = N-bound D proofend; theorem Th4: :: JORDAN1A:4 for D being non empty Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in E-most D holds p `1 = E-bound D proofend; theorem Th5: :: JORDAN1A:5 for D being non empty Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in S-most D holds p `2 = S-bound D proofend; theorem Th6: :: JORDAN1A:6 for D being non empty Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in W-most D holds p `1 = W-bound D proofend; theorem :: JORDAN1A:7 for D being Subset of (TOP-REAL 2) holds BDD D misses D proofend; theorem Th8: :: JORDAN1A:8 for p being Point of (TOP-REAL 2) holds p in Vertical_Line (p `1) proofend; theorem :: JORDAN1A:9 for r, s being real number holds |[r,s]| in Vertical_Line r proofend; theorem :: JORDAN1A:10 for s being real number for A being Subset of (TOP-REAL 2) st A c= Vertical_Line s holds A is vertical proofend; theorem :: JORDAN1A:11 for p, q being Point of (TOP-REAL 2) for r being real number st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds |[(p `1),r]| in LSeg (p,q) proofend; theorem :: JORDAN1A:12 for p, q being Point of (TOP-REAL 2) for r being real number st p `2 = q `2 & r in [.(proj1 . p),(proj1 . q).] holds |[r,(p `2)]| in LSeg (p,q) proofend; theorem :: JORDAN1A:13 for p, q being Point of (TOP-REAL 2) for s being real number st p in Vertical_Line s & q in Vertical_Line s holds LSeg (p,q) c= Vertical_Line s proofend; theorem :: JORDAN1A:14 for A, B being Subset of (TOP-REAL 2) st A meets B holds proj2 .: A meets proj2 .: B proofend; theorem :: JORDAN1A:15 for s being real number for A, B being Subset of (TOP-REAL 2) st A misses B & A c= Vertical_Line s & B c= Vertical_Line s holds proj2 .: A misses proj2 .: B proofend; begin theorem :: JORDAN1A:16 for i, j being Element of NAT for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds G * (i,j) in LSeg ((G * (i,1)),(G * (i,(width G)))) proofend; theorem :: JORDAN1A:17 for i, j being Element of NAT for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds G * (i,j) in LSeg ((G * (1,j)),(G * ((len G),j))) proofend; theorem Th18: :: JORDAN1A:18 for j1, j2, i1, i2 being Element of NAT for G being Go-board st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 <= i2 & i2 <= len G holds (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 proofend; theorem Th19: :: JORDAN1A:19 for i1, i2, j1, j2 being Element of NAT for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= j2 & j2 <= width G holds (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 proofend; theorem Th20: :: JORDAN1A:20 for t being Element of NAT for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds (G * (t,(width G))) `2 >= N-bound (L~ f) proofend; theorem Th21: :: JORDAN1A:21 for t being Element of NAT for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds (G * (1,t)) `1 <= W-bound (L~ f) proofend; theorem Th22: :: JORDAN1A:22 for t being Element of NAT for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds (G * (t,1)) `2 <= S-bound (L~ f) proofend; theorem Th23: :: JORDAN1A:23 for t being Element of NAT for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds (G * ((len G),t)) `1 >= E-bound (L~ f) proofend; theorem Th24: :: JORDAN1A:24 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds not cell (G,i,j) is empty proofend; theorem Th25: :: JORDAN1A:25 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds cell (G,i,j) is connected proofend; theorem Th26: :: JORDAN1A:26 for i being Element of NAT for G being Go-board st i <= len G holds not cell (G,i,0) is bounded proofend; theorem Th27: :: JORDAN1A:27 for i being Element of NAT for G being Go-board st i <= len G holds not cell (G,i,(width G)) is bounded proofend; begin theorem :: JORDAN1A:28 for n being Element of NAT for D being non empty Subset of (TOP-REAL 2) holds width (Gauge (D,n)) = (2 |^ n) + 3 proofend; theorem :: JORDAN1A:29 for i, j being Element of NAT for D being non empty Subset of (TOP-REAL 2) st i < j holds len (Gauge (D,i)) < len (Gauge (D,j)) proofend; theorem :: JORDAN1A:30 for i, j being Element of NAT for D being non empty Subset of (TOP-REAL 2) st i <= j holds len (Gauge (D,i)) <= len (Gauge (D,j)) proofend; theorem Th31: :: JORDAN1A:31 for m, n, i being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) holds ( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge (D,n)) ) proofend; theorem Th32: :: JORDAN1A:32 for m, n, i being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < width (Gauge (D,m)) holds ( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < width (Gauge (D,n)) ) proofend; theorem Th33: :: JORDAN1A:33 for m, n, i, j being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) & 1 < j & j < width (Gauge (D,m)) holds for i1, j1 being Element of NAT st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds (Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1) proofend; theorem Th34: :: JORDAN1A:34 for m, n, i being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (D,m)) holds ( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= len (Gauge (D,n)) ) proofend; theorem Th35: :: JORDAN1A:35 for m, n, i being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < width (Gauge (D,m)) holds ( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= width (Gauge (D,n)) ) proofend; Lm3: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n_being_Element_of_NAT_holds_ (_1_<=_Center_(Gauge_(D,n))_&_Center_(Gauge_(D,n))_<=_len_(Gauge_(D,n))_) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds ( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) ) let n be Element of NAT ; ::_thesis: ( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) ) set G = Gauge (D,n); 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 by XREAL_1:6; hence 1 <= Center (Gauge (D,n)) ; ::_thesis: Center (Gauge (D,n)) <= len (Gauge (D,n)) 0 < len (Gauge (D,n)) by JORDAN8:10; then (len (Gauge (D,n))) div 2 < len (Gauge (D,n)) by INT_1:56; hence Center (Gauge (D,n)) <= len (Gauge (D,n)) by NAT_1:13; ::_thesis: verum end; Lm4: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_len_(Gauge_(D,n))_holds_ [(Center_(Gauge_(D,n))),j]_in_Indices_(Gauge_(D,n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) let n, j be Element of NAT ; ::_thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) ) set G = Gauge (D,n); assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; ::_thesis: [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def_1, XREAL_1:6; Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3; hence [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) by A1, A2, MATRIX_1:36; ::_thesis: verum end; Lm5: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_len_(Gauge_(D,n))_holds_ [j,(Center_(Gauge_(D,n)))]_in_Indices_(Gauge_(D,n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, j being Element of NAT st 1 <= j & j <= len (Gauge (D,n)) holds [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) let n, j be Element of NAT ; ::_thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) ) set G = Gauge (D,n); assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; ::_thesis: [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def_1, XREAL_1:6; Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3; hence [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) by A1, A2, MATRIX_1:36; ::_thesis: verum end; Lm6: for n being Element of NAT for D being non empty Subset of (TOP-REAL 2) for w being real number st n > 0 holds (w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2 proofend; Lm7: now__::_thesis:_for_m,_n_being_Element_of_NAT_ for_c,_d_being_real_number_st_0_<=_c_&_m_<=_n_holds_ c_/_(2_|^_n)_<=_c_/_(2_|^_m) let m, n be Element of NAT ; ::_thesis: for c, d being real number st 0 <= c & m <= n holds c / (2 |^ n) <= c / (2 |^ m) let c, d be real number ; ::_thesis: ( 0 <= c & m <= n implies c / (2 |^ n) <= c / (2 |^ m) ) assume A1: 0 <= c ; ::_thesis: ( m <= n implies c / (2 |^ n) <= c / (2 |^ m) ) assume m <= n ; ::_thesis: c / (2 |^ n) <= c / (2 |^ m) then ( 0 < 2 |^ m & 2 |^ m <= 2 |^ n ) by NEWTON:83, PREPOWER:93; hence c / (2 |^ n) <= c / (2 |^ m) by A1, XREAL_1:118; ::_thesis: verum end; Lm8: now__::_thesis:_for_m,_n_being_Element_of_NAT_ for_c,_d_being_real_number_st_0_<=_c_&_m_<=_n_holds_ d_+_(c_/_(2_|^_n))_<=_d_+_(c_/_(2_|^_m)) let m, n be Element of NAT ; ::_thesis: for c, d being real number st 0 <= c & m <= n holds d + (c / (2 |^ n)) <= d + (c / (2 |^ m)) let c, d be real number ; ::_thesis: ( 0 <= c & m <= n implies d + (c / (2 |^ n)) <= d + (c / (2 |^ m)) ) assume ( 0 <= c & m <= n ) ; ::_thesis: d + (c / (2 |^ n)) <= d + (c / (2 |^ m)) then c / (2 |^ n) <= c / (2 |^ m) by Lm7; hence d + (c / (2 |^ n)) <= d + (c / (2 |^ m)) by XREAL_1:6; ::_thesis: verum end; Lm9: now__::_thesis:_for_m,_n_being_Element_of_NAT_ for_c,_d_being_real_number_st_0_<=_c_&_m_<=_n_holds_ d_-_(c_/_(2_|^_m))_<=_d_-_(c_/_(2_|^_n)) let m, n be Element of NAT ; ::_thesis: for c, d being real number st 0 <= c & m <= n holds d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) let c, d be real number ; ::_thesis: ( 0 <= c & m <= n implies d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) ) assume ( 0 <= c & m <= n ) ; ::_thesis: d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) then c / (2 |^ n) <= c / (2 |^ m) by Lm7; hence d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) by XREAL_1:13; ::_thesis: verum end; theorem Th36: :: JORDAN1A:36 for i, n, j, m being Element of NAT for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 proofend; theorem :: JORDAN1A:37 for i, n, j, m being Element of NAT for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds ((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2 proofend; Lm10: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n_being_Element_of_NAT_ for_e,_w_being_real_number_holds_w_+_(((e_-_w)_/_(2_|^_n))_*_((len_(Gauge_(D,n)))_-_2))_=_e_+_((e_-_w)_/_(2_|^_n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for e, w being real number holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n)) let n be Element of NAT ; ::_thesis: for e, w being real number holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n)) let e, w be real number ; ::_thesis: w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n)) A1: 2 |^ n <> 0 by NEWTON:83; thus w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = w + (((e - w) / (2 |^ n)) * (((2 |^ n) + 3) - 2)) by JORDAN8:def_1 .= (w + (((e - w) / (2 |^ n)) * (2 |^ n))) + ((e - w) / (2 |^ n)) .= (w + (e - w)) + ((e - w) / (2 |^ n)) by A1, XCMPLX_1:87 .= e + ((e - w) / (2 |^ n)) ; ::_thesis: verum end; Lm11: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_i_being_Element_of_NAT_st_[i,1]_in_Indices_(Gauge_(D,n))_holds_ ((Gauge_(D,n))_*_(i,1))_`2_=_(S-bound_D)_-_(((N-bound_D)_-_(S-bound_D))_/_(2_|^_n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, i being Element of NAT st [i,1] in Indices (Gauge (D,n)) holds ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) let n, i be Element of NAT ; ::_thesis: ( [i,1] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) ) 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,1] in Indices (Gauge (D,n)) ; ::_thesis: ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) hence ((Gauge (D,n)) * (i,1)) `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)) * (1 - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) by EUCLID:52 ; ::_thesis: verum end; Lm12: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_i_being_Element_of_NAT_st_[1,i]_in_Indices_(Gauge_(D,n))_holds_ ((Gauge_(D,n))_*_(1,i))_`1_=_(W-bound_D)_-_(((E-bound_D)_-_(W-bound_D))_/_(2_|^_n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, i being Element of NAT st [1,i] in Indices (Gauge (D,n)) holds ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) let n, i be Element of NAT ; ::_thesis: ( [1,i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) ) 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 [1,i] in Indices (Gauge (D,n)) ; ::_thesis: ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) hence ((Gauge (D,n)) * (1,i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) by EUCLID:52 ; ::_thesis: verum end; Lm13: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_i_being_Element_of_NAT_st_[i,(len_(Gauge_(D,n)))]_in_Indices_(Gauge_(D,n))_holds_ ((Gauge_(D,n))_*_(i,(len_(Gauge_(D,n)))))_`2_=_(N-bound_D)_+_(((N-bound_D)_-_(S-bound_D))_/_(2_|^_n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, i being Element of NAT st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) let n, i be Element of NAT ; ::_thesis: ( [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) ) 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,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) ; ::_thesis: ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) hence ((Gauge (D,n)) * (i,(len (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)) * ((len (Gauge (D,n))) - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52 .= (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) by Lm10 ; ::_thesis: verum end; Lm14: now__::_thesis:_for_D_being_non_empty_Subset_of_(TOP-REAL_2) for_n,_i_being_Element_of_NAT_st_[(len_(Gauge_(D,n))),i]_in_Indices_(Gauge_(D,n))_holds_ ((Gauge_(D,n))_*_((len_(Gauge_(D,n))),i))_`1_=_(E-bound_D)_+_(((E-bound_D)_-_(W-bound_D))_/_(2_|^_n)) let D be non empty Subset of (TOP-REAL 2); ::_thesis: for n, i being Element of NAT st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) let n, i be Element of NAT ; ::_thesis: ( [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) ) 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 [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) ; ::_thesis: ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) hence ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52 .= (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) by Lm10 ; ::_thesis: verum end; theorem :: JORDAN1A:38 for i being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds ((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 proofend; theorem :: JORDAN1A:39 for i being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds ((Gauge (C,1)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-bound C)) / 2 proofend; theorem Th40: :: JORDAN1A:40 for i, n, j, m being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds ((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2 proofend; theorem :: JORDAN1A:41 for i, n, j, m being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds ((Gauge (E,n)) * ((len (Gauge (E,n))),i)) `1 <= ((Gauge (E,m)) * ((len (Gauge (E,m))),j)) `1 proofend; theorem :: JORDAN1A:42 for i, n, j, m being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds ((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1 proofend; theorem :: JORDAN1A:43 for i, n, j, m being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds ((Gauge (E,m)) * (j,1)) `2 <= ((Gauge (E,n)) * (i,1)) `2 proofend; theorem :: JORDAN1A:44 for m, n being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n holds LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n)))))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) proofend; theorem :: JORDAN1A:45 for m, n, j being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) proofend; theorem :: JORDAN1A:46 for m, n, j being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) proofend; theorem Th47: :: JORDAN1A:47 for m, n, i, j being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds for i1, j1 being Element of NAT st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j) proofend; theorem :: JORDAN1A:48 for m, n, i, j being Element of NAT for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 3 <= i & i < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds for i1, j1 being Element of NAT st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j) proofend; theorem :: JORDAN1A:49 for i, n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (C,n)) holds cell ((Gauge (C,n)),i,0) c= UBD C proofend; theorem :: JORDAN1A:50 for i, n being Element of NAT for E, C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (E,n)) holds cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E proofend; begin theorem Th51: :: JORDAN1A:51 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in C holds north_halfline p meets L~ (Cage (C,n)) proofend; theorem Th52: :: JORDAN1A:52 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in C holds east_halfline p meets L~ (Cage (C,n)) proofend; theorem Th53: :: JORDAN1A:53 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in C holds south_halfline p meets L~ (Cage (C,n)) proofend; theorem Th54: :: JORDAN1A:54 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in C holds west_halfline p meets L~ (Cage (C,n)) proofend; Lm15: for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) ) proofend; Lm16: for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) ) proofend; Lm17: for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) ) proofend; theorem Th55: :: JORDAN1A:55 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) ) proofend; theorem Th56: :: JORDAN1A:56 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) ) proofend; theorem Th57: :: JORDAN1A:57 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st ( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) ) proofend; theorem Th58: :: JORDAN1A:58 for k, n, t being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) holds (Cage (C,n)) /. k in N-most (L~ (Cage (C,n))) proofend; theorem Th59: :: JORDAN1A:59 for k, n, t being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) holds (Cage (C,n)) /. k in W-most (L~ (Cage (C,n))) proofend; theorem Th60: :: JORDAN1A:60 for k, n, t being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) holds (Cage (C,n)) /. k in S-most (L~ (Cage (C,n))) proofend; theorem Th61: :: JORDAN1A:61 for k, n, t being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) holds (Cage (C,n)) /. k in E-most (L~ (Cage (C,n))) proofend; theorem Th62: :: JORDAN1A:62 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) - (((E-bound C) - (W-bound C)) / (2 |^ n)) proofend; theorem Th63: :: JORDAN1A:63 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) - (((N-bound C) - (S-bound C)) / (2 |^ n)) proofend; theorem Th64: :: JORDAN1A:64 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound (L~ (Cage (C,n))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) proofend; theorem :: JORDAN1A:65 for n, m being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m)))) proofend; theorem :: JORDAN1A:66 for n, m being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n)))) = (E-bound (L~ (Cage (C,m)))) + (W-bound (L~ (Cage (C,m)))) proofend; theorem :: JORDAN1A:67 for i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i))) proofend; theorem :: JORDAN1A:68 for i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds W-bound (L~ (Cage (C,i))) < W-bound (L~ (Cage (C,j))) proofend; theorem :: JORDAN1A:69 for i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j))) proofend; theorem :: JORDAN1A:70 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds N-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `2 proofend; theorem :: JORDAN1A:71 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),i)) `1 proofend; theorem :: JORDAN1A:72 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2 proofend; theorem :: JORDAN1A:73 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds W-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (1,i)) `1 proofend; theorem Th74: :: JORDAN1A:74 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds p `2 > x `2 proofend; theorem Th75: :: JORDAN1A:75 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds p `1 > x `1 proofend; theorem Th76: :: JORDAN1A:76 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds p `2 < x `2 proofend; theorem Th77: :: JORDAN1A:77 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds p `1 < x `1 proofend; theorem Th78: :: JORDAN1A:78 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in N-most C & p in north_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds LSeg ((Cage (C,n)),i) is horizontal proofend; theorem Th79: :: JORDAN1A:79 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds LSeg ((Cage (C,n)),i) is vertical proofend; theorem Th80: :: JORDAN1A:80 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in S-most C & p in south_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds LSeg ((Cage (C,n)),i) is horizontal proofend; theorem Th81: :: JORDAN1A:81 for i, n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in W-most C & p in west_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds LSeg ((Cage (C,n)),i) is vertical proofend; theorem Th82: :: JORDAN1A:82 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in N-most C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds p `2 = N-bound (L~ (Cage (C,n))) proofend; theorem Th83: :: JORDAN1A:83 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds p `1 = E-bound (L~ (Cage (C,n))) proofend; theorem Th84: :: JORDAN1A:84 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in S-most C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds p `2 = S-bound (L~ (Cage (C,n))) proofend; theorem Th85: :: JORDAN1A:85 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x, p being Point of (TOP-REAL 2) st x in W-most C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds p `1 = W-bound (L~ (Cage (C,n))) proofend; theorem :: JORDAN1A:86 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x being Point of (TOP-REAL 2) st x in N-most C holds ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p} proofend; theorem :: JORDAN1A:87 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x being Point of (TOP-REAL 2) st x in E-most C holds ex p being Point of (TOP-REAL 2) st (east_halfline x) /\ (L~ (Cage (C,n))) = {p} proofend; theorem :: JORDAN1A:88 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x being Point of (TOP-REAL 2) st x in S-most C holds ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p} proofend; theorem :: JORDAN1A:89 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for x being Point of (TOP-REAL 2) st x in W-most C holds ex p being Point of (TOP-REAL 2) st (west_halfline x) /\ (L~ (Cage (C,n))) = {p} proofend;