:: JORDAN5D semantic presentation
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))
proof
let n be Element of NAT ; ::_thesis: for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg (h,((len h) -' 1))
let h be FinSequence of (TOP-REAL n); ::_thesis: ( len h >= 2 implies h /. (len h) in LSeg (h,((len h) -' 1)) )
set i = len h;
assume A1: len h >= 2 ; ::_thesis: h /. (len h) in LSeg (h,((len h) -' 1))
then A2: 2 - 1 <= (len h) - 1 by XREAL_1:9;
((len h) -' 1) + 1 = len h by A1, XREAL_1:235, XXREAL_0:2;
hence h /. (len h) in LSeg (h,((len h) -' 1)) by A2, TOPREAL1:21; ::_thesis: verum
end;
theorem Th2: :: JORDAN5D:2
for i being Element of NAT st 3 <= i holds
i mod (i -' 1) = 1
proof
let i be Element of NAT ; ::_thesis: ( 3 <= i implies i mod (i -' 1) = 1 )
assume A1: 3 <= i ; ::_thesis: i mod (i -' 1) = 1
then A2: i -' 1 = i - 1 by XREAL_1:233, XXREAL_0:2;
3 -' 1 = (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then 2 <= i -' 1 by A1, NAT_D:42;
then 1 < i - 1 by A2, XXREAL_0:2;
then 1 + i < (i - 1) + i by XREAL_1:8;
then (1 + i) - 1 < ((i - 1) + i) - 1 by XREAL_1:14;
then A3: i < (i - 1) + (i - 1) ;
i -' 1 <= i by NAT_D:35;
hence i mod (i -' 1) = i - (i - 1) by A2, A3, JORDAN4:2
.= 1 ;
::_thesis: verum
end;
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 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 )
let h be non constant standard special_circular_sequence; ::_thesis: ( p in rng h implies ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p ) )
A1: 4 < len h by GOBOARD7:34;
A2: 1 < len h by GOBOARD7:34, XXREAL_0:2;
assume p in rng h ; ::_thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )
then consider x being set such that
A3: x in dom h and
A4: p = h . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A3;
A5: 1 <= i by A3, FINSEQ_3:25;
set j = S_Drop (i,h);
A6: i <= len h by A3, FINSEQ_3:25;
( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )
proof
A7: i <= ((len h) -' 1) + 1 by A5, A6, XREAL_1:235, XXREAL_0:2;
percases ( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 ) by A7, NAT_1:8;
supposeA8: i <= (len h) -' 1 ; ::_thesis: ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )
then S_Drop (i,h) = i by A5, JORDAN4:22;
then (S_Drop (i,h)) + 1 <= ((len h) -' 1) + 1 by A8, XREAL_1:7;
hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by A4, A5, A2, A8, JORDAN4:22, XREAL_1:235; ::_thesis: verum
end;
supposeA9: i = ((len h) -' 1) + 1 ; ::_thesis: ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )
then i = len h by A1, XREAL_1:235, XXREAL_0:2;
then i mod ((len h) -' 1) = 1 by A1, Th2, XXREAL_0:2;
then A10: S_Drop (i,h) = 1 by JORDAN4:def_1;
A11: 1 <= len h by GOBOARD7:34, XXREAL_0:2;
then A12: len h in dom h by FINSEQ_3:25;
1 in dom h by A11, FINSEQ_3:25;
then h . 1 = h /. 1 by PARTFUN1:def_6
.= h /. (len h) by FINSEQ_6:def_1
.= h . (len h) by A12, PARTFUN1:def_6 ;
hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by A4, A1, A9, A10, XREAL_1:235, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p ) ; ::_thesis: verum
end;
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)) )
proof
let r be Real; ::_thesis: for g being FinSequence of REAL st r in rng g holds
( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )
let g be FinSequence of REAL ; ::_thesis: ( r in rng g implies ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) )
assume r in rng g ; ::_thesis: ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )
then r in rng (Incr g) by SEQ_4:def_21;
then consider x being set such that
A1: x in dom (Incr g) and
A2: (Incr g) . x = r by FUNCT_1:def_3;
reconsider j = x as Element of NAT by A1;
A3: x in Seg (len (Incr g)) by A1, FINSEQ_1:def_3;
then A4: j <= len (Incr g) by FINSEQ_1:1;
A5: 1 <= j by A3, FINSEQ_1:1;
then A6: 1 <= len (Incr g) by A4, XXREAL_0:2;
then 1 in dom (Incr g) by FINSEQ_3:25;
hence (Incr g) . 1 <= r by A1, A2, A5, SEQ_4:137; ::_thesis: r <= (Incr g) . (len (Incr g))
len (Incr g) in dom (Incr g) by A6, FINSEQ_3:25;
hence r <= (Incr g) . (len (Incr g)) by A1, A2, A4, SEQ_4:137; ::_thesis: verum
end;
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 )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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 )
let i, I be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) implies ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) )
assume that
A1: 1 <= i and
A2: i <= len h and
A3: 1 <= I and
A4: I <= width (GoB h) ; ::_thesis: ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )
A5: I <= width (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def_2;
i <= len (X_axis h) by A2, GOBOARD1:def_1;
then A6: i in dom (X_axis h) by A1, FINSEQ_3:25;
then (X_axis h) . i = (h /. i) `1 by GOBOARD1:def_1;
then A7: (h /. i) `1 in rng (X_axis h) by A6, FUNCT_1:def_3;
A8: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def_2;
then 1 <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:32;
then A9: [1,I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, MATRIX_1:36;
A10: 1 <= len (GoB h) by GOBOARD7:32;
len (GoB h) <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD2:def_2;
then A11: [(len (GoB h)),I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, A10, MATRIX_1:36;
(GoB h) * ((len (GoB h)),I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * ((len (GoB h)),I) by GOBOARD2:def_2
.= |[((Incr (X_axis h)) . (len (GoB h))),((Incr (Y_axis h)) . I)]| by A11, GOBOARD2:def_1 ;
then A12: ((GoB h) * ((len (GoB h)),I)) `1 = (Incr (X_axis h)) . (len (GoB h)) by EUCLID:52;
(GoB h) * (1,I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (1,I) by GOBOARD2:def_2
.= |[((Incr (X_axis h)) . 1),((Incr (Y_axis h)) . I)]| by A9, GOBOARD2:def_1 ;
then A13: ((GoB h) * (1,I)) `1 = (Incr (X_axis h)) . 1 by EUCLID:52;
len (GoB h) = len (Incr (X_axis h)) by A8, GOBOARD2:def_1;
hence ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) by A12, A13, A7, Th4; ::_thesis: verum
end;
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 )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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 )
let i, I be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) implies ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) )
assume that
A1: 1 <= i and
A2: i <= len h and
A3: 1 <= I and
A4: I <= len (GoB h) ; ::_thesis: ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 )
A5: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def_2;
then A6: 1 <= width (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:33;
i <= len (Y_axis h) by A2, GOBOARD1:def_2;
then A7: i in dom (Y_axis h) by A1, FINSEQ_3:25;
then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def_2;
then A8: (h /. i) `2 in rng (Y_axis h) by A7, FUNCT_1:def_3;
1 <= width (GoB h) by GOBOARD7:33;
then A9: [I,(width (GoB h))] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A4, A5, MATRIX_1:36;
(GoB h) * (I,(width (GoB h))) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,(width (GoB h))) by GOBOARD2:def_2
.= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . (width (GoB h)))]| by A9, GOBOARD2:def_1 ;
then A10: ((GoB h) * (I,(width (GoB h)))) `2 = (Incr (Y_axis h)) . (width (GoB h)) by EUCLID:52;
I <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def_2;
then A11: [I,1] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A6, MATRIX_1:36;
(GoB h) * (I,1) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,1) by GOBOARD2:def_2
.= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . 1)]| by A11, GOBOARD2:def_1 ;
then A12: ((GoB h) * (I,1)) `2 = (Incr (Y_axis h)) . 1 by EUCLID:52;
width (GoB h) = len (Incr (Y_axis h)) by A5, GOBOARD2:def_1;
hence ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) by A10, A12, A8, Th4; ::_thesis: verum
end;
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) )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) implies ex k, j being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )
assume that
A1: 1 <= i and
A2: i <= len (GoB f) ; ::_thesis: ex k, j being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
A3: i in dom (GoB f) by A1, A2, FINSEQ_3:25;
A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2;
then len (Incr (X_axis f)) = len (GoB f) by GOBOARD2:def_1;
then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25;
then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def_3;
then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def_21;
then consider k being Nat such that
A5: k in dom (X_axis f) and
A6: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;
A7: len (X_axis f) = len f by GOBOARD1:def_1
.= len (Y_axis f) by GOBOARD1:def_2 ;
then dom (X_axis f) = dom (Y_axis f) by FINSEQ_3:29;
then (Y_axis f) . k in rng (Y_axis f) by A5, FUNCT_1:def_3;
then (Y_axis f) . k in rng (Incr (Y_axis f)) by SEQ_4:def_21;
then consider j being Nat such that
A8: j in dom (Incr (Y_axis f)) and
A9: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;
reconsider k = k, j = j as Element of NAT by ORDINAL1:def_12;
A10: (X_axis f) . k = (f /. k) `1 by A5, GOBOARD1:def_1;
take k ; ::_thesis: ex j being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take j ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
len (X_axis f) = len f by GOBOARD1:def_1;
hence k in dom f by A5, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
j in Seg (len (Incr (Y_axis f))) by A8, FINSEQ_1:def_3;
then j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A4, A3, ZFMISC_1:87;
hence A11: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. k = (GoB f) * (i,j)
dom (X_axis f) = dom (Y_axis f) by A7, FINSEQ_3:29;
then (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def_2;
hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53
.= (GoB f) * (i,j) by A4, A11, GOBOARD2:def_1 ;
::_thesis: verum
end;
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) )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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) )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= width (GoB f) implies ex k, i being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )
assume that
A1: 1 <= j and
A2: j <= width (GoB f) ; ::_thesis: ex k, i being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
A3: j in Seg (width (GoB f)) by A1, A2, FINSEQ_1:1;
A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2;
then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1;
then j in dom (Incr (Y_axis f)) by A1, A2, FINSEQ_3:25;
then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def_3;
then (Incr (Y_axis f)) . j in rng (Y_axis f) by SEQ_4:def_21;
then consider k being Nat such that
A5: k in dom (Y_axis f) and
A6: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;
A7: len (X_axis f) = len f by GOBOARD1:def_1
.= len (Y_axis f) by GOBOARD1:def_2 ;
then k in dom (X_axis f) by A5, FINSEQ_3:29;
then (X_axis f) . k in rng (X_axis f) by FUNCT_1:def_3;
then (X_axis f) . k in rng (Incr (X_axis f)) by SEQ_4:def_21;
then consider i being Nat such that
A8: i in dom (Incr (X_axis f)) and
A9: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;
reconsider k = k, i = i as Element of NAT by ORDINAL1:def_12;
k in dom (X_axis f) by A5, A7, FINSEQ_3:29;
then A10: (X_axis f) . k = (f /. k) `1 by GOBOARD1:def_1;
take k ; ::_thesis: ex i being Element of NAT st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
take i ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
len (Y_axis f) = len f by GOBOARD1:def_2;
hence k in dom f by A5, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
len (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) = len (Incr (X_axis f)) by GOBOARD2:def_1;
then i in dom (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A8, FINSEQ_3:29;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A4, A3, ZFMISC_1:87;
hence A11: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. k = (GoB f) * (i,j)
(Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def_2;
hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53
.= (GoB f) * (i,j) by A4, A11, GOBOARD2:def_1 ;
::_thesis: verum
end;
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 )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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 )
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies 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 ) )
assume that
A1: 1 <= i and
A2: i <= len (GoB f) and
A3: 1 <= j and
A4: j <= width (GoB f) ; ::_thesis: 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 )
A5: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2;
then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1;
then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;
then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def_3;
then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1;
len (Incr (X_axis f)) = len (GoB f) by A5, GOBOARD2:def_1;
then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25;
then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def_3;
then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def_21;
then consider k being Nat such that
A7: k in dom (X_axis f) and
A8: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 )
len (X_axis f) = len f by GOBOARD1:def_1;
hence k in dom f by A7, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 )
i in dom (GoB f) by A1, A2, FINSEQ_3:25;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87;
hence [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: (f /. k) `1 = ((GoB f) * (i,j)) `1
then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def_1;
thus (f /. k) `1 = (Incr (X_axis f)) . i by A7, A8, GOBOARD1:def_1
.= ((GoB f) * (i,j)) `1 by A9, EUCLID:52 ; ::_thesis: verum
end;
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 )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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 )
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies 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 ) )
assume that
A1: 1 <= i and
A2: i <= len (GoB f) and
A3: 1 <= j and
A4: j <= width (GoB f) ; ::_thesis: 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 )
A5: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2;
then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1;
then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;
then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def_3;
then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1;
len (Incr (Y_axis f)) = width (GoB f) by A5, GOBOARD2:def_1;
then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;
then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def_3;
then (Incr (Y_axis f)) . j in rng (Y_axis f) by SEQ_4:def_21;
then consider k being Nat such that
A7: k in dom (Y_axis f) and
A8: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
len (Y_axis f) = len f by GOBOARD1:def_2;
hence k in dom f by A7, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
i in dom (GoB f) by A1, A2, FINSEQ_3:25;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87;
hence [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: (f /. k) `2 = ((GoB f) * (i,j)) `2
then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def_1;
thus (f /. k) `2 = (Incr (Y_axis f)) . j by A7, A8, GOBOARD1:def_2
.= ((GoB f) * (i,j)) `2 by A9, EUCLID:52 ; ::_thesis: verum
end;
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) )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h implies ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) )
A1: len h > 4 by GOBOARD7:34;
assume that
A2: 1 <= i and
A3: i <= len h ; ::_thesis: ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )
i in dom h by A2, A3, FINSEQ_3:25;
then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2;
hence ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) by PSCOMP_1:24; ::_thesis: verum
end;
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) )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h implies ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) )
A1: len h > 4 by GOBOARD7:34;
assume that
A2: 1 <= i and
A3: i <= len h ; ::_thesis: ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )
i in dom h by A2, A3, FINSEQ_3:25;
then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2;
hence ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) by PSCOMP_1:24; ::_thesis: verum
end;
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)))
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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)))
set T = (TOP-REAL 2) | (W-most (L~ h));
set F = proj2 | (W-most (L~ h));
let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) )
assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))
thus X c= (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) )
A2: dom (proj2 | (W-most (L~ h))) = the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (W-most (L~ h)))
.= W-most (L~ h) by PRE_TOPC:def_5 ;
assume x in X ; ::_thesis: x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))
then consider q1 being Point of (TOP-REAL 2) such that
A3: q1 `2 = x and
A4: q1 `1 = W-bound (L~ h) and
A5: q1 in L~ h by A1;
A6: x = (proj2 | (W-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:12;
A7: q1 in W-most (L~ h) by A4, A5, SPRECT_2:12;
then q1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, FUNCT_2:def_1;
hence x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) or x in X )
A8: W-most (L~ h) c= L~ h by XBOOLE_1:17;
assume x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj2 | (W-most (L~ h))) and
A9: x1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) and
A10: x = (proj2 | (W-most (L~ h))) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (W-most (L~ h))) by A9;
then A11: x1 in W-most (L~ h) by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
A12: x2 `1 = (W-min (L~ h)) `1 by A11, PSCOMP_1:31
.= W-bound (L~ h) by EUCLID:52 ;
x = x2 `2 by A10, A11, PSCOMP_1:23;
hence x in X by A1, A11, A12, A8; ::_thesis: verum
end;
end;
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)))
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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)))
set T = (TOP-REAL 2) | (E-most (L~ h));
set F = proj2 | (E-most (L~ h));
let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) )
assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h)))
thus X c= (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) )
A2: dom (proj2 | (E-most (L~ h))) = the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (E-most (L~ h)))
.= E-most (L~ h) by PRE_TOPC:def_5 ;
assume x in X ; ::_thesis: x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h)))
then consider q1 being Point of (TOP-REAL 2) such that
A3: q1 `2 = x and
A4: q1 `1 = E-bound (L~ h) and
A5: q1 in L~ h by A1;
A6: x = (proj2 | (E-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:13;
A7: q1 in E-most (L~ h) by A4, A5, SPRECT_2:13;
then q1 in the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by A2, FUNCT_2:def_1;
hence x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) or x in X )
A8: E-most (L~ h) c= L~ h by XBOOLE_1:17;
assume x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj2 | (E-most (L~ h))) and
A9: x1 in the carrier of ((TOP-REAL 2) | (E-most (L~ h))) and
A10: x = (proj2 | (E-most (L~ h))) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (E-most (L~ h))) by A9;
then A11: x1 in E-most (L~ h) by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
A12: x2 `1 = (E-min (L~ h)) `1 by A11, PSCOMP_1:47
.= E-bound (L~ h) by EUCLID:52 ;
x = x2 `2 by A10, A11, PSCOMP_1:23;
hence x in X by A1, A11, A12, A8; ::_thesis: verum
end;
end;
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)))
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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)))
set T = (TOP-REAL 2) | (N-most (L~ h));
set F = proj1 | (N-most (L~ h));
let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } implies X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) )
assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
thus X c= (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) )
A2: dom (proj1 | (N-most (L~ h))) = the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (N-most (L~ h)))
.= N-most (L~ h) by PRE_TOPC:def_5 ;
assume x in X ; ::_thesis: x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
then consider q1 being Point of (TOP-REAL 2) such that
A3: q1 `1 = x and
A4: q1 `2 = N-bound (L~ h) and
A5: q1 in L~ h by A1;
A6: x = (proj1 | (N-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:22, SPRECT_2:10;
A7: q1 in N-most (L~ h) by A4, A5, SPRECT_2:10;
then q1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by A2, FUNCT_2:def_1;
hence x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) or x in X )
A8: N-most (L~ h) c= L~ h by XBOOLE_1:17;
assume x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj1 | (N-most (L~ h))) and
A9: x1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) and
A10: x = (proj1 | (N-most (L~ h))) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (N-most (L~ h))) by A9;
then A11: x1 in N-most (L~ h) by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
A12: x2 `2 = (N-min (L~ h)) `2 by A11, PSCOMP_1:39
.= N-bound (L~ h) by EUCLID:52 ;
x = x2 `1 by A10, A11, PSCOMP_1:22;
hence x in X by A1, A11, A12, A8; ::_thesis: verum
end;
end;
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)))
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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)))
set T = (TOP-REAL 2) | (S-most (L~ h));
set F = proj1 | (S-most (L~ h));
let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } implies X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) )
assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h)))
thus X c= (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) )
A2: dom (proj1 | (S-most (L~ h))) = the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (S-most (L~ h)))
.= S-most (L~ h) by PRE_TOPC:def_5 ;
assume x in X ; ::_thesis: x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h)))
then consider q1 being Point of (TOP-REAL 2) such that
A3: q1 `1 = x and
A4: q1 `2 = S-bound (L~ h) and
A5: q1 in L~ h by A1;
A6: x = (proj1 | (S-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:22, SPRECT_2:11;
A7: q1 in S-most (L~ h) by A4, A5, SPRECT_2:11;
then q1 in the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by A2, FUNCT_2:def_1;
hence x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) or x in X )
A8: S-most (L~ h) c= L~ h by XBOOLE_1:17;
assume x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj1 | (S-most (L~ h))) and
A9: x1 in the carrier of ((TOP-REAL 2) | (S-most (L~ h))) and
A10: x = (proj1 | (S-most (L~ h))) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (S-most (L~ h))) by A9;
then A11: x1 in S-most (L~ h) by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
A12: x2 `2 = (S-min (L~ h)) `2 by A11, PSCOMP_1:55
.= S-bound (L~ h) by EUCLID:52 ;
x = x2 `1 by A10, A11, PSCOMP_1:22;
hence x in X by A1, A11, A12, A8; ::_thesis: verum
end;
end;
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))
proof
let g be FinSequence of (TOP-REAL 2); ::_thesis: 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))
set T = (TOP-REAL 2) | (L~ g);
set F = proj1 | (L~ g);
let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } ; ::_thesis: X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
thus X c= (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume x in X ; ::_thesis: x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
then consider q1 being Point of (TOP-REAL 2) such that
A2: q1 `1 = x and
A3: q1 in L~ g by A1;
A4: x = (proj1 | (L~ g)) . q1 by A2, A3, PSCOMP_1:22;
A5: dom (proj1 | (L~ g)) = the carrier of ((TOP-REAL 2) | (L~ g)) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (L~ g))
.= L~ g by PRE_TOPC:def_5 ;
then q1 in the carrier of ((TOP-REAL 2) | (L~ g)) by A3, FUNCT_2:def_1;
hence x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X )
assume x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj1 | (L~ g)) and
A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and
A7: x = (proj1 | (L~ g)) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (L~ g)) by A6;
then A8: x1 in L~ g by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
x = x2 `1 by A7, A8, PSCOMP_1:22;
hence x in X by A1, A8; ::_thesis: verum
end;
end;
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))
proof
let g be FinSequence of (TOP-REAL 2); ::_thesis: 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))
set T = (TOP-REAL 2) | (L~ g);
set F = proj2 | (L~ g);
let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } ; ::_thesis: X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
thus X c= (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume x in X ; ::_thesis: x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
then consider q1 being Point of (TOP-REAL 2) such that
A2: q1 `2 = x and
A3: q1 in L~ g by A1;
A4: x = (proj2 | (L~ g)) . q1 by A2, A3, PSCOMP_1:23;
A5: dom (proj2 | (L~ g)) = the carrier of ((TOP-REAL 2) | (L~ g)) by FUNCT_2:def_1
.= [#] ((TOP-REAL 2) | (L~ g))
.= L~ g by PRE_TOPC:def_5 ;
then q1 in the carrier of ((TOP-REAL 2) | (L~ g)) by A3, FUNCT_2:def_1;
hence x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def_6; ::_thesis: verum
end;
thus (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X )
assume x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; ::_thesis: x in X
then consider x1 being set such that
x1 in dom (proj2 | (L~ g)) and
A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and
A7: x = (proj2 | (L~ g)) . x1 by FUNCT_1:def_6;
x1 in [#] ((TOP-REAL 2) | (L~ g)) by A6;
then A8: x1 in L~ g by PRE_TOPC:def_5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
x = x2 `2 by A7, A8, PSCOMP_1:23;
hence x in X by A1, A8; ::_thesis: verum
end;
end;
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
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: 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
let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies ((GoB h) * (1,I)) `1 <= p `1 )
assume that
A1: p in L~ h and
A2: 1 <= I and
A3: I <= width (GoB h) ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1
consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len h and
A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then i <= len h by A5, XXREAL_0:2;
then A7: ((GoB h) * (1,I)) `1 <= (h /. i) `1 by A2, A3, A4, Th5;
1 <= i + 1 by NAT_1:11;
then A8: ((GoB h) * (1,I)) `1 <= (h /. (i + 1)) `1 by A2, A3, A5, Th5;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,I))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,I))_`1_<=_p_`1_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1
then (h /. i) `1 <= p `1 by A6, TOPREAL1:3;
hence ((GoB h) * (1,I)) `1 <= p `1 by A7, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1
then (h /. (i + 1)) `1 <= p `1 by A6, TOPREAL1:3;
hence ((GoB h) * (1,I)) `1 <= p `1 by A8, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,I)) `1 <= p `1 ; ::_thesis: verum
end;
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
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: 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
let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )
assume that
A1: p in L~ h and
A2: 1 <= I and
A3: I <= width (GoB h) ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1
consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len h and
A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then i <= len h by A5, XXREAL_0:2;
then A7: ((GoB h) * ((len (GoB h)),I)) `1 >= (h /. i) `1 by A2, A3, A4, Th5;
1 <= i + 1 by NAT_1:11;
then A8: ((GoB h) * ((len (GoB h)),I)) `1 >= (h /. (i + 1)) `1 by A2, A3, A5, Th5;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_p_`1_<=_((GoB_h)_*_((len_(GoB_h)),I))_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_p_`1_<=_((GoB_h)_*_((len_(GoB_h)),I))_`1_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1
then (h /. (i + 1)) `1 >= p `1 by A6, TOPREAL1:3;
hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 by A8, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1
then (h /. i) `1 >= p `1 by A6, TOPREAL1:3;
hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 by A7, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ; ::_thesis: verum
end;
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
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: 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
let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies ((GoB h) * (I,1)) `2 <= p `2 )
assume that
A1: p in L~ h and
A2: 1 <= I and
A3: I <= len (GoB h) ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2
consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len h and
A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then i <= len h by A5, XXREAL_0:2;
then A7: ((GoB h) * (I,1)) `2 <= (h /. i) `2 by A2, A3, A4, Th6;
1 <= i + 1 by NAT_1:11;
then A8: ((GoB h) * (I,1)) `2 <= (h /. (i + 1)) `2 by A2, A3, A5, Th6;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(I,1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(I,1))_`2_<=_p_`2_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2
then (h /. i) `2 <= p `2 by A6, TOPREAL1:4;
hence ((GoB h) * (I,1)) `2 <= p `2 by A7, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2
then (h /. (i + 1)) `2 <= p `2 by A6, TOPREAL1:4;
hence ((GoB h) * (I,1)) `2 <= p `2 by A8, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (I,1)) `2 <= p `2 ; ::_thesis: verum
end;
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
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: 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
let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 )
assume that
A1: p in L~ h and
A2: 1 <= I and
A3: I <= len (GoB h) ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2
consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len h and
A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then i <= len h by A5, XXREAL_0:2;
then A7: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. i) `2 by A2, A3, A4, Th6;
1 <= i + 1 by NAT_1:11;
then A8: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. (i + 1)) `2 by A2, A3, A5, Th6;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_p_`2_<=_((GoB_h)_*_(I,(width_(GoB_h))))_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_p_`2_<=_((GoB_h)_*_(I,(width_(GoB_h))))_`2_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2
then (h /. (i + 1)) `2 >= p `2 by A6, TOPREAL1:4;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by A8, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2
then (h /. i) `2 >= p `2 by A6, TOPREAL1:4;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by A7, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ; ::_thesis: verum
end;
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 )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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 )
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st
( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h ) )
assume that
A1: 1 <= i and
A2: i <= len (GoB h) and
A3: 1 <= j and
A4: j <= width (GoB h) ; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h )
consider k being Element of NAT such that
A5: k in dom h and
[i,j] in Indices (GoB h) and
A6: (h /. k) `1 = ((GoB h) * (i,j)) `1 by A1, A2, A3, A4, Th9;
take q = h /. k; ::_thesis: ( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h )
thus q `1 = ((GoB h) * (i,j)) `1 by A6; ::_thesis: q in L~ h
4 < len h by GOBOARD7:34;
hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; ::_thesis: verum
end;
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 )
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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 )
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st
( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) )
assume that
A1: 1 <= i and
A2: i <= len (GoB h) and
A3: 1 <= j and
A4: j <= width (GoB h) ; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )
consider k being Element of NAT such that
A5: k in dom h and
[i,j] in Indices (GoB h) and
A6: (h /. k) `2 = ((GoB h) * (i,j)) `2 by A1, A2, A3, A4, Th10;
take q = h /. k; ::_thesis: ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )
thus q `2 = ((GoB h) * (i,j)) `2 by A6; ::_thesis: q in L~ h
4 < len h by GOBOARD7:34;
hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; ::_thesis: verum
end;
theorem Th37: :: JORDAN5D:37
for h being non constant standard special_circular_sequence holds W-bound (L~ h) = ((GoB h) * (1,1)) `1
proof
let h be non constant standard special_circular_sequence; ::_thesis: W-bound (L~ h) = ((GoB h) * (1,1)) `1
set X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ;
set A = ((GoB h) * (1,1)) `1 ;
consider a being set such that
A1: a in L~ h by XBOOLE_0:def_1;
A2: { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL )
assume b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL
then ex qq being Point of (TOP-REAL 2) st
( b = qq `1 & qq in L~ h ) ;
hence b in REAL ; ::_thesis: verum
end;
reconsider a = a as Point of (TOP-REAL 2) by A1;
a `1 in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;
then reconsider X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;
lower_bound X = ((GoB h) * (1,1)) `1
proof
A3: 1 <= width (GoB h) by GOBOARD7:33;
A4: for p being real number st p in X holds
p >= ((GoB h) * (1,1)) `1
proof
let p be real number ; ::_thesis: ( p in X implies p >= ((GoB h) * (1,1)) `1 )
assume p in X ; ::_thesis: p >= ((GoB h) * (1,1)) `1
then ex s being Point of (TOP-REAL 2) st
( p = s `1 & s in L~ h ) ;
hence p >= ((GoB h) * (1,1)) `1 by A3, Th31; ::_thesis: verum
end;
1 <= len (GoB h) by GOBOARD7:32;
then consider q1 being Point of (TOP-REAL 2) such that
A5: q1 `1 = ((GoB h) * (1,1)) `1 and
A6: q1 in L~ h by A3, Th35;
reconsider q11 = q1 `1 as Real ;
for q being real number st ( for p being real number st p in X holds
p >= q ) holds
((GoB h) * (1,1)) `1 >= q
proof
A7: q11 in X by A6;
let q be real number ; ::_thesis: ( ( for p being real number st p in X holds
p >= q ) implies ((GoB h) * (1,1)) `1 >= q )
assume for p being real number st p in X holds
p >= q ; ::_thesis: ((GoB h) * (1,1)) `1 >= q
hence ((GoB h) * (1,1)) `1 >= q by A5, A7; ::_thesis: verum
end;
hence lower_bound X = ((GoB h) * (1,1)) `1 by A4, SEQ_4:44; ::_thesis: verum
end;
hence W-bound (L~ h) = ((GoB h) * (1,1)) `1 by Th17; ::_thesis: verum
end;
theorem Th38: :: JORDAN5D:38
for h being non constant standard special_circular_sequence holds S-bound (L~ h) = ((GoB h) * (1,1)) `2
proof
let h be non constant standard special_circular_sequence; ::_thesis: S-bound (L~ h) = ((GoB h) * (1,1)) `2
set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ;
set A = ((GoB h) * (1,1)) `2 ;
consider a being set such that
A1: a in L~ h by XBOOLE_0:def_1;
A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL )
assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL
then ex qq being Point of (TOP-REAL 2) st
( b = qq `2 & qq in L~ h ) ;
hence b in REAL ; ::_thesis: verum
end;
reconsider a = a as Point of (TOP-REAL 2) by A1;
a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;
then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;
lower_bound X = ((GoB h) * (1,1)) `2
proof
A3: 1 <= len (GoB h) by GOBOARD7:32;
A4: for p being real number st p in X holds
p >= ((GoB h) * (1,1)) `2
proof
let p be real number ; ::_thesis: ( p in X implies p >= ((GoB h) * (1,1)) `2 )
assume p in X ; ::_thesis: p >= ((GoB h) * (1,1)) `2
then ex s being Point of (TOP-REAL 2) st
( p = s `2 & s in L~ h ) ;
hence p >= ((GoB h) * (1,1)) `2 by A3, Th33; ::_thesis: verum
end;
1 <= width (GoB h) by GOBOARD7:33;
then consider q1 being Point of (TOP-REAL 2) such that
A5: q1 `2 = ((GoB h) * (1,1)) `2 and
A6: q1 in L~ h by A3, Th36;
reconsider q11 = q1 `2 as Real ;
for q being real number st ( for p being real number st p in X holds
p >= q ) holds
((GoB h) * (1,1)) `2 >= q
proof
A7: q11 in X by A6;
let q be real number ; ::_thesis: ( ( for p being real number st p in X holds
p >= q ) implies ((GoB h) * (1,1)) `2 >= q )
assume for p being real number st p in X holds
p >= q ; ::_thesis: ((GoB h) * (1,1)) `2 >= q
hence ((GoB h) * (1,1)) `2 >= q by A5, A7; ::_thesis: verum
end;
hence lower_bound X = ((GoB h) * (1,1)) `2 by A4, SEQ_4:44; ::_thesis: verum
end;
hence S-bound (L~ h) = ((GoB h) * (1,1)) `2 by Th18; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1
set X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ;
set A = ((GoB h) * ((len (GoB h)),1)) `1 ;
consider a being set such that
A1: a in L~ h by XBOOLE_0:def_1;
A2: { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL )
assume b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL
then ex qq being Point of (TOP-REAL 2) st
( b = qq `1 & qq in L~ h ) ;
hence b in REAL ; ::_thesis: verum
end;
reconsider a = a as Point of (TOP-REAL 2) by A1;
a `1 in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;
then reconsider X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;
upper_bound X = ((GoB h) * ((len (GoB h)),1)) `1
proof
A3: for p being real number st p in X holds
p <= ((GoB h) * ((len (GoB h)),1)) `1
proof
let p be real number ; ::_thesis: ( p in X implies p <= ((GoB h) * ((len (GoB h)),1)) `1 )
assume p in X ; ::_thesis: p <= ((GoB h) * ((len (GoB h)),1)) `1
then A4: ex s being Point of (TOP-REAL 2) st
( p = s `1 & s in L~ h ) ;
1 <= width (GoB h) by GOBOARD7:33;
hence p <= ((GoB h) * ((len (GoB h)),1)) `1 by A4, Th32; ::_thesis: verum
end;
A5: 1 <= width (GoB h) by GOBOARD7:33;
1 <= len (GoB h) by GOBOARD7:32;
then consider q1 being Point of (TOP-REAL 2) such that
A6: q1 `1 = ((GoB h) * ((len (GoB h)),1)) `1 and
A7: q1 in L~ h by A5, Th35;
reconsider q11 = q1 `1 as Real ;
for q being real number st ( for p being real number st p in X holds
p <= q ) holds
((GoB h) * ((len (GoB h)),1)) `1 <= q
proof
A8: q11 in X by A7;
let q be real number ; ::_thesis: ( ( for p being real number st p in X holds
p <= q ) implies ((GoB h) * ((len (GoB h)),1)) `1 <= q )
assume for p being real number st p in X holds
p <= q ; ::_thesis: ((GoB h) * ((len (GoB h)),1)) `1 <= q
hence ((GoB h) * ((len (GoB h)),1)) `1 <= q by A6, A8; ::_thesis: verum
end;
hence upper_bound X = ((GoB h) * ((len (GoB h)),1)) `1 by A3, SEQ_4:46; ::_thesis: verum
end;
hence E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1 by Th17; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2
set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ;
set A = ((GoB h) * (1,(width (GoB h)))) `2 ;
consider a being set such that
A1: a in L~ h by XBOOLE_0:def_1;
A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL )
assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL
then ex qq being Point of (TOP-REAL 2) st
( b = qq `2 & qq in L~ h ) ;
hence b in REAL ; ::_thesis: verum
end;
reconsider a = a as Point of (TOP-REAL 2) by A1;
a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1;
then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2;
upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2
proof
A3: 1 <= len (GoB h) by GOBOARD7:32;
A4: for p being real number st p in X holds
p <= ((GoB h) * (1,(width (GoB h)))) `2
proof
let p be real number ; ::_thesis: ( p in X implies p <= ((GoB h) * (1,(width (GoB h)))) `2 )
assume p in X ; ::_thesis: p <= ((GoB h) * (1,(width (GoB h)))) `2
then ex s being Point of (TOP-REAL 2) st
( p = s `2 & s in L~ h ) ;
hence p <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, Th34; ::_thesis: verum
end;
1 <= width (GoB h) by GOBOARD7:33;
then consider q1 being Point of (TOP-REAL 2) such that
A5: q1 `2 = ((GoB h) * (1,(width (GoB h)))) `2 and
A6: q1 in L~ h by A3, Th36;
reconsider q11 = q1 `2 as Real ;
for q being real number st ( for p being real number st p in X holds
p <= q ) holds
((GoB h) * (1,(width (GoB h)))) `2 <= q
proof
A7: q11 in X by A6;
let q be real number ; ::_thesis: ( ( for p being real number st p in X holds
p <= q ) implies ((GoB h) * (1,(width (GoB h)))) `2 <= q )
assume for p being real number st p in X holds
p <= q ; ::_thesis: ((GoB h) * (1,(width (GoB h)))) `2 <= q
hence ((GoB h) * (1,(width (GoB h)))) `2 <= q by A5, A7; ::_thesis: verum
end;
hence upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2 by A4, SEQ_4:46; ::_thesis: verum
end;
hence N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2 by Th18; ::_thesis: verum
end;
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
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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
let i, I, i1 be Element of NAT ; ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB f) * (I,i1)) `2 <= (f /. i) `2 )
A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53;
assume A2: ( 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 ) ; ::_thesis: ((GoB f) * (I,i1)) `2 <= (f /. i) `2
then A3: i in dom f by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A4: [i2,j2] in Indices (GoB f) and
A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11;
A6: j2 <= width (GoB f) by A4, MATRIX_1:38;
A7: 1 <= j2 by A4, MATRIX_1:38;
then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_1:36;
A9: i2 <= len (GoB f) by A4, MATRIX_1:38;
1 <= i2 by A4, MATRIX_1:38;
then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A7, A6, GOBOARD5:1
.= ((GoB f) * (I,j2)) `2 by A2, A7, A6, GOBOARD5:1 ;
i1 in Y by A2, XXREAL_2:def_7;
then ex j being Element of NAT st
( i1 = j & [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2;
then A11: 1 <= i1 by MATRIX_1:38;
(f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A7, A6, GOBOARD5:2;
then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53;
then j2 in Y by A2, A3, A8;
then A12: i1 <= j2 by A2, XXREAL_2:def_7;
A13: j2 <= width (GoB f) by A4, MATRIX_1:38;
now__::_thesis:_(_(_i1_<_j2_&_((GoB_f)_*_(I,i1))_`2_<=_((GoB_f)_*_(I,j2))_`2_)_or_(_i1_>=_j2_&_((GoB_f)_*_(I,i1))_`2_<=_((GoB_f)_*_(I,j2))_`2_)_)
percases ( i1 < j2 or i1 >= j2 ) ;
case i1 < j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2
hence ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 by A2, A11, A13, GOBOARD5:4; ::_thesis: verum
end;
case i1 >= j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2
hence ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 by A12, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence ((GoB f) * (I,i1)) `2 <= (f /. i) `2 by A10; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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
let i, I, i1 be Element of NAT ; ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB h) * (i1,I)) `1 <= (h /. i) `1 )
A1: h /. i = |[((h /. i) `1),((h /. i) `2)]| by EUCLID:53;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (i1,I)) `1 <= (h /. i) `1
then A3: i in dom h by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A4: [i2,j2] in Indices (GoB h) and
A5: h /. i = (GoB h) * (i2,j2) by GOBOARD5:11;
A6: i2 <= len (GoB h) by A4, MATRIX_1:38;
A7: 1 <= i2 by A4, MATRIX_1:38;
then A8: [i2,I] in Indices (GoB h) by A2, A6, MATRIX_1:36;
A9: j2 <= width (GoB h) by A4, MATRIX_1:38;
1 <= j2 by A4, MATRIX_1:38;
then A10: (h /. i) `1 = ((GoB h) * (i2,1)) `1 by A5, A7, A6, A9, GOBOARD5:2
.= ((GoB h) * (i2,I)) `1 by A2, A7, A6, GOBOARD5:2 ;
i1 in Y by A2, XXREAL_2:def_7;
then ex j being Element of NAT st
( i1 = j & [j,I] in Indices (GoB h) & ex k being Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) by A2;
then A11: 1 <= i1 by MATRIX_1:38;
(h /. i) `2 = ((GoB h) * (i2,I)) `2 by A2, A7, A6, GOBOARD5:1;
then h /. i = (GoB h) * (i2,I) by A10, A1, EUCLID:53;
then i2 in Y by A2, A3, A8;
then A12: i1 <= i2 by A2, XXREAL_2:def_7;
A13: i2 <= len (GoB h) by A4, MATRIX_1:38;
now__::_thesis:_(_(_i1_<_i2_&_((GoB_h)_*_(i1,I))_`1_<=_((GoB_h)_*_(i2,I))_`1_)_or_(_i1_>=_i2_&_((GoB_h)_*_(i1,I))_`1_<=_((GoB_h)_*_(i2,I))_`1_)_)
percases ( i1 < i2 or i1 >= i2 ) ;
case i1 < i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1
hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A2, A11, A13, GOBOARD5:3; ::_thesis: verum
end;
case i1 >= i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1
hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A12, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,I)) `1 <= (h /. i) `1 by A10; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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
let i, I, i1 be Element of NAT ; ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB h) * (i1,I)) `1 >= (h /. i) `1 )
A1: h /. i = |[((h /. i) `1),((h /. i) `2)]| by EUCLID:53;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (i1,I)) `1 >= (h /. i) `1
then A3: i in dom h by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A4: [i2,j2] in Indices (GoB h) and
A5: h /. i = (GoB h) * (i2,j2) by GOBOARD5:11;
A6: 1 <= i2 by A4, MATRIX_1:38;
A7: i2 <= len (GoB h) by A4, MATRIX_1:38;
then A8: [i2,I] in Indices (GoB h) by A2, A6, MATRIX_1:36;
A9: j2 <= width (GoB h) by A4, MATRIX_1:38;
1 <= j2 by A4, MATRIX_1:38;
then A10: (h /. i) `1 = ((GoB h) * (i2,1)) `1 by A5, A6, A7, A9, GOBOARD5:2
.= ((GoB h) * (i2,I)) `1 by A2, A6, A7, GOBOARD5:2 ;
i1 in Y by A2, XXREAL_2:def_8;
then ex j being Element of NAT st
( i1 = j & [j,I] in Indices (GoB h) & ex k being Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) by A2;
then A11: i1 <= len (GoB h) by MATRIX_1:38;
(h /. i) `2 = ((GoB h) * (i2,I)) `2 by A2, A6, A7, GOBOARD5:1;
then h /. i = (GoB h) * (i2,I) by A10, A1, EUCLID:53;
then i2 in Y by A2, A3, A8;
then A12: i1 >= i2 by A2, XXREAL_2:def_8;
now__::_thesis:_(_(_i1_>_i2_&_((GoB_h)_*_(i1,I))_`1_>=_((GoB_h)_*_(i2,I))_`1_)_or_(_i1_<=_i2_&_((GoB_h)_*_(i1,I))_`1_>=_((GoB_h)_*_(i2,I))_`1_)_)
percases ( i1 > i2 or i1 <= i2 ) ;
case i1 > i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1
hence ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 by A2, A6, A11, GOBOARD5:3; ::_thesis: verum
end;
case i1 <= i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1
hence ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 by A12, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,I)) `1 >= (h /. i) `1 by A10; ::_thesis: verum
end;
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
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: 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
let i, I, i1 be Element of NAT ; ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB f) * (I,i1)) `2 >= (f /. i) `2 )
A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53;
assume A2: ( 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 ) ; ::_thesis: ((GoB f) * (I,i1)) `2 >= (f /. i) `2
then A3: i in dom f by FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A4: [i2,j2] in Indices (GoB f) and
A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11;
A6: 1 <= j2 by A4, MATRIX_1:38;
A7: j2 <= width (GoB f) by A4, MATRIX_1:38;
then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_1:36;
A9: i2 <= len (GoB f) by A4, MATRIX_1:38;
1 <= i2 by A4, MATRIX_1:38;
then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A6, A7, GOBOARD5:1
.= ((GoB f) * (I,j2)) `2 by A2, A6, A7, GOBOARD5:1 ;
i1 in Y by A2, XXREAL_2:def_8;
then ex j being Element of NAT st
( i1 = j & [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2;
then A11: i1 <= width (GoB f) by MATRIX_1:38;
(f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A6, A7, GOBOARD5:2;
then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53;
then j2 in Y by A2, A3, A8;
then A12: i1 >= j2 by A2, XXREAL_2:def_8;
now__::_thesis:_(_(_i1_>_j2_&_((GoB_f)_*_(I,i1))_`2_>=_((GoB_f)_*_(I,j2))_`2_)_or_(_i1_<=_j2_&_((GoB_f)_*_(I,i1))_`2_>=_((GoB_f)_*_(I,j2))_`2_)_)
percases ( i1 > j2 or i1 <= j2 ) ;
case i1 > j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2
hence ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 by A2, A11, A6, GOBOARD5:4; ::_thesis: verum
end;
case i1 <= j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2
hence ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 by A12, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence ((GoB f) * (I,i1)) `2 >= (f /. i) `2 by A10; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * (1,i1)) `2 <= p `2 )
A1: 1 <= len (GoB h) by GOBOARD7:32;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `1 = ((GoB h) * (1,1)) `1 by A2, Th37;
A9: 1 <= width (GoB h) by GOBOARD7:33;
now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_)
percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A13: (h /. i) `2 <= p `2 by A5, TOPREAL1:4;
((GoB h) * (1,i1)) `2 <= (h /. i) `2 by A2, A8, A1, A3, A7, A11, Th41;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A14: (h /. (i + 1)) `2 <= p `2 by A5, TOPREAL1:4;
((GoB h) * (1,i1)) `2 <= (h /. (i + 1)) `2 by A2, A8, A1, A4, A6, A12, Th41;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum
end;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A18: (h /. i) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3;
(h /. i) `1 >= ((GoB h) * (1,1)) `1 by A9, A3, A7, Th5;
then (h /. i) `1 = ((GoB h) * (1,1)) `1 by A18, XXREAL_0:1;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A3, A7, A16, Th41; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A19: (h /. (i + 1)) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3;
(h /. (i + 1)) `1 >= ((GoB h) * (1,1)) `1 by A9, A4, A6, Th5;
then (h /. (i + 1)) `1 = ((GoB h) * (1,1)) `1 by A19, XXREAL_0:1;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A4, A6, A17, Th41; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * (1,i1)) `2 >= p `2 )
A1: 1 <= len (GoB h) by GOBOARD7:32;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `1 = ((GoB h) * (1,1)) `1 by A2, Th37;
A9: 1 <= width (GoB h) by GOBOARD7:33;
now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_)
percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_)
percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ;
case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then A13: (h /. i) `2 >= p `2 by A5, TOPREAL1:4;
((GoB h) * (1,i1)) `2 >= (h /. i) `2 by A2, A8, A3, A1, A7, A11, Th44;
hence ((GoB h) * (1,i1)) `2 >= p `2 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then A14: (h /. (i + 1)) `2 >= p `2 by A5, TOPREAL1:4;
((GoB h) * (1,i1)) `2 >= (h /. (i + 1)) `2 by A2, A8, A4, A1, A6, A12, Th44;
hence ((GoB h) * (1,i1)) `2 >= p `2 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum
end;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then A18: (h /. i) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3;
(h /. i) `1 >= ((GoB h) * (1,1)) `1 by A3, A9, A7, Th5;
then (h /. i) `1 = ((GoB h) * (1,1)) `1 by A18, XXREAL_0:1;
hence ((GoB h) * (1,i1)) `2 >= p `2 by A2, A3, A1, A7, A16, Th44; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2
then A19: (h /. (i + 1)) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3;
(h /. (i + 1)) `1 >= ((GoB h) * (1,1)) `1 by A4, A9, A6, Th5;
then (h /. (i + 1)) `1 = ((GoB h) * (1,1)) `1 by A19, XXREAL_0:1;
hence ((GoB h) * (1,i1)) `2 >= p `2 by A2, A4, A1, A6, A17, Th44; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 )
A1: 1 <= len (GoB h) by GOBOARD7:32;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A2, Th39;
A9: 1 <= width (GoB h) by GOBOARD7:33;
now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_)
percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then A13: (h /. i) `2 <= p `2 by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 <= (h /. i) `2 by A2, A8, A3, A7, A1, A11, Th41;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then A14: (h /. (i + 1)) `2 <= p `2 by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 <= (h /. (i + 1)) `2 by A2, A8, A4, A6, A1, A12, Th41;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum
end;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_)
percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ;
case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then A18: (h /. i) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3;
(h /. i) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A3, A7, Th5;
then (h /. i) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A18, XXREAL_0:1;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A2, A3, A7, A1, A16, Th41; ::_thesis: verum
end;
case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
then A19: (h /. (i + 1)) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3;
(h /. (i + 1)) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A4, A6, Th5;
then (h /. (i + 1)) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A19, XXREAL_0:1;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A2, A4, A6, A1, A17, Th41; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 )
A1: 1 <= len (GoB h) by GOBOARD7:32;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A2, Th39;
A9: 1 <= width (GoB h) by GOBOARD7:33;
now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_)
percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_)
percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ;
case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then A13: (h /. i) `2 >= p `2 by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. i) `2 by A2, A8, A1, A3, A7, A11, Th44;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then A14: (h /. (i + 1)) `2 >= p `2 by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. (i + 1)) `2 by A2, A8, A1, A4, A6, A12, Th44;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum
end;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_)
percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ;
case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then A18: (h /. i) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3;
(h /. i) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A3, A7, Th5;
then (h /. i) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A18, XXREAL_0:1;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A2, A1, A3, A7, A16, Th44; ::_thesis: verum
end;
case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then A19: (h /. (i + 1)) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3;
(h /. (i + 1)) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A4, A6, Th5;
then (h /. (i + 1)) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A19, XXREAL_0:1;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A2, A1, A4, A6, A17, Th44; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * (i1,1)) `1 <= p `1 )
A1: 1 <= width (GoB h) by GOBOARD7:33;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `2 = ((GoB h) * (1,1)) `2 by A2, Th38;
A9: 1 <= len (GoB h) by GOBOARD7:32;
now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_)
percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A11: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A12: p `2 = (h /. (i + 1)) `2 by A5, A10, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then A13: (h /. i) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,1)) `1 <= (h /. i) `1 by A2, A8, A3, A7, A1, A11, Th42;
hence ((GoB h) * (i1,1)) `1 <= p `1 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then A14: (h /. (i + 1)) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,1)) `1 <= (h /. (i + 1)) `1 by A2, A8, A4, A1, A6, A12, Th42;
hence ((GoB h) * (i1,1)) `1 <= p `1 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum
end;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A16: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A17: p `1 = (h /. (i + 1)) `1 by A5, A15, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then A18: (h /. i) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4;
(h /. i) `2 >= ((GoB h) * (1,1)) `2 by A3, A7, A9, Th6;
then (h /. i) `2 = ((GoB h) * (1,1)) `2 by A18, XXREAL_0:1;
hence ((GoB h) * (i1,1)) `1 <= p `1 by A2, A3, A7, A1, A16, Th42; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1
then A19: (h /. (i + 1)) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4;
(h /. (i + 1)) `2 >= ((GoB h) * (1,1)) `2 by A4, A9, A6, Th6;
then (h /. (i + 1)) `2 = ((GoB h) * (1,1)) `2 by A19, XXREAL_0:1;
hence ((GoB h) * (i1,1)) `1 <= p `1 by A2, A4, A1, A6, A17, Th42; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum
end;
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
proof
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: 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
let h be non constant standard special_circular_sequence; ::_thesis: ( 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 implies ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 )
set I = width (GoB h);
A1: 1 <= width (GoB h) by GOBOARD7:33;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A2, Th40;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: 1 <= i + 1 by A3, XREAL_1:145;
now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_)
percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A9: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A10: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A11: p `2 = (h /. (i + 1)) `2 by A5, A9, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_)
percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ;
case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then A12: (h /. i) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. i) `1 by A2, A6, A1, A3, A7, A10, Th42;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A12, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then A13: (h /. (i + 1)) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. (i + 1)) `1 by A2, A6, A1, A4, A8, A11, Th42;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A13, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum
end;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A14: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A15: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A16: 1 <= len (GoB h) by GOBOARD7:32;
A17: p `1 = (h /. (i + 1)) `1 by A5, A14, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_)
percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ;
case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then A18: (h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4;
(h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A16, Th6;
then (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A18, XXREAL_0:1;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A3, A7, A15, Th42; ::_thesis: verum
end;
case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
then A19: (h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4;
(h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A4, A8, A16, Th6;
then (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A4, A8, A17, Th42; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB h) * (i1,1)) `1 >= p `1 )
A1: 1 <= width (GoB h) by GOBOARD7:33;
assume A2: ( 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 ) ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then consider i being Element of NAT such that
A3: 1 <= i and
A4: i + 1 <= len h and
A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A6: 1 <= i + 1 by A3, XREAL_1:145;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: p `2 = ((GoB h) * (1,1)) `2 by A2, Th38;
A9: 1 <= len (GoB h) by GOBOARD7:32;
now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_)
percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3;
then A10: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A11: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A12: p `2 = (h /. (i + 1)) `2 by A5, A10, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_)
percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ;
case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then A13: (h /. i) `1 >= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,1)) `1 >= (h /. i) `1 by A2, A8, A3, A7, A1, A11, Th43;
hence ((GoB h) * (i1,1)) `1 >= p `1 by A13, XXREAL_0:2; ::_thesis: verum
end;
case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then A14: (h /. (i + 1)) `1 >= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,1)) `1 >= (h /. (i + 1)) `1 by A2, A8, A4, A1, A6, A12, Th43;
hence ((GoB h) * (i1,1)) `1 >= p `1 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum
end;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3;
then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A16: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A17: p `1 = (h /. (i + 1)) `1 by A5, A15, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_)
percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;
case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then A18: (h /. i) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4;
(h /. i) `2 >= ((GoB h) * (1,1)) `2 by A3, A7, A9, Th6;
then (h /. i) `2 = ((GoB h) * (1,1)) `2 by A18, XXREAL_0:1;
hence ((GoB h) * (i1,1)) `1 >= p `1 by A2, A3, A7, A1, A16, Th43; ::_thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1
then A19: (h /. (i + 1)) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4;
(h /. (i + 1)) `2 >= ((GoB h) * (1,1)) `2 by A4, A9, A6, Th6;
then (h /. (i + 1)) `2 = ((GoB h) * (1,1)) `2 by A19, XXREAL_0:1;
hence ((GoB h) * (i1,1)) `1 >= p `1 by A2, A4, A1, A6, A17, Th43; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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
let i1 be Element of NAT ; ::_thesis: 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
let p be Point of (TOP-REAL 2); ::_thesis: 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
let Y be non empty finite Subset of NAT; ::_thesis: ( 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 implies ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 )
assume A1: ( 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 ) ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
then consider i being Element of NAT such that
A2: 1 <= i and
A3: i + 1 <= len h and
A4: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;
A5: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A1, Th40;
i <= i + 1 by NAT_1:11;
then A6: i <= len h by A3, XXREAL_0:2;
A7: 1 <= i + 1 by A2, XREAL_1:145;
now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_)
percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19;
case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A2, A3, TOPREAL1:def_3;
then A8: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A9: p `2 = (h /. i) `2 by A4, GOBOARD7:6;
A10: p `2 = (h /. (i + 1)) `2 by A4, A8, GOBOARD7:6;
now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_)
percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ;
caseA11: (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
1 <= width (GoB h) by GOBOARD7:33;
then A12: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. i) `1 by A1, A5, A2, A6, A9, Th43;
(h /. i) `1 >= p `1 by A4, A11, TOPREAL1:3;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A12, XXREAL_0:2; ::_thesis: verum
end;
caseA13: (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
1 <= width (GoB h) by GOBOARD7:33;
then A14: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. (i + 1)) `1 by A1, A5, A3, A7, A10, Th43;
(h /. (i + 1)) `1 >= p `1 by A4, A13, TOPREAL1:3;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum
end;
case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
then LSeg ((h /. i),(h /. (i + 1))) is vertical by A2, A3, TOPREAL1:def_3;
then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A16: p `1 = (h /. i) `1 by A4, GOBOARD7:5;
A17: 1 <= len (GoB h) by GOBOARD7:32;
A18: p `1 = (h /. (i + 1)) `1 by A4, A15, GOBOARD7:5;
now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_)
percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ;
case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
then A19: (h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A5, A4, TOPREAL1:4;
(h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A2, A6, A17, Th6;
then A20: (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1;
1 <= width (GoB h) by GOBOARD7:33;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A2, A6, A16, A20, Th43; ::_thesis: verum
end;
case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
then A21: (h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A5, A4, TOPREAL1:4;
(h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A17, Th6;
then A22: (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A21, XXREAL_0:1;
1 <= width (GoB h) by GOBOARD7:33;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A3, A7, A18, A22, Th43; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum
end;
end;
end;
hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum
end;
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) )
proof
{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * (1,1)) `2 ;
defpred S1[ Element of NAT ] means ( [1,$1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,$1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A1: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [1,j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,j) ) ) ;
then [1,y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum
end;
A2: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
A3: 1 <= len (GoB g) by GOBOARD7:32;
then consider i, j being Element of NAT such that
A4: i in dom g and
A5: [1,j] in Indices (GoB g) and
A6: g /. i = (GoB g) * (1,j) by Th7;
j in { j where j is Element of NAT : S1[j] } by A4, A5, A6;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A1, A2;
set i1 = min Y;
min Y in Y by XXREAL_2:def_7;
then consider j being Element of NAT such that
A7: j = min Y and
A8: [1,j] in Indices (GoB g) and
A9: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,j) ) ;
A10: min Y <= width (GoB g) by A7, A8, MATRIX_1:38;
A11: 1 <= len (GoB g) by A8, MATRIX_1:38;
1 <= min Y by A7, A8, MATRIX_1:38;
then A12: ((GoB g) * (1,(min Y))) `1 = ((GoB g) * (1,1)) `1 by A11, A10, GOBOARD5:2;
then A13: ((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by Th37;
consider i being Element of NAT such that
A14: i in dom g and
A15: g /. i = (GoB g) * (1,j) by A9;
A16: i <= len g by A14, FINSEQ_3:25;
A17: 1 <= i by A14, FINSEQ_3:25;
A18: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(1,(min_Y))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(1,(min_Y))_in_L~_g_)_)
percases ( i < len g or i = len g ) by A16, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * (1,(min Y)) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A17, TOPREAL1:21;
hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * (1,(min Y)) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by A12, Th37;
then A19: ((GoB g) * (1,(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } by A18;
for r being real number st r in B holds
r >= ((GoB g) * (1,(min Y))) `2
proof
let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * (1,(min Y))) `2 )
assume r in B ; ::_thesis: r >= ((GoB g) * (1,(min Y))) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence r >= ((GoB g) * (1,(min Y))) `2 by Lm1; ::_thesis: verum
end;
then A20: lower_bound B >= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:43;
((GoB g) * (1,1)) `2 is LowerBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,1)) `2 <= r )
assume r in B ; ::_thesis: ((GoB g) * (1,1)) `2 <= r
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence ((GoB g) * (1,1)) `2 <= r by A3, Th33; ::_thesis: verum
end;
then B is bounded_below by XXREAL_2:def_9;
then lower_bound B <= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:def_2;
then ((GoB g) * (1,(min Y))) `2 = lower_bound B by A20, XXREAL_0:1
.= lower_bound (proj2 | (W-most (L~ g))) by Th13 ;
hence ex b1 being Element of NAT st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) ) by A7, A8, A13, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * (1,(width (GoB g)))) `2 ;
defpred S1[ Element of NAT ] means ( [1,$1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,$1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A21: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [1,j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,j) ) ) ;
then [1,y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum
end;
A22: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
A23: 1 <= len (GoB g) by GOBOARD7:32;
then consider i, j being Element of NAT such that
A24: i in dom g and
A25: [1,j] in Indices (GoB g) and
A26: g /. i = (GoB g) * (1,j) by Th7;
j in { j where j is Element of NAT : S1[j] } by A24, A25, A26;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A21, A22;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12;
i1 in Y by XXREAL_2:def_8;
then consider j being Element of NAT such that
A27: j = i1 and
A28: [1,j] in Indices (GoB g) and
A29: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (1,j) ) ;
A30: i1 <= width (GoB g) by A27, A28, MATRIX_1:38;
A31: 1 <= len (GoB g) by A28, MATRIX_1:38;
1 <= i1 by A27, A28, MATRIX_1:38;
then A32: ((GoB g) * (1,i1)) `1 = ((GoB g) * (1,1)) `1 by A31, A30, GOBOARD5:2;
then A33: ((GoB g) * (1,i1)) `1 = W-bound (L~ g) by Th37;
consider i being Element of NAT such that
A34: i in dom g and
A35: g /. i = (GoB g) * (1,j) by A29;
A36: i <= len g by A34, FINSEQ_3:25;
A37: 1 <= i by A34, FINSEQ_3:25;
A38: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(1,i1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(1,i1)_in_L~_g_)_)
percases ( i < len g or i = len g ) by A36, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * (1,i1) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A37, TOPREAL1:21;
hence (GoB g) * (1,i1) in L~ g by A27, A35, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * (1,i1) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * (1,i1) in L~ g by A27, A35, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * (1,i1)) `1 = W-bound (L~ g) by A32, Th37;
then A39: ((GoB g) * (1,i1)) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } by A38;
for r being real number st r in B holds
r <= ((GoB g) * (1,i1)) `2
proof
let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (1,i1)) `2 )
assume r in B ; ::_thesis: r <= ((GoB g) * (1,i1)) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * (1,i1)) `2 by Lm2; ::_thesis: verum
end;
then A40: upper_bound B <= ((GoB g) * (1,i1)) `2 by A39, SEQ_4:45;
((GoB g) * (1,(width (GoB g)))) `2 is UpperBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * (1,(width (GoB g)))) `2 )
assume r in B ; ::_thesis: r <= ((GoB g) * (1,(width (GoB g)))) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * (1,(width (GoB g)))) `2 by A23, Th34; ::_thesis: verum
end;
then B is bounded_above by XXREAL_2:def_10;
then upper_bound B >= ((GoB g) * (1,i1)) `2 by A39, SEQ_4:def_1;
then ((GoB g) * (1,i1)) `2 = upper_bound B by A40, XXREAL_0:1
.= upper_bound (proj2 | (W-most (L~ g))) by Th13 ;
hence ex b1 being Element of NAT st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) ) by A27, A28, A33, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * ((len (GoB g)),1)) `2 ;
defpred S1[ Element of NAT ] means ( [(len (GoB g)),$1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),$1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A41: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ) ;
then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum
end;
A42: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
A43: 1 <= len (GoB g) by GOBOARD7:32;
then consider i, j being Element of NAT such that
A44: i in dom g and
A45: [(len (GoB g)),j] in Indices (GoB g) and
A46: g /. i = (GoB g) * ((len (GoB g)),j) by Th7;
j in { j where j is Element of NAT : S1[j] } by A44, A45, A46;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A41, A42;
set i1 = min Y;
min Y in Y by XXREAL_2:def_7;
then consider j being Element of NAT such that
A47: j = min Y and
A48: [(len (GoB g)),j] in Indices (GoB g) and
A49: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ;
A50: min Y <= width (GoB g) by A47, A48, MATRIX_1:38;
A51: 1 <= len (GoB g) by A48, MATRIX_1:38;
1 <= min Y by A47, A48, MATRIX_1:38;
then A52: ((GoB g) * ((len (GoB g)),(min Y))) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A51, A50, GOBOARD5:2;
then A53: ((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by Th39;
consider i being Element of NAT such that
A54: i in dom g and
A55: g /. i = (GoB g) * ((len (GoB g)),j) by A49;
A56: i <= len g by A54, FINSEQ_3:25;
A57: 1 <= i by A54, FINSEQ_3:25;
A58: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((len_(GoB_g)),(min_Y))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((len_(GoB_g)),(min_Y))_in_L~_g_)_)
percases ( i < len g or i = len g ) by A56, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * ((len (GoB g)),(min Y)) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A57, TOPREAL1:21;
hence (GoB g) * ((len (GoB g)),(min Y)) in L~ g by A47, A55, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * ((len (GoB g)),(min Y)) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * ((len (GoB g)),(min Y)) in L~ g by A47, A55, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by A52, Th39;
then A59: ((GoB g) * ((len (GoB g)),(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A58;
for r being real number st r in B holds
r >= ((GoB g) * ((len (GoB g)),(min Y))) `2
proof
let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 )
assume r in B ; ::_thesis: r >= ((GoB g) * ((len (GoB g)),(min Y))) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by Lm3; ::_thesis: verum
end;
then A60: lower_bound B >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:43;
((GoB g) * ((len (GoB g)),1)) `2 is LowerBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * ((len (GoB g)),1)) `2 <= r )
assume r in B ; ::_thesis: ((GoB g) * ((len (GoB g)),1)) `2 <= r
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence ((GoB g) * ((len (GoB g)),1)) `2 <= r by A43, Th33; ::_thesis: verum
end;
then B is bounded_below by XXREAL_2:def_9;
then lower_bound B <= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:def_2;
then ((GoB g) * ((len (GoB g)),(min Y))) `2 = lower_bound B by A60, XXREAL_0:1
.= lower_bound (proj2 | (E-most (L~ g))) by Th14 ;
hence 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) ) by A47, A48, A53, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S1[ Element of NAT ] means ( [(len (GoB g)),$1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),$1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A61: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ) ;
then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum
end;
A62: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
0 <> len (GoB g) by GOBOARD1:def_3;
then 1 <= len (GoB g) by NAT_1:14;
then consider i, j being Element of NAT such that
A63: i in dom g and
A64: [(len (GoB g)),j] in Indices (GoB g) and
A65: g /. i = (GoB g) * ((len (GoB g)),j) by Th7;
j in { j where j is Element of NAT : S1[j] } by A63, A64, A65;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A61, A62;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12;
set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 ;
i1 in Y by XXREAL_2:def_8;
then consider j being Element of NAT such that
A66: j = i1 and
A67: [(len (GoB g)),j] in Indices (GoB g) and
A68: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ;
A69: i1 <= width (GoB g) by A66, A67, MATRIX_1:38;
A70: 1 <= len (GoB g) by A67, MATRIX_1:38;
1 <= i1 by A66, A67, MATRIX_1:38;
then A71: ((GoB g) * ((len (GoB g)),i1)) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A70, A69, GOBOARD5:2;
then A72: ((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by Th39;
consider i being Element of NAT such that
A73: i in dom g and
A74: g /. i = (GoB g) * ((len (GoB g)),j) by A68;
A75: i <= len g by A73, FINSEQ_3:25;
A76: 1 <= i by A73, FINSEQ_3:25;
A77: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((len_(GoB_g)),i1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((len_(GoB_g)),i1)_in_L~_g_)_)
percases ( i < len g or i = len g ) by A75, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * ((len (GoB g)),i1) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A76, TOPREAL1:21;
hence (GoB g) * ((len (GoB g)),i1) in L~ g by A66, A74, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * ((len (GoB g)),i1) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * ((len (GoB g)),i1) in L~ g by A66, A74, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by A71, Th39;
then A78: ((GoB g) * ((len (GoB g)),i1)) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A77;
for r being real number st r in B holds
r <= ((GoB g) * ((len (GoB g)),i1)) `2
proof
let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * ((len (GoB g)),i1)) `2 )
assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),i1)) `2
then ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * ((len (GoB g)),i1)) `2 by Lm4; ::_thesis: verum
end;
then A79: upper_bound B <= ((GoB g) * ((len (GoB g)),i1)) `2 by A78, SEQ_4:45;
((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 is UpperBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 )
assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2
then A80: ex q being Point of (TOP-REAL 2) st
( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
1 <= len (GoB g) by GOBOARD7:32;
hence r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 by A80, Th34; ::_thesis: verum
end;
then B is bounded_above by XXREAL_2:def_10;
then upper_bound B >= ((GoB g) * ((len (GoB g)),i1)) `2 by A78, SEQ_4:def_1;
then ((GoB g) * ((len (GoB g)),i1)) `2 = upper_bound B by A79, XXREAL_0:1
.= upper_bound (proj2 | (E-most (L~ g))) by Th14 ;
hence 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) ) by A66, A67, A72, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * (1,1)) `1 ;
defpred S1[ Element of NAT ] means ( [$1,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ($1,1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A81: { j where j is Element of NAT : S1[j] } c= dom (GoB g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,1) ) ) ;
then [y,1] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum
end;
A82: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
A83: 1 <= width (GoB g) by GOBOARD7:33;
then consider i, j being Element of NAT such that
A84: i in dom g and
A85: [j,1] in Indices (GoB g) and
A86: g /. i = (GoB g) * (j,1) by Th8;
j in { j where j is Element of NAT : S1[j] } by A84, A85, A86;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A81, A82;
set i1 = min Y;
min Y in Y by XXREAL_2:def_7;
then consider j being Element of NAT such that
A87: j = min Y and
A88: [j,1] in Indices (GoB g) and
A89: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,1) ) ;
A90: min Y <= len (GoB g) by A87, A88, MATRIX_1:38;
A91: 1 <= width (GoB g) by A88, MATRIX_1:38;
1 <= min Y by A87, A88, MATRIX_1:38;
then A92: ((GoB g) * ((min Y),1)) `2 = ((GoB g) * (1,1)) `2 by A90, A91, GOBOARD5:1;
then A93: ((GoB g) * ((min Y),1)) `2 = S-bound (L~ g) by Th38;
consider i being Element of NAT such that
A94: i in dom g and
A95: g /. i = (GoB g) * (j,1) by A89;
A96: i <= len g by A94, FINSEQ_3:25;
A97: 1 <= i by A94, FINSEQ_3:25;
A98: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((min_Y),1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((min_Y),1)_in_L~_g_)_)
percases ( i < len g or i = len g ) by A96, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * ((min Y),1) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A97, TOPREAL1:21;
hence (GoB g) * ((min Y),1) in L~ g by A87, A95, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * ((min Y),1) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * ((min Y),1) in L~ g by A87, A95, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * ((min Y),1)) `2 = S-bound (L~ g) by A92, Th38;
then A99: ((GoB g) * ((min Y),1)) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } by A98;
for r being real number st r in B holds
r >= ((GoB g) * ((min Y),1)) `1
proof
let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((min Y),1)) `1 )
assume r in B ; ::_thesis: r >= ((GoB g) * ((min Y),1)) `1
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence r >= ((GoB g) * ((min Y),1)) `1 by Lm5; ::_thesis: verum
end;
then A100: lower_bound B >= ((GoB g) * ((min Y),1)) `1 by A99, SEQ_4:43;
((GoB g) * (1,1)) `1 is LowerBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,1)) `1 <= r )
assume r in B ; ::_thesis: ((GoB g) * (1,1)) `1 <= r
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence ((GoB g) * (1,1)) `1 <= r by A83, Th31; ::_thesis: verum
end;
then B is bounded_below by XXREAL_2:def_9;
then lower_bound B <= ((GoB g) * ((min Y),1)) `1 by A99, SEQ_4:def_2;
then ((GoB g) * ((min Y),1)) `1 = lower_bound B by A100, XXREAL_0:1
.= lower_bound (proj1 | (S-most (L~ g))) by Th16 ;
hence ex b1 being Element of NAT st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) ) by A87, A88, A93, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S1[ Element of NAT ] means ( [$1,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ($1,1) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A101: { j where j is Element of NAT : S1[j] } c= dom (GoB g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,1) ) ) ;
then [y,1] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum
end;
A102: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
1 <= width (GoB g) by GOBOARD7:33;
then consider i, j being Element of NAT such that
A103: i in dom g and
A104: [j,1] in Indices (GoB g) and
A105: g /. i = (GoB g) * (j,1) by Th8;
j in { j where j is Element of NAT : S1[j] } by A103, A104, A105;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A101, A102;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12;
set s1 = ((GoB g) * ((len (GoB g)),1)) `1 ;
i1 in Y by XXREAL_2:def_8;
then consider j being Element of NAT such that
A106: j = i1 and
A107: [j,1] in Indices (GoB g) and
A108: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,1) ) ;
A109: i1 <= len (GoB g) by A106, A107, MATRIX_1:38;
A110: 1 <= width (GoB g) by A107, MATRIX_1:38;
1 <= i1 by A106, A107, MATRIX_1:38;
then A111: ((GoB g) * (i1,1)) `2 = ((GoB g) * (1,1)) `2 by A109, A110, GOBOARD5:1;
then A112: ((GoB g) * (i1,1)) `2 = S-bound (L~ g) by Th38;
consider i being Element of NAT such that
A113: i in dom g and
A114: g /. i = (GoB g) * (j,1) by A108;
A115: i <= len g by A113, FINSEQ_3:25;
A116: 1 <= i by A113, FINSEQ_3:25;
A117: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(i1,1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(i1,1)_in_L~_g_)_)
percases ( i < len g or i = len g ) by A115, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * (i1,1) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A116, TOPREAL1:21;
hence (GoB g) * (i1,1) in L~ g by A106, A114, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * (i1,1) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * (i1,1) in L~ g by A106, A114, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * (i1,1)) `2 = S-bound (L~ g) by A111, Th38;
then A118: ((GoB g) * (i1,1)) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } by A117;
for r being real number st r in B holds
r <= ((GoB g) * (i1,1)) `1
proof
let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (i1,1)) `1 )
assume r in B ; ::_thesis: r <= ((GoB g) * (i1,1)) `1
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * (i1,1)) `1 by Lm7; ::_thesis: verum
end;
then A119: upper_bound B <= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:45;
((GoB g) * ((len (GoB g)),1)) `1 is UpperBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),1)) `1 )
assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),1)) `1
then A120: ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ;
1 <= width (GoB g) by GOBOARD7:33;
hence r <= ((GoB g) * ((len (GoB g)),1)) `1 by A120, Th32; ::_thesis: verum
end;
then B is bounded_above by XXREAL_2:def_10;
then upper_bound B >= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:def_1;
then ((GoB g) * (i1,1)) `1 = upper_bound B by A119, XXREAL_0:1
.= upper_bound (proj1 | (S-most (L~ g))) by Th16 ;
hence ex b1 being Element of NAT st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) ) by A106, A107, A112, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S1[ Element of NAT ] means ( [$1,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ($1,(width (GoB g))) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A121: { j where j is Element of NAT : S1[j] } c= dom (GoB g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ) ;
then [y,(width (GoB g))] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum
end;
A122: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
1 <= width (GoB g) by GOBOARD7:33;
then consider i, j being Element of NAT such that
A123: i in dom g and
A124: [j,(width (GoB g))] in Indices (GoB g) and
A125: g /. i = (GoB g) * (j,(width (GoB g))) by Th8;
j in { j where j is Element of NAT : S1[j] } by A123, A124, A125;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A121, A122;
set i1 = min Y;
set s1 = ((GoB g) * (1,(width (GoB g)))) `1 ;
min Y in Y by XXREAL_2:def_7;
then consider j being Element of NAT such that
A126: j = min Y and
A127: [j,(width (GoB g))] in Indices (GoB g) and
A128: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ;
A129: min Y <= len (GoB g) by A126, A127, MATRIX_1:38;
A130: 1 <= width (GoB g) by A127, MATRIX_1:38;
1 <= min Y by A126, A127, MATRIX_1:38;
then A131: ((GoB g) * ((min Y),(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A129, A130, GOBOARD5:1;
then A132: ((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g) by Th40;
consider i being Element of NAT such that
A133: i in dom g and
A134: g /. i = (GoB g) * (j,(width (GoB g))) by A128;
A135: i <= len g by A133, FINSEQ_3:25;
A136: 1 <= i by A133, FINSEQ_3:25;
A137: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((min_Y),(width_(GoB_g)))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((min_Y),(width_(GoB_g)))_in_L~_g_)_)
percases ( i < len g or i = len g ) by A135, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * ((min Y),(width (GoB g))) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A136, TOPREAL1:21;
hence (GoB g) * ((min Y),(width (GoB g))) in L~ g by A126, A134, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * ((min Y),(width (GoB g))) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * ((min Y),(width (GoB g))) in L~ g by A126, A134, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g) by A131, Th40;
then A138: ((GoB g) * ((min Y),(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A137;
for r being real number st r in B holds
r >= ((GoB g) * ((min Y),(width (GoB g)))) `1
proof
let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 )
assume r in B ; ::_thesis: r >= ((GoB g) * ((min Y),(width (GoB g)))) `1
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
hence r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 by Lm6; ::_thesis: verum
end;
then A139: lower_bound B >= ((GoB g) * ((min Y),(width (GoB g)))) `1 by A138, SEQ_4:43;
((GoB g) * (1,(width (GoB g)))) `1 is LowerBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,(width (GoB g)))) `1 <= r )
assume r in B ; ::_thesis: ((GoB g) * (1,(width (GoB g)))) `1 <= r
then A140: ex q1 being Point of (TOP-REAL 2) st
( r = q1 `1 & q1 `2 = N-bound (L~ g) & q1 in L~ g ) ;
1 <= width (GoB g) by GOBOARD7:33;
hence ((GoB g) * (1,(width (GoB g)))) `1 <= r by A140, Th31; ::_thesis: verum
end;
then B is bounded_below by XXREAL_2:def_9;
then lower_bound B <= ((GoB g) * ((min Y),(width (GoB g)))) `1 by A138, SEQ_4:def_2;
then ((GoB g) * ((min Y),(width (GoB g)))) `1 = lower_bound B by A139, XXREAL_0:1
.= lower_bound (proj1 | (N-most (L~ g))) by Th15 ;
hence 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) ) by A126, A127, A132, EUCLID:53; ::_thesis: verum
end;
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) )
proof
{ (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; ::_thesis: verum
end;
then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
defpred S1[ Element of NAT ] means ( [$1,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * ($1,(width (GoB g))) ) );
set Y = { j where j is Element of NAT : S1[j] } ;
A141: { j where j is Element of NAT : S1[j] } c= dom (GoB g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) )
assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ) ;
then [y,(width (GoB g))] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4;
hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum
end;
A142: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7();
1 <= width (GoB g) by GOBOARD7:33;
then consider i, j being Element of NAT such that
A143: i in dom g and
A144: [j,(width (GoB g))] in Indices (GoB g) and
A145: g /. i = (GoB g) * (j,(width (GoB g))) by Th8;
j in { j where j is Element of NAT : S1[j] } by A143, A144, A145;
then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A141, A142;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12;
set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 ;
i1 in Y by XXREAL_2:def_8;
then consider j being Element of NAT such that
A146: j = i1 and
A147: [j,(width (GoB g))] in Indices (GoB g) and
A148: ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ;
A149: i1 <= len (GoB g) by A146, A147, MATRIX_1:38;
A150: 1 <= width (GoB g) by A147, MATRIX_1:38;
1 <= i1 by A146, A147, MATRIX_1:38;
then A151: ((GoB g) * (i1,(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A149, A150, GOBOARD5:1;
then A152: ((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by Th40;
consider i being Element of NAT such that
A153: i in dom g and
A154: g /. i = (GoB g) * (j,(width (GoB g))) by A148;
A155: i <= len g by A153, FINSEQ_3:25;
A156: 1 <= i by A153, FINSEQ_3:25;
A157: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(i1,(width_(GoB_g)))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(i1,(width_(GoB_g)))_in_L~_g_)_)
percases ( i < len g or i = len g ) by A155, XXREAL_0:1;
case i < len g ; ::_thesis: (GoB g) * (i1,(width (GoB g))) in L~ g
then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg (g,i) by A156, TOPREAL1:21;
hence (GoB g) * (i1,(width (GoB g))) in L~ g by A146, A154, SPPOL_2:17; ::_thesis: verum
end;
case i = len g ; ::_thesis: (GoB g) * (i1,(width (GoB g))) in L~ g
then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1;
hence (GoB g) * (i1,(width (GoB g))) in L~ g by A146, A154, SPPOL_2:17; ::_thesis: verum
end;
end;
end;
((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by A151, Th40;
then A158: ((GoB g) * (i1,(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A157;
for r being real number st r in B holds
r <= ((GoB g) * (i1,(width (GoB g)))) `1
proof
let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (i1,(width (GoB g)))) `1 )
assume r in B ; ::_thesis: r <= ((GoB g) * (i1,(width (GoB g)))) `1
then ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
hence r <= ((GoB g) * (i1,(width (GoB g)))) `1 by Lm8; ::_thesis: verum
end;
then A159: upper_bound B <= ((GoB g) * (i1,(width (GoB g)))) `1 by A158, SEQ_4:45;
((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 is UpperBound of B
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 )
assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1
then A160: ex q being Point of (TOP-REAL 2) st
( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
1 <= width (GoB g) by GOBOARD7:33;
hence r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 by A160, Th32; ::_thesis: verum
end;
then B is bounded_above by XXREAL_2:def_10;
then upper_bound B >= ((GoB g) * (i1,(width (GoB g)))) `1 by A158, SEQ_4:def_1;
then ((GoB g) * (i1,(width (GoB g)))) `1 = upper_bound B by A159, XXREAL_0:1
.= upper_bound (proj1 | (N-most (L~ g))) by Th15 ;
hence 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) ) by A146, A147, A152, EUCLID:53; ::_thesis: verum
end;
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) )
proof
let h be non constant standard special_circular_sequence; ::_thesis: ( 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) )
A1: [(i_e_n h),(width (GoB h))] in Indices (GoB h) by Def8;
A2: [(i_w_s h),1] in Indices (GoB h) by Def5;
A3: [(i_e_s h),1] in Indices (GoB h) by Def6;
[(i_w_n h),(width (GoB h))] in Indices (GoB h) by Def7;
hence ( 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) ) by A1, A2, A3, MATRIX_1:38; ::_thesis: verum
end;
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) )
proof
let h be non constant standard special_circular_sequence; ::_thesis: ( 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) )
A1: [(len (GoB h)),(i_s_e h)] in Indices (GoB h) by Def3;
A2: [1,(i_n_w h)] in Indices (GoB h) by Def2;
A3: [1,(i_s_w h)] in Indices (GoB h) by Def1;
[(len (GoB h)),(i_n_e h)] in Indices (GoB h) by Def4;
hence ( 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) ) by A1, A2, A3, MATRIX_1:38; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: 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
let i1, i2 be Element of NAT ; ::_thesis: ( 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 implies i1 = i2 )
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len h ; ::_thesis: ( not 1 <= i2 or not i2 + 1 <= len h or not h . i1 = h . i2 or i1 = i2 )
A3: i1 < len h by A2, NAT_1:13;
assume that
A4: 1 <= i2 and
A5: i2 + 1 <= len h and
A6: h . i1 = h . i2 ; ::_thesis: i1 = i2
A7: i2 < len h by A5, NAT_1:13;
then A8: i2 in dom h by A4, FINSEQ_3:25;
assume A9: i1 <> i2 ; ::_thesis: contradiction
A10: now__::_thesis:_h_/._i1_<>_h_/._i2
percases ( i1 < i2 or i2 < i1 ) by A9, XXREAL_0:1;
suppose i1 < i2 ; ::_thesis: h /. i1 <> h /. i2
hence h /. i1 <> h /. i2 by A1, A7, GOBOARD7:36; ::_thesis: verum
end;
suppose i2 < i1 ; ::_thesis: h /. i1 <> h /. i2
hence h /. i1 <> h /. i2 by A4, A3, GOBOARD7:36; ::_thesis: verum
end;
end;
end;
i1 in dom h by A1, A3, FINSEQ_3:25;
then h /. i1 = h . i2 by A6, PARTFUN1:def_6
.= h /. i2 by A8, PARTFUN1:def_6 ;
hence contradiction by A10; ::_thesis: verum
end;
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) )
proof
W-min (L~ g) in rng g by SPRECT_2:43;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
W-max (L~ g) in rng g by SPRECT_2:44;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
E-min (L~ g) in rng g by SPRECT_2:45;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
E-max (L~ g) in rng g by SPRECT_2:46;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
S-min (L~ g) in rng g by SPRECT_2:41;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
S-max (L~ g) in rng g by SPRECT_2:42;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
N-min (L~ g) in rng g by SPRECT_2:39;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) ) by Th3; ::_thesis: verum
end;
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) )
proof
N-max (L~ g) in rng g by SPRECT_2:40;
hence ex b1 being Element of NAT st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) ) by Th3; ::_thesis: verum
end;
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
proof
let h be non constant standard special_circular_sequence; ::_thesis: n_w_n h <> n_w_s h
set i1 = n_w_n h;
set i2 = n_w_s h;
A1: n_w_n h <= (n_w_n h) + 1 by NAT_1:11;
A2: 1 <= n_w_n h by Def15;
(n_w_n h) + 1 <= len h by Def15;
then n_w_n h <= len h by A1, XXREAL_0:2;
then n_w_n h in dom h by A2, FINSEQ_3:25;
then A3: h . (n_w_n h) = h /. (n_w_n h) by PARTFUN1:def_6;
A4: n_w_s h <= (n_w_s h) + 1 by NAT_1:11;
A5: h . (n_w_s h) = S-min (L~ h) by Def13;
A6: 1 <= n_w_s h by Def13;
(n_w_s h) + 1 <= len h by Def13;
then n_w_s h <= len h by A4, XXREAL_0:2;
then n_w_s h in dom h by A6, FINSEQ_3:25;
then A7: h . (n_w_s h) = h /. (n_w_s h) by PARTFUN1:def_6;
A8: h . (n_w_n h) = N-min (L~ h) by Def15;
thus n_w_n h <> n_w_s h ::_thesis: verum
proof
assume n_w_n h = n_w_s h ; ::_thesis: contradiction
then A9: N-bound (L~ h) = (h /. (n_w_s h)) `2 by A8, A3, EUCLID:52
.= S-bound (L~ h) by A5, A7, EUCLID:52 ;
A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;
then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11;
consider ii being Element of NAT such that
A12: ii in dom h and
A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31;
A14: ii <= len h by A12, FINSEQ_3:25;
A15: 1 <= ii by A12, FINSEQ_3:25;
then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11;
A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11;
(h /. 1) `2 <= N-bound (L~ h) by A10, Th11;
then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1;
hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum
end;
end;
theorem :: JORDAN5D:48
for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h
proof
let h be non constant standard special_circular_sequence; ::_thesis: n_s_w h <> n_s_e h
set i1 = n_s_w h;
set i2 = n_s_e h;
A1: n_s_w h <= (n_s_w h) + 1 by NAT_1:11;
A2: 1 <= n_s_w h by Def9;
(n_s_w h) + 1 <= len h by Def9;
then n_s_w h <= len h by A1, XXREAL_0:2;
then n_s_w h in dom h by A2, FINSEQ_3:25;
then A3: h . (n_s_w h) = h /. (n_s_w h) by PARTFUN1:def_6;
A4: n_s_e h <= (n_s_e h) + 1 by NAT_1:11;
A5: h . (n_s_e h) = E-min (L~ h) by Def11;
A6: 1 <= n_s_e h by Def11;
(n_s_e h) + 1 <= len h by Def11;
then n_s_e h <= len h by A4, XXREAL_0:2;
then n_s_e h in dom h by A6, FINSEQ_3:25;
then A7: h . (n_s_e h) = h /. (n_s_e h) by PARTFUN1:def_6;
A8: h . (n_s_w h) = W-min (L~ h) by Def9;
thus n_s_w h <> n_s_e h ::_thesis: verum
proof
assume n_s_w h = n_s_e h ; ::_thesis: contradiction
then A9: W-bound (L~ h) = (h /. (n_s_e h)) `1 by A8, A3, EUCLID:52
.= E-bound (L~ h) by A5, A7, EUCLID:52 ;
A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;
then A11: (h /. 1) `1 >= W-bound (L~ h) by Th12;
consider ii being Element of NAT such that
A12: ii in dom h and
A13: (h /. ii) `1 <> (h /. 1) `1 by GOBOARD7:30;
A14: ii <= len h by A12, FINSEQ_3:25;
A15: 1 <= ii by A12, FINSEQ_3:25;
then A16: (h /. ii) `1 <= E-bound (L~ h) by A14, Th12;
A17: (h /. ii) `1 >= W-bound (L~ h) by A15, A14, Th12;
(h /. 1) `1 <= E-bound (L~ h) by A10, Th12;
then (h /. 1) `1 = W-bound (L~ h) by A9, A11, XXREAL_0:1;
hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum
end;
end;
theorem :: JORDAN5D:49
for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h
proof
let h be non constant standard special_circular_sequence; ::_thesis: n_e_n h <> n_e_s h
set i1 = n_e_n h;
set i2 = n_e_s h;
A1: n_e_n h <= (n_e_n h) + 1 by NAT_1:11;
A2: 1 <= n_e_n h by Def16;
(n_e_n h) + 1 <= len h by Def16;
then n_e_n h <= len h by A1, XXREAL_0:2;
then n_e_n h in dom h by A2, FINSEQ_3:25;
then A3: h . (n_e_n h) = h /. (n_e_n h) by PARTFUN1:def_6;
A4: n_e_s h <= (n_e_s h) + 1 by NAT_1:11;
A5: h . (n_e_s h) = S-max (L~ h) by Def14;
A6: 1 <= n_e_s h by Def14;
(n_e_s h) + 1 <= len h by Def14;
then n_e_s h <= len h by A4, XXREAL_0:2;
then n_e_s h in dom h by A6, FINSEQ_3:25;
then A7: h . (n_e_s h) = h /. (n_e_s h) by PARTFUN1:def_6;
A8: h . (n_e_n h) = N-max (L~ h) by Def16;
thus n_e_n h <> n_e_s h ::_thesis: verum
proof
assume n_e_n h = n_e_s h ; ::_thesis: contradiction
then A9: N-bound (L~ h) = (h /. (n_e_s h)) `2 by A8, A3, EUCLID:52
.= S-bound (L~ h) by A5, A7, EUCLID:52 ;
A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;
then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11;
consider ii being Element of NAT such that
A12: ii in dom h and
A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31;
A14: ii <= len h by A12, FINSEQ_3:25;
A15: 1 <= ii by A12, FINSEQ_3:25;
then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11;
A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11;
(h /. 1) `2 <= N-bound (L~ h) by A10, Th11;
then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1;
hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum
end;
end;
theorem :: JORDAN5D:50
for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h
proof
let h be non constant standard special_circular_sequence; ::_thesis: n_n_w h <> n_n_e h
set i1 = n_n_w h;
set i2 = n_n_e h;
A1: n_n_w h <= (n_n_w h) + 1 by NAT_1:11;
A2: 1 <= n_n_w h by Def10;
(n_n_w h) + 1 <= len h by Def10;
then n_n_w h <= len h by A1, XXREAL_0:2;
then n_n_w h in dom h by A2, FINSEQ_3:25;
then A3: h . (n_n_w h) = h /. (n_n_w h) by PARTFUN1:def_6;
A4: n_n_e h <= (n_n_e h) + 1 by NAT_1:11;
A5: h . (n_n_e h) = E-max (L~ h) by Def12;
A6: 1 <= n_n_e h by Def12;
(n_n_e h) + 1 <= len h by Def12;
then n_n_e h <= len h by A4, XXREAL_0:2;
then n_n_e h in dom h by A6, FINSEQ_3:25;
then A7: h . (n_n_e h) = h /. (n_n_e h) by PARTFUN1:def_6;
A8: h . (n_n_w h) = W-max (L~ h) by Def10;
thus n_n_w h <> n_n_e h ::_thesis: verum
proof
assume n_n_w h = n_n_e h ; ::_thesis: contradiction
then A9: W-bound (L~ h) = (h /. (n_n_e h)) `1 by A8, A3, EUCLID:52
.= E-bound (L~ h) by A5, A7, EUCLID:52 ;
A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;
then A11: (h /. 1) `1 >= W-bound (L~ h) by Th12;
consider ii being Element of NAT such that
A12: ii in dom h and
A13: (h /. ii) `1 <> (h /. 1) `1 by GOBOARD7:30;
A14: ii <= len h by A12, FINSEQ_3:25;
A15: 1 <= ii by A12, FINSEQ_3:25;
then A16: (h /. ii) `1 <= E-bound (L~ h) by A14, Th12;
A17: (h /. ii) `1 >= W-bound (L~ h) by A15, A14, Th12;
(h /. 1) `1 <= E-bound (L~ h) by A10, Th12;
then (h /. 1) `1 = W-bound (L~ h) by A9, A11, XXREAL_0:1;
hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum
end;
end;