environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, NAT_1, ARYTM_3, INT_1, CARD_1, ARYTM_1, XXREAL_0, RELAT_1, XBOOLE_0, FINSEQ_1, FINSEQ_6, FUNCT_1, PARTFUN1, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, FINSEQ_5, RLTOPSP1, GOBOARD5, ORDINAL4, TARSKI, PRE_TOPC, SUPINF_2, TOPREAL4, TOPREAL2, MCART_1, JORDAN4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2, TOPREAL4, GOBOARD5, PRE_TOPC, RLVECT_1, RLTOPSP1, EUCLID, FINSEQ_6, RFINSEQ, XXREAL_0;
definitions TARSKI;
theorems TARSKI, JORDAN3, TOPREAL4, TOPREAL1, TOPREAL2, FUNCT_1, SPPOL_1, GOBOARD5, FINSEQ_1, GOBOARD7, NAT_1, SPPOL_2, FINSEQ_3, FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6, ENUMSET1, ZFMISC_1, TOPREAL3, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, NAT_D, CARD_1, XREAL_0, RLTOPSP1, RLVECT_4, RLVECT_1;
schemes ;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, EUCLID, SPPOL_2, GOBOARD5, NAT_1, FINSEQ_1, CARD_1, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, RFINSEQ, BINARITH, FINSEQ_5, TOPREAL2, TOPREAL4, GOBOARD5, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLTOPSP1, RLVECT_1;
expansions ;
Lm1:
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 Th50:
for
f being non
constant standard special_circular_sequence for
i1,
i2 being
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 ) ) )
definition
let f be non
constant standard special_circular_sequence;
let i1,
i2 be
Element of
NAT ;
assume that A1:
1
<= i1
and A2:
i1 + 1
<= len f
and A3:
1
<= i2
and A4:
i2 + 1
<= len f
and A5:
i1 <> i2
;
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;
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;