:: Subsequences of Standard Special Circular Sequences in $ { \cal E} ^2_ { \rm T } $
:: by Yatsuka Nakamura , Roman Matuszewski and Adam Grabowski
::
:: Received May 12, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: JORDAN4:1
canceled;
theorem :: JORDAN4:2
canceled;
theorem :: JORDAN4:3
canceled;
theorem :: JORDAN4:4
canceled;
theorem :: JORDAN4:5
canceled;
theorem Th6: :: JORDAN4:6
theorem Th7: :: JORDAN4:7
theorem Th8: :: JORDAN4:8
theorem Th9: :: JORDAN4:9
theorem :: JORDAN4:10
canceled;
theorem :: JORDAN4:11
canceled;
theorem :: JORDAN4:12
canceled;
theorem :: JORDAN4:13
canceled;
theorem Th14: :: JORDAN4:14
theorem :: JORDAN4:15
canceled;
theorem :: JORDAN4:16
canceled;
theorem :: JORDAN4:17
canceled;
theorem Th18: :: JORDAN4:18
theorem Th19: :: JORDAN4:19
theorem Th20: :: JORDAN4:20
theorem Th21: :: JORDAN4:21
theorem Th22: :: JORDAN4:22
theorem Th23: :: JORDAN4:23
theorem Th24: :: JORDAN4:24
theorem Th25: :: JORDAN4:25
theorem :: JORDAN4:26
theorem Th27: :: JORDAN4:27
theorem Th28: :: JORDAN4:28
theorem Th29: :: JORDAN4:29
theorem Th30: :: JORDAN4:30
theorem Th31: :: JORDAN4:31
theorem Th32: :: JORDAN4:32
:: deftheorem Def1 defines S_Drop JORDAN4:def 1 :
theorem Th33: :: JORDAN4:33
theorem Th34: :: JORDAN4:34
theorem Th35: :: JORDAN4:35
:: deftheorem Def2 defines is_a_part>_of JORDAN4:def 2 :
:: deftheorem Def3 defines is_a_part<_of JORDAN4:def 3 :
:: deftheorem Def4 defines is_a_part_of JORDAN4:def 4 :
theorem :: JORDAN4:36
theorem Th37: :: JORDAN4:37
theorem Th38: :: JORDAN4:38
theorem Th39: :: JORDAN4:39
theorem Th40: :: JORDAN4:40
theorem Th41: :: JORDAN4:41
theorem Th42: :: JORDAN4:42
theorem Th43: :: JORDAN4:43
theorem Th44: :: JORDAN4:44
theorem Th45: :: JORDAN4:45
theorem Th46: :: JORDAN4:46
theorem Th47: :: JORDAN4:47
theorem Th48: :: JORDAN4:48
theorem Th49: :: JORDAN4:49
theorem Th50: :: JORDAN4:50
theorem Th51: :: JORDAN4:51
theorem Th52: :: JORDAN4:52
theorem Th53: :: JORDAN4:53
theorem Th54: :: JORDAN4:54
theorem Th55: :: JORDAN4:55
theorem Th56: :: JORDAN4:56
Lm1:
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
theorem :: JORDAN4:57
theorem Th58: :: JORDAN4:58
theorem Th59: :: JORDAN4:59
theorem Th60: :: JORDAN4:60
theorem :: JORDAN4:61
theorem Th62: :: JORDAN4:62
for
f being non
constant standard special_circular_sequence for
i1,
i2 being
Element of
NAT st 1
<= i1 &
i1 + 1
<= len f & 1
<= i2 &
i2 + 1
<= len f &
i1 <> i2 holds
ex
g1,
g2 being
FinSequence of
(TOP-REAL 2) st
(
g1 is_a_part_of f,
i1,
i2 &
g2 is_a_part_of f,
i1,
i2 &
(L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &
(L~ g1) \/ (L~ g2) = L~ f &
L~ g1 is_S-P_arc_joining f /. i1,
f /. i2 &
L~ g2 is_S-P_arc_joining f /. i1,
f /. i2 & ( for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = g1 or
g = g2 ) ) )
theorem :: JORDAN4:63
theorem Th64: :: JORDAN4:64
theorem Th65: :: JORDAN4:65
theorem Th66: :: JORDAN4:66
theorem Th67: :: JORDAN4:67
definition
let f be non
constant standard special_circular_sequence;
let i1,
i2 be
Element of
NAT ;
assume A1:
( 1
<= i1 &
i1 + 1
<= len f & 1
<= i2 &
i2 + 1
<= len f &
i1 <> i2 )
;
func Lower f,
i1,
i2 -> FinSequence of
(TOP-REAL 2) means :: JORDAN4:def 5
(
it is_a_part_of f,
i1,
i2 & ( (
(f /. (i1 + 1)) `1 < (f /. i1) `1 or
(f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies
it . 2
= f . (i1 + 1) ) & (
(f /. (i1 + 1)) `1 >= (f /. i1) `1 &
(f /. (i1 + 1)) `2 >= (f /. i1) `2 implies
it . 2
= f . (S_Drop (i1 -' 1),f) ) );
correctness
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) );
uniqueness
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) & b2 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b2 . 2 = f . (S_Drop (i1 -' 1),f) ) holds
b1 = b2;
func Upper f,
i1,
i2 -> FinSequence of
(TOP-REAL 2) means :: JORDAN4:def 6
(
it is_a_part_of f,
i1,
i2 & ( (
(f /. (i1 + 1)) `1 > (f /. i1) `1 or
(f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies
it . 2
= f . (i1 + 1) ) & (
(f /. (i1 + 1)) `1 <= (f /. i1) `1 &
(f /. (i1 + 1)) `2 <= (f /. i1) `2 implies
it . 2
= f . (S_Drop (i1 -' 1),f) ) );
correctness
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) );
uniqueness
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) & b2 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b2 . 2 = f . (S_Drop (i1 -' 1),f) ) holds
b1 = b2;
end;
:: deftheorem defines Lower JORDAN4:def 5 :
:: deftheorem defines Upper JORDAN4:def 6 :