:: Bounding Boxes for Special Sequences in ${\calE}^2$ :: by Yatsuka Nakamura and Adam Grabowski :: :: Received June 8, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin theorem Th1: :: JORDAN5D:1 for n being Element of NAT for h being FinSequence of (TOP-REAL n) st len h >= 2 holds h /. (len h) in LSeg (h,((len h) -' 1)) proofend; theorem Th2: :: JORDAN5D:2 for i being Element of NAT st 3 <= i holds i mod (i -' 1) = 1 proofend; theorem Th3: :: JORDAN5D:3 for p being Point of (TOP-REAL 2) for h being non constant standard special_circular_sequence st p in rng h holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) proofend; theorem Th4: :: JORDAN5D:4 for r being Real for g being FinSequence of REAL st r in rng g holds ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) proofend; theorem Th5: :: JORDAN5D:5 for h being non constant standard special_circular_sequence for i, I being Element of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) holds ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) proofend; theorem Th6: :: JORDAN5D:6 for h being non constant standard special_circular_sequence for i, I being Element of NAT st 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) holds ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) proofend; theorem Th7: :: JORDAN5D:7 for f being non empty FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i <= len (GoB f) holds ex k, j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) proofend; theorem Th8: :: JORDAN5D:8 for f being non empty FinSequence of (TOP-REAL 2) for j being Element of NAT st 1 <= j & j <= width (GoB f) holds ex k, i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) proofend; theorem Th9: :: JORDAN5D:9 for f being non empty FinSequence of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) proofend; theorem Th10: :: JORDAN5D:10 for f being non empty FinSequence of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) proofend; begin theorem Th11: :: JORDAN5D:11 for h being non constant standard special_circular_sequence for i being Element of NAT st 1 <= i & i <= len h holds ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) proofend; theorem Th12: :: JORDAN5D:12 for h being non constant standard special_circular_sequence for i being Element of NAT st 1 <= i & i <= len h holds ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) proofend; theorem Th13: :: JORDAN5D:13 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) proofend; theorem Th14: :: JORDAN5D:14 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) proofend; theorem Th15: :: JORDAN5D:15 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) proofend; theorem Th16: :: JORDAN5D:16 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) proofend; theorem Th17: :: JORDAN5D:17 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) proofend; theorem Th18: :: JORDAN5D:18 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) proofend; theorem :: JORDAN5D:19 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds lower_bound X = lower_bound (proj2 | (W-most (L~ h))) by Th13; theorem :: JORDAN5D:20 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds upper_bound X = upper_bound (proj2 | (W-most (L~ h))) by Th13; theorem :: JORDAN5D:21 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds lower_bound X = lower_bound (proj2 | (E-most (L~ h))) by Th14; theorem :: JORDAN5D:22 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds upper_bound X = upper_bound (proj2 | (E-most (L~ h))) by Th14; theorem :: JORDAN5D:23 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds lower_bound X = lower_bound (proj1 | (L~ g)) by Th17; theorem :: JORDAN5D:24 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds lower_bound X = lower_bound (proj1 | (S-most (L~ h))) by Th16; theorem :: JORDAN5D:25 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds upper_bound X = upper_bound (proj1 | (S-most (L~ h))) by Th16; theorem :: JORDAN5D:26 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds lower_bound X = lower_bound (proj1 | (N-most (L~ h))) by Th15; theorem :: JORDAN5D:27 for h being non constant standard special_circular_sequence for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds upper_bound X = upper_bound (proj1 | (N-most (L~ h))) by Th15; theorem :: JORDAN5D:28 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds lower_bound X = lower_bound (proj2 | (L~ g)) by Th18; theorem :: JORDAN5D:29 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds upper_bound X = upper_bound (proj1 | (L~ g)) by Th17; theorem :: JORDAN5D:30 for g being FinSequence of (TOP-REAL 2) for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds upper_bound X = upper_bound (proj2 | (L~ g)) by Th18; theorem Th31: :: JORDAN5D:31 for p being Point of (TOP-REAL 2) for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds ((GoB h) * (1,I)) `1 <= p `1 proofend; theorem Th32: :: JORDAN5D:32 for p being Point of (TOP-REAL 2) for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 proofend; theorem Th33: :: JORDAN5D:33 for p being Point of (TOP-REAL 2) for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds ((GoB h) * (I,1)) `2 <= p `2 proofend; theorem Th34: :: JORDAN5D:34 for p being Point of (TOP-REAL 2) for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 proofend; theorem Th35: :: JORDAN5D:35 for h being non constant standard special_circular_sequence for i, j being Element of NAT st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds ex q being Point of (TOP-REAL 2) st ( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h ) proofend; theorem Th36: :: JORDAN5D:36 for h being non constant standard special_circular_sequence for i, j being Element of NAT st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds ex q being Point of (TOP-REAL 2) st ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) proofend; theorem Th37: :: JORDAN5D:37 for h being non constant standard special_circular_sequence holds W-bound (L~ h) = ((GoB h) * (1,1)) `1 proofend; theorem Th38: :: JORDAN5D:38 for h being non constant standard special_circular_sequence holds S-bound (L~ h) = ((GoB h) * (1,1)) `2 proofend; theorem Th39: :: JORDAN5D:39 for h being non constant standard special_circular_sequence holds E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1 proofend; theorem Th40: :: JORDAN5D:40 for h being non constant standard special_circular_sequence holds N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2 proofend; theorem Th41: :: JORDAN5D:41 for f being non empty FinSequence of (TOP-REAL 2) for i, I, i1 being Element of NAT for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = min Y holds ((GoB f) * (I,i1)) `2 <= (f /. i) `2 proofend; theorem Th42: :: JORDAN5D:42 for h being non constant standard special_circular_sequence for i, I, i1 being Element of NAT for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y holds ((GoB h) * (i1,I)) `1 <= (h /. i) `1 proofend; theorem Th43: :: JORDAN5D:43 for h being non constant standard special_circular_sequence for i, I, i1 being Element of NAT for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y holds ((GoB h) * (i1,I)) `1 >= (h /. i) `1 proofend; theorem Th44: :: JORDAN5D:44 for f being non empty FinSequence of (TOP-REAL 2) for i, I, i1 being Element of NAT for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = max Y holds ((GoB f) * (I,i1)) `2 >= (f /. i) `2 proofend; Lm1: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds ((GoB h) * (1,i1)) `2 <= p `2 proofend; Lm2: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds ((GoB h) * (1,i1)) `2 >= p `2 proofend; Lm3: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y holds ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 proofend; Lm4: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 proofend; Lm5: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds ((GoB h) * (i1,1)) `1 <= p `1 proofend; Lm6: for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT for h being non constant standard special_circular_sequence st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y holds ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 proofend; Lm7: for h being non constant standard special_circular_sequence for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds ((GoB h) * (i1,1)) `1 >= p `1 proofend; Lm8: for h being non constant standard special_circular_sequence for i1 being Element of NAT for p being Point of (TOP-REAL 2) for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 proofend; Lm9: for h being non constant standard special_circular_sequence holds len h >= 2 by GOBOARD7:34, XXREAL_0:2; begin definition let g be non constant standard special_circular_sequence; func i_s_w g -> Element of NAT means :Def1: :: JORDAN5D:def 1 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-min (L~ g) ); existence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-min (L~ g) holds b1 = b2 by GOBOARD1:5; func i_n_w g -> Element of NAT means :Def2: :: JORDAN5D:def 2 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-max (L~ g) ); existence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-max (L~ g) holds b1 = b2 by GOBOARD1:5; func i_s_e g -> Element of NAT means :Def3: :: JORDAN5D:def 3 ( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-min (L~ g) ); existence ex b1 being Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-min (L~ g) holds b1 = b2 by GOBOARD1:5; func i_n_e g -> Element of NAT means :Def4: :: JORDAN5D:def 4 ( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-max (L~ g) ); existence ex b1 being Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-max (L~ g) holds b1 = b2 by GOBOARD1:5; func i_w_s g -> Element of NAT means :Def5: :: JORDAN5D:def 5 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-min (L~ g) ); existence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) holds b1 = b2 by GOBOARD1:5; func i_e_s g -> Element of NAT means :Def6: :: JORDAN5D:def 6 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-max (L~ g) ); existence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-max (L~ g) holds b1 = b2 by GOBOARD1:5; func i_w_n g -> Element of NAT means :Def7: :: JORDAN5D:def 7 ( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-min (L~ g) ); existence ex b1 being Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-min (L~ g) holds b1 = b2 by GOBOARD1:5; func i_e_n g -> Element of NAT means :Def8: :: JORDAN5D:def 8 ( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-max (L~ g) ); existence ex b1 being Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-max (L~ g) holds b1 = b2 by GOBOARD1:5; end; :: deftheorem Def1 defines i_s_w JORDAN5D:def_1_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_s_w g iff ( [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-min (L~ g) ) ); :: deftheorem Def2 defines i_n_w JORDAN5D:def_2_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_n_w g iff ( [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-max (L~ g) ) ); :: deftheorem Def3 defines i_s_e JORDAN5D:def_3_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_s_e g iff ( [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-min (L~ g) ) ); :: deftheorem Def4 defines i_n_e JORDAN5D:def_4_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_n_e g iff ( [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-max (L~ g) ) ); :: deftheorem Def5 defines i_w_s JORDAN5D:def_5_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_w_s g iff ( [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) ) ); :: deftheorem Def6 defines i_e_s JORDAN5D:def_6_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_e_s g iff ( [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-max (L~ g) ) ); :: deftheorem Def7 defines i_w_n JORDAN5D:def_7_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_w_n g iff ( [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-min (L~ g) ) ); :: deftheorem Def8 defines i_e_n JORDAN5D:def_8_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = i_e_n g iff ( [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-max (L~ g) ) ); theorem :: JORDAN5D:45 for h being non constant standard special_circular_sequence holds ( 1 <= i_w_n h & i_w_n h <= len (GoB h) & 1 <= i_e_n h & i_e_n h <= len (GoB h) & 1 <= i_w_s h & i_w_s h <= len (GoB h) & 1 <= i_e_s h & i_e_s h <= len (GoB h) ) proofend; theorem :: JORDAN5D:46 for h being non constant standard special_circular_sequence holds ( 1 <= i_n_e h & i_n_e h <= width (GoB h) & 1 <= i_s_e h & i_s_e h <= width (GoB h) & 1 <= i_n_w h & i_n_w h <= width (GoB h) & 1 <= i_s_w h & i_s_w h <= width (GoB h) ) proofend; Lm10: for h being non constant standard special_circular_sequence for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds i1 = i2 proofend; definition let g be non constant standard special_circular_sequence; func n_s_w g -> Element of NAT means :Def9: :: JORDAN5D:def 9 ( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = W-min (L~ g) holds b1 = b2 by Lm10; func n_n_w g -> Element of NAT means :Def10: :: JORDAN5D:def 10 ( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = W-max (L~ g) holds b1 = b2 by Lm10; func n_s_e g -> Element of NAT means :Def11: :: JORDAN5D:def 11 ( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = E-min (L~ g) holds b1 = b2 by Lm10; func n_n_e g -> Element of NAT means :Def12: :: JORDAN5D:def 12 ( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = E-max (L~ g) holds b1 = b2 by Lm10; func n_w_s g -> Element of NAT means :Def13: :: JORDAN5D:def 13 ( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = S-min (L~ g) holds b1 = b2 by Lm10; func n_e_s g -> Element of NAT means :Def14: :: JORDAN5D:def 14 ( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = S-max (L~ g) holds b1 = b2 by Lm10; func n_w_n g -> Element of NAT means :Def15: :: JORDAN5D:def 15 ( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = N-min (L~ g) holds b1 = b2 by Lm10; func n_e_n g -> Element of NAT means :Def16: :: JORDAN5D:def 16 ( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) ) proofend; uniqueness for b1, b2 being Element of NAT st 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = N-max (L~ g) holds b1 = b2 by Lm10; end; :: deftheorem Def9 defines n_s_w JORDAN5D:def_9_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_s_w g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = W-min (L~ g) ) ); :: deftheorem Def10 defines n_n_w JORDAN5D:def_10_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_n_w g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = W-max (L~ g) ) ); :: deftheorem Def11 defines n_s_e JORDAN5D:def_11_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_s_e g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = E-min (L~ g) ) ); :: deftheorem Def12 defines n_n_e JORDAN5D:def_12_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_n_e g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = E-max (L~ g) ) ); :: deftheorem Def13 defines n_w_s JORDAN5D:def_13_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_w_s g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = S-min (L~ g) ) ); :: deftheorem Def14 defines n_e_s JORDAN5D:def_14_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_e_s g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = S-max (L~ g) ) ); :: deftheorem Def15 defines n_w_n JORDAN5D:def_15_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_w_n g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = N-min (L~ g) ) ); :: deftheorem Def16 defines n_e_n JORDAN5D:def_16_:_ for g being non constant standard special_circular_sequence for b2 being Element of NAT holds ( b2 = n_e_n g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = N-max (L~ g) ) ); theorem :: JORDAN5D:47 for h being non constant standard special_circular_sequence holds n_w_n h <> n_w_s h proofend; theorem :: JORDAN5D:48 for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h proofend; theorem :: JORDAN5D:49 for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h proofend; theorem :: JORDAN5D:50 for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h proofend;