:: Bounding Boxes for Special Sequences in ${\calE}^2$
:: by Yatsuka Nakamura and Adam Grabowski
::
:: Received June 8, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: JORDAN5D:1
canceled;
theorem :: JORDAN5D:2
canceled;
theorem Th3: :: JORDAN5D:3
theorem Th4: :: JORDAN5D:4
theorem Th5: :: JORDAN5D:5
theorem Th6: :: JORDAN5D:6
theorem Th7: :: JORDAN5D:7
theorem Th8: :: JORDAN5D:8
theorem Th9: :: JORDAN5D:9
theorem Th10: :: JORDAN5D:10
theorem Th11: :: JORDAN5D:11
theorem Th12: :: JORDAN5D:12
theorem Th13: :: JORDAN5D:13
theorem Th14: :: JORDAN5D:14
theorem Th15: :: JORDAN5D:15
theorem Th16: :: JORDAN5D:16
theorem Th17: :: JORDAN5D:17
theorem Th18: :: JORDAN5D:18
theorem Th19: :: JORDAN5D:19
theorem Th20: :: JORDAN5D:20
theorem :: JORDAN5D:21
theorem :: JORDAN5D:22
theorem :: JORDAN5D:23
theorem :: JORDAN5D:24
theorem :: JORDAN5D:25
theorem :: JORDAN5D:26
theorem :: JORDAN5D:27
theorem :: JORDAN5D:28
theorem :: JORDAN5D:29
theorem :: JORDAN5D:30
theorem :: JORDAN5D:31
theorem :: JORDAN5D:32
theorem Th33: :: JORDAN5D:33
theorem Th34: :: JORDAN5D:34
theorem Th35: :: JORDAN5D:35
theorem Th36: :: JORDAN5D:36
theorem Th37: :: JORDAN5D:37
theorem Th38: :: JORDAN5D:38
theorem Th39: :: JORDAN5D:39
theorem Th40: :: JORDAN5D:40
theorem Th41: :: JORDAN5D:41
theorem Th42: :: JORDAN5D:42
theorem Th43: :: JORDAN5D:43
theorem Th44: :: JORDAN5D:44
theorem Th45: :: JORDAN5D:45
theorem Th46: :: JORDAN5D:46
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
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
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
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
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
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
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
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
Lm9:
for h being non constant standard special_circular_sequence holds len h >= 2
by GOBOARD7:36, XXREAL_0:2;
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) )
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:21;
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) )
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:21;
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) )
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:21;
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) )
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:21;
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) )
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:21;
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) )
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:21;
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) )
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:21;
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) )
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: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
theorem :: JORDAN5D:48
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
:: 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
theorem :: JORDAN5D:50
theorem :: JORDAN5D:51
theorem :: JORDAN5D:52