:: JORDAN5D semantic presentation

theorem :: JORDAN5D:1

canceled;

theorem :: JORDAN5D:2

canceled;

theorem Th3: :: JORDAN5D:3

for n being Nat
for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg h,((len h) -' 1)

proof end;

theorem Th4: :: JORDAN5D:4

for i being Nat st 3 <= i holds
i mod (i -' 1) = 1

proof end;

theorem Th5: :: JORDAN5D:5

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 Nat st
( 1 <= i & i + 1 <= len h & h . i = p )

proof end;

theorem Th6: :: JORDAN5D:6

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 end;

theorem Th7: :: JORDAN5D:7

for h being non constant standard special_circular_sequence
for i, I being 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 end;

theorem Th8: :: JORDAN5D:8

for h being non constant standard special_circular_sequence
for i, I being 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 end;

theorem Th9: :: JORDAN5D:9

for f being non empty FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i <= len (GoB f) holds
ex k, j being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * i,j )

proof end;

theorem Th10: :: JORDAN5D:10

for f being non empty FinSequence of (TOP-REAL 2)
for j being Nat st 1 <= j & j <= width (GoB f) holds
ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * i,j )

proof end;

theorem Th11: :: JORDAN5D:11

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * i,j) `1 )

proof end;

theorem Th12: :: JORDAN5D:12

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * i,j) `2 )

proof end;

theorem Th13: :: JORDAN5D:13

for h being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i <= len h holds
( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

proof end;

theorem Th14: :: JORDAN5D:14

for h being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i <= len h holds
( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )

proof end;

theorem Th15: :: JORDAN5D:15

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 end;

theorem Th16: :: JORDAN5D:16

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 end;

theorem Th17: :: JORDAN5D:17

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 end;

theorem Th18: :: JORDAN5D:18

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 end;

theorem Th19: :: JORDAN5D:19

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 end;

theorem Th20: :: JORDAN5D:20

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 end;

theorem Th21: :: 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 = W-bound (L~ h) & q in L~ h ) } holds
lower_bound X = inf (proj2 || (W-most (L~ h)))

proof end;

theorem Th22: :: 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 = W-bound (L~ h) & q in L~ h ) } holds
upper_bound X = sup (proj2 || (W-most (L~ h)))

proof end;

theorem Th23: :: JORDAN5D:23

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 = inf (proj2 || (E-most (L~ h)))

proof end;

theorem Th24: :: JORDAN5D:24

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 = sup (proj2 || (E-most (L~ h)))

proof end;

theorem Th25: :: JORDAN5D:25

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 = inf (proj1 || (L~ g))

proof end;

theorem Th26: :: 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 = S-bound (L~ h) & q in L~ h ) } holds
lower_bound X = inf (proj1 || (S-most (L~ h)))

proof end;

theorem Th27: :: 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 = S-bound (L~ h) & q in L~ h ) } holds
upper_bound X = sup (proj1 || (S-most (L~ h)))

proof end;

theorem Th28: :: JORDAN5D:28

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 = inf (proj1 || (N-most (L~ h)))

proof end;

theorem Th29: :: JORDAN5D:29

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 = sup (proj1 || (N-most (L~ h)))

proof end;

theorem Th30: :: 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
lower_bound X = inf (proj2 || (L~ g))

proof end;

theorem Th31: :: JORDAN5D:31

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 = sup (proj1 || (L~ g))

proof end;

theorem Th32: :: JORDAN5D:32

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 = sup (proj2 || (L~ g))

proof 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 Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds
((GoB h) * 1,I) `1 <= p `1

proof 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 Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds
p `1 <= ((GoB h) * (len (GoB h)),I) `1

proof end;

theorem Th35: :: JORDAN5D:35

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= len (GoB h) holds
((GoB h) * I,1) `2 <= p `2

proof end;

theorem Th36: :: JORDAN5D:36

for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= len (GoB h) holds
p `2 <= ((GoB h) * I,(width (GoB h))) `2

proof end;

theorem Th37: :: JORDAN5D:37

for h being non constant standard special_circular_sequence
for i, j being 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 end;

theorem Th38: :: JORDAN5D:38

for h being non constant standard special_circular_sequence
for i, j being 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 end;

theorem Th39: :: JORDAN5D:39

for h being non constant standard special_circular_sequence holds W-bound (L~ h) = ((GoB h) * 1,1) `1

proof end;

theorem Th40: :: JORDAN5D:40

for h being non constant standard special_circular_sequence holds S-bound (L~ h) = ((GoB h) * 1,1) `2

proof end;

theorem Th41: :: JORDAN5D:41

for h being non constant standard special_circular_sequence holds E-bound (L~ h) = ((GoB h) * (len (GoB h)),1) `1

proof end;

theorem Th42: :: JORDAN5D:42

for h being non constant standard special_circular_sequence holds N-bound (L~ h) = ((GoB h) * 1,(width (GoB h))) `2

proof end;

theorem Th43: :: JORDAN5D:43

for f being non empty FinSequence of (TOP-REAL 2)
for i, I, i1 being 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 Nat : ( [I,j] in Indices (GoB f) & ex k being 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 end;

theorem Th44: :: JORDAN5D:44

for h being non constant standard special_circular_sequence
for i, I, i1 being 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 Nat : ( [j,I] in Indices (GoB h) & ex k being 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 end;

theorem Th45: :: JORDAN5D:45

proof end;

theorem Th46: :: JORDAN5D:46

proof end;

Lm1: for i1 being 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 Nat : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y holds
((GoB h) * 1,i1) `2 <= p `2

proof end;

Lm2: for i1 being 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 Nat : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = max Y holds
((GoB h) * 1,i1) `2 >= p `2

proof end;

Lm3: for i1 being 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 Nat : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being 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 end;

Lm4: for i1 being 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 Nat : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being 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 end;

Lm5: for i1 being 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 Nat : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * j,1 ) ) } & i1 = min Y holds
((GoB h) * i1,1) `1 <= p `1

proof end;

Lm6: for i1 being 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 Nat : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being 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 end;

Lm7: for h being non constant standard special_circular_sequence
for i1 being 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 Nat : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * j,1 ) ) } & i1 = max Y holds
((GoB h) * i1,1) `1 >= p `1

proof end;

Lm8: for h being non constant standard special_circular_sequence
for i1 being 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 Nat : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being 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 end;

Lm9: for h being non constant standard special_circular_sequence holds len h >= 2

proof end;

definition

let g be non constant standard special_circular_sequence;
func i_s_w g -> Nat means :Def1: :: JORDAN5D:def 1
( [1,it] in Indices (GoB g) & (GoB g) * 1,it = W-min (L~ g) );
existence

proof end;

uniqueness by GOBOARD1:21;
func i_n_w g -> Nat means :Def2: :: JORDAN5D:def 2
( [1,it] in Indices (GoB g) & (GoB g) * 1,it = W-max (L~ g) );
existence

proof end;

uniqueness by GOBOARD1:21;
func i_s_e g -> 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

proof end;

uniqueness by GOBOARD1:21;
func i_n_e g -> 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

proof end;

uniqueness by GOBOARD1:21;
func i_w_s g -> Nat means :Def5: :: JORDAN5D:def 5
( [it,1] in Indices (GoB g) & (GoB g) * it,1 = S-min (L~ g) );
existence

proof end;

uniqueness by GOBOARD1:21;
func i_e_s g -> Nat means :Def6: :: JORDAN5D:def 6
( [it,1] in Indices (GoB g) & (GoB g) * it,1 = S-max (L~ g) );
existence

proof end;

uniqueness by GOBOARD1:21;
func i_w_n g -> 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

proof end;

uniqueness by GOBOARD1:21;
func i_e_n g -> 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

proof end;

uniqueness by GOBOARD1:21;

end;

:: deftheorem Def1 defines i_s_w JORDAN5D:def 1 :

:: deftheorem Def2 defines i_n_w JORDAN5D:def 2 :

:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :

:: deftheorem Def4 defines i_n_e JORDAN5D:def 4 :

:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :

:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :

:: deftheorem Def7 defines i_w_n JORDAN5D:def 7 :

:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :

theorem :: JORDAN5D:47

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 end;

theorem :: JORDAN5D:48

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 end;

Lm10: for h being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds
i1 = i2

proof end;

definition

let g be non constant standard special_circular_sequence;
func n_s_w g -> Nat means :Def9: :: JORDAN5D:def 9
( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_n_w g -> Nat means :Def10: :: JORDAN5D:def 10
( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_s_e g -> Nat means :Def11: :: JORDAN5D:def 11
( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_n_e g -> Nat means :Def12: :: JORDAN5D:def 12
( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_w_s g -> Nat means :Def13: :: JORDAN5D:def 13
( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_e_s g -> Nat means :Def14: :: JORDAN5D:def 14
( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_w_n g -> Nat means :Def15: :: JORDAN5D:def 15
( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) );
existence

proof end;

uniqueness by Lm10;
func n_e_n g -> Nat means :Def16: :: JORDAN5D:def 16
( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) );
existence

proof end;

uniqueness by Lm10;

end;

:: deftheorem Def9 defines n_s_w JORDAN5D:def 9 :

:: deftheorem Def10 defines n_n_w JORDAN5D:def 10 :

:: deftheorem Def11 defines n_s_e JORDAN5D:def 11 :

:: deftheorem Def12 defines n_n_e JORDAN5D:def 12 :

:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :

:: deftheorem Def14 defines n_e_s JORDAN5D:def 14 :

:: deftheorem Def15 defines n_w_n JORDAN5D:def 15 :

:: deftheorem Def16 defines n_e_n JORDAN5D:def 16 :

theorem :: JORDAN5D:49

for h being non constant standard special_circular_sequence holds n_w_n h <> n_w_s h

proof end;

theorem :: JORDAN5D:50

for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h

proof end;

theorem :: JORDAN5D:51

for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h

proof end;

theorem :: JORDAN5D:52

for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h

proof end;