ORDERS_5: About Quotient Orders and Ordering Sequences

proof end;

end;

:: into FINSEQ_2 ?
:: compare FINSEQ_2:32

registration

let A be set ;
let B be Subset of A;
let C be non empty set ;
let f be FinSequence of B;
let g be Function of A,C;

cluster f * g -> FinSequence-like ;

proof end;

end;

:: into FINSEQ_2 ?

registration

let s be FinSequence;

cluster (idseq (len s)) * s -> FinSequence-like ;

proof end;

end;

:: into FINSEQ_5 ?

registration

let s be FinSequence;

reduce Rev (Rev s) to s;

reducibility ;

end;

:: into FINSET_1 ?

scheme :: ORDERS_5:sch 1
Finite2{ F₁() -> set , F₂() -> Subset of F₁(), P₁[ set ] } :

P₁[F₁()]

provided

A1: F₁() is finite and
A2: P₁[F₂()] and
A3: for x, C being set st x in F₁() \ F₂() & F₂() c= C & C c= F₁() & P₁[C] holds
P₁[C \/ {x}]

proof end;

:: into STRUCT_0 ?
:: actually, I'm not sure why this redefinition is even needed by the analyzer

definition

let S, T be 1-sorted ;
let f be Function of S,T;
let B be Subset of S;
:: original: .:
redefine func f .: B -> Subset of T;
coherence by FUNCT_2:36;

end;

theorem :: ORDERS_5:4

canceled;

::$CT
:: into RVSUM_1 ?

theorem Th6: :: ORDERS_5:5

for s being FinSequence of REAL st Sum s <> 0 holds
ex i being Nat st
( i in dom s & s . i <> 0 )

proof end;

:: into RVSUM_1 ?
:: similar to RVSUM_1:85

theorem Th7: :: ORDERS_5:6

for s being FinSequence of REAL st s is nonnegative-yielding & ex i being Nat st
( i in dom s & s . i <> 0 ) holds
Sum s > 0

proof end;

:: into RVSUM_1 ?
:: used the preceeding proof to proof this one, which seemed to be both:
:: a good exercise and a demonstration of symmetry
:: However, a copy and paste proof would need less article references

theorem :: ORDERS_5:7

for s being FinSequence of REAL st s is nonpositive-yielding & ex i being Nat st
( i in dom s & s . i <> 0 ) holds
Sum s < 0

proof end;

:: into RFINSEQ ?

theorem Th9: :: ORDERS_5:8

for X being set
for s, t being FinSequence of X
for f being Function of X,REAL st s is one-to-one & t is one-to-one & rng t c= rng s & ( for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ) holds
Sum (f * s) = Sum (f * t)

proof end;

:: into PARTFUN3 ?

registration

let X be set ;
let f be Function;
let g be positive-yielding Function of X,REAL;

cluster f * g -> positive-yielding ;

proof end;

end;

:: into PARTFUN3 ?

registration

let X be set ;
let f be Function;
let g be negative-yielding Function of X,REAL;

cluster f * g -> negative-yielding ;

proof end;

end;

:: into PARTFUN3 ?

registration

let X be set ;
let f be Function;
let g be nonpositive-yielding Function of X,REAL;

cluster f * g -> nonpositive-yielding ;

proof end;

end;

:: into PARTFUN3 ?

registration

let X be set ;
let f be Function;
let g be nonnegative-yielding Function of X,REAL;

cluster f * g -> nonnegative-yielding ;

proof end;

end;

:: into PRE_POLY ?

definition

let s be Function;
:: original: support
redefine func support s -> Subset of (dom s);
coherence by PRE_POLY:37;

end;

::: into PRE_POLY ?

registration

let X be set ;

cluster Relation-like X -defined REAL -valued Function-like total quasi_total V53() V54() V55() nonnegative-yielding finite-support for Element of K16(K17(X,REAL));

proof end;

end;

::: into PRE_POLY ?

registration

let X be set ;

cluster Relation-like X -defined COMPLEX -valued Function-like total quasi_total V53() nonnegative-yielding finite-support for Element of K16(K17(X,COMPLEX));

proof end;

end;

:: into CFUNCT_1 ?

theorem Th10: :: ORDERS_5:9

for A being set
for f being Function of A,COMPLEX holds support f = support (- f)

proof end;

:: into CFUNCT_1 ?

registration

let A be set ;
let f be finite-support Function of A,COMPLEX;

cluster - f -> finite-support ;

proof end;

end;

:: into CFUNCT_1 as a consequence?

registration

let A be set ;
let f be finite-support Function of A,REAL;

cluster - f -> finite-support ;

proof end;

end;

theorem :: ORDERS_5:10

for X being set
for R being Relation
for Y being Subset of X st R is_irreflexive_in X holds
R is_irreflexive_in Y

proof end;

theorem :: ORDERS_5:11

for X being set
for R being Relation
for Y being Subset of X st R is_symmetric_in X holds
R is_symmetric_in Y

proof end;

theorem :: ORDERS_5:12

for X being set
for R being Relation
for Y being Subset of X st R is_asymmetric_in X holds
R is_asymmetric_in Y

proof end;

Th16: for X being set
for R being Relation
for Y being Subset of X st R is_connected_in X holds
R is_connected_in Y
by ORDERS_1:76;

definition

let A be RelStr ;

attr A is connected means :Def1: :: ORDERS_5:def 1
the InternalRel of A is_connected_in the carrier of A;

attr A is strongly_connected means :: ORDERS_5:def 2
the InternalRel of A is_strongly_connected_in the carrier of A;

end;

:: deftheorem Def1 defines connected ORDERS_5:def 1 :

:: deftheorem defines strongly_connected ORDERS_5:def 2 :

registration

cluster non empty strict total reflexive transitive antisymmetric connected strongly_connected for RelStr ;

proof end;

end;

registration

cluster strongly_connected -> reflexive connected for RelStr ;

proof end;

end;

registration

cluster reflexive connected -> strongly_connected for RelStr ;

proof end;

end;

registration

cluster empty -> reflexive transitive antisymmetric connected strongly_connected for RelStr ;

proof end;

end;

definition

let A be RelStr ;
let a1, a2 be Element of A;

pred a1 =~ a2 means :Def3: :: ORDERS_5:def 3
( a1 <= a2 & a2 <= a1 );

end;

:: deftheorem Def3 defines =~ ORDERS_5:def 3 :

theorem Th22: :: ORDERS_5:13

for A being non empty reflexive RelStr
for a being Element of A holds a =~ a

proof end;

definition

let A be non empty reflexive RelStr ;
let a1, a2 be Element of A;
:: original: =~
redefine pred a1 =~ a2;
reflexivity by Th22;

end;

definition

let A be RelStr ;
let a1, a2 be Element of A;

pred a1 <~ a2 means :: ORDERS_5:def 4
( a1 <= a2 & not a2 <= a1 );

irreflexivity ;

end;

:: deftheorem defines <~ ORDERS_5:def 4 :

notation

let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 >~ a1 for a1 <~ a2;

end;

definition

let A be connected RelStr ;
let a1, a2 be Element of A;
:: original: <~
redefine pred a1 <~ a2;
asymmetry ;

end;

theorem :: ORDERS_5:14

for A being non empty RelStr
for a1, a2 being Element of A holds
( not A is strongly_connected or a1 <~ a2 or a1 =~ a2 or a1 >~ a2 )

proof end;

theorem :: ORDERS_5:15

for A being transitive RelStr
for a1, a2, a3 being Element of A holds
( ( a1 <~ a2 & a2 <= a3 implies a1 <~ a3 ) & ( a1 <= a2 & a2 <~ a3 implies a1 <~ a3 ) ) by ORDERS_2:3;

theorem Th25: :: ORDERS_5:16

for A being non empty RelStr
for a1, a2 being Element of A holds
( not A is strongly_connected or a1 <= a2 or a2 <= a1 )

proof end;

theorem Th26: :: ORDERS_5:17

for A being non empty RelStr
for B being Subset of A
for a1, a2 being Element of A st the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2 & not a1 <= a2 holds
a2 <= a1

proof end;

theorem Th27: :: ORDERS_5:18

for A being non empty RelStr
for a1, a2 being Element of A st A is connected & a1 <> a2 & not a1 <= a2 holds
a2 <= a1

proof end;

theorem :: ORDERS_5:19

for A being non empty RelStr
for a1, a2 being Element of A holds
( not A is strongly_connected or a1 = a2 or a1 < a2 or a2 < a1 )

proof end;

theorem Th29: :: ORDERS_5:20

for A being RelStr
for a1, a2 being Element of A st a1 <= a2 holds
( a1 in the carrier of A & a2 in the carrier of A )

proof end;

theorem :: ORDERS_5:21

for A being RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not A is empty by Th29;

theorem Th31: :: ORDERS_5:22

for A being transitive RelStr
for B being finite Subset of A st not B is empty & the InternalRel of A is_connected_in B holds
ex x being Element of A st
( x in B & ( for y being Element of A st y in B & x <> y holds
x <= y ) )

proof end;

theorem :: ORDERS_5:23

for A being transitive connected RelStr
for B being finite Subset of A st not B is empty holds
ex x being Element of A st
( x in B & ( for y being Element of A st y in B & x <> y holds
x <= y ) )

proof end;

theorem Th33: :: ORDERS_5:24

proof end;

theorem :: ORDERS_5:25

for A being transitive connected RelStr
for B being finite Subset of A st not B is empty holds
ex x being Element of A st
( x in B & ( for y being Element of A st y in B & x <> y holds
y <= x ) )

proof end;

:: I repeated some definitions here to have them all in one place

definition

mode Preorder is reflexive transitive RelStr ;
mode LinearPreorder is transitive strongly_connected RelStr ;
mode Order is reflexive transitive antisymmetric RelStr ;
mode LinearOrder is transitive antisymmetric strongly_connected RelStr ;

end;

registration

cluster reflexive transitive -> quasi_ordered for RelStr ;

coherence by DICKSON:def 3;

end;

registration

cluster empty total reflexive transitive antisymmetric quasi_ordered connected strongly_connected for RelStr ;

proof end;

end;

theorem :: ORDERS_5:26

for A being Preorder holds the InternalRel of A quasi_orders the carrier of A

proof end;

theorem :: ORDERS_5:27

for A being Order holds the InternalRel of A partially_orders the carrier of A

proof end;

theorem Th37: :: ORDERS_5:28

for A being LinearOrder holds the InternalRel of A linearly_orders the carrier of A

proof end;

theorem :: ORDERS_5:29

for A being RelStr st the InternalRel of A quasi_orders the carrier of A holds
( A is reflexive & A is transitive ) by ORDERS_1:def 7, ORDERS_2:def 2, ORDERS_2:def 3;

theorem Th39: :: ORDERS_5:30

for A being RelStr st the InternalRel of A partially_orders the carrier of A holds
( A is reflexive & A is transitive & A is antisymmetric ) by ORDERS_1:def 8, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

theorem :: ORDERS_5:31

for A being RelStr st the InternalRel of A linearly_orders the carrier of A holds
( A is reflexive & A is transitive & A is antisymmetric & A is connected )

proof end;

scheme :: ORDERS_5:sch 2
RelStrMin{ F₁() -> transitive connected RelStr , F₂() -> finite Subset of F₁(), P₁[ Element of F₁()] } :

ex x being Element of F₁() st
( x in F₂() & P₁[x] & ( for y being Element of F₁() st y in F₂() & y <~ x holds
not P₁[y] ) )

provided

A1: ex x being Element of F₁() st
( x in F₂() & P₁[x] )

proof end;

scheme :: ORDERS_5:sch 3
RelStrMax{ F₁() -> transitive connected RelStr , F₂() -> finite Subset of F₁(), P₁[ Element of F₁()] } :

ex x being Element of F₁() st
( x in F₂() & P₁[x] & ( for y being Element of F₁() st y in F₂() & x <~ y holds
not P₁[y] ) )

provided

A1: ex x being Element of F₁() st
( x in F₂() & P₁[x] )

proof end;

definition

let A be Preorder;

func EqRelOf A -> Equivalence_Relation of the carrier of A means :Def6: :: ORDERS_5:def 6
for x, y being Element of A holds
( [x,y] in it iff ( x <= y & y <= x ) );

proof end;

proof end;

end;

:: deftheorem ORDERS_5:def 5 :

:: deftheorem Def6 defines EqRelOf ORDERS_5:def 6 :

theorem Th41: :: ORDERS_5:32

for A being Preorder holds EqRelOf A = EqRel A

proof end;

registration

let A be empty Preorder;

cluster EqRelOf A -> empty ;

end;

registration

let A be non empty Preorder;

cluster EqRelOf A -> non empty ;

end;

theorem Th42: :: ORDERS_5:33

for A being Order holds EqRelOf A = id the carrier of A

proof end;

definition

let A be Preorder;

func QuotientOrder A -> strict RelStr means :Def7: :: ORDERS_5:def 7
( the carrier of it = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds
( [X,Y] in the InternalRel of it iff ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines QuotientOrder ORDERS_5:def 7 :

registration

let A be empty Preorder;

cluster QuotientOrder A -> empty strict ;

proof end;

end;

theorem Th43: :: ORDERS_5:34

for A being non empty Preorder
for x being Element of A holds Class ((EqRelOf A),x) in the carrier of (QuotientOrder A)

proof end;

registration

let A be non empty Preorder;

cluster QuotientOrder A -> non empty strict ;

coherence by Th43;

end;

theorem Th44: :: ORDERS_5:35

for A being Preorder holds the InternalRel of (QuotientOrder A) = <=E A

proof end;

registration

let A be Preorder;

cluster QuotientOrder A -> strict total reflexive transitive antisymmetric ;

proof end;

end;

:: this generalizes DICKSON:10 to possibly empty RelStr

registration

let A be LinearPreorder;

cluster QuotientOrder A -> strict connected strongly_connected ;

proof end;

end;

definition

let A be Preorder;

func proj A -> Function of A,(QuotientOrder A) means :Def8: :: ORDERS_5:def 8
for x being Element of A holds it . x = Class ((EqRelOf A),x);

proof end;

proof end;

end;

:: deftheorem Def8 defines proj ORDERS_5:def 8 :

registration

let A be empty Preorder;

cluster proj A -> empty ;

end;

registration

let A be non empty Preorder;

cluster proj A -> non empty ;

end;

theorem Th45: :: ORDERS_5:36

for A being non empty Preorder
for x, y being Element of A st x <= y holds
(proj A) . x <= (proj A) . y

proof end;

theorem :: ORDERS_5:37

for A being Preorder
for x, y being Element of A st x =~ y holds
(proj A) . x = (proj A) . y

proof end;

definition

let A be Preorder;
let R be Equivalence_Relation of the carrier of A;

attr R is EqRelOf-like means :Def9: :: ORDERS_5:def 9
R = EqRelOf A;

end;

:: deftheorem Def9 defines EqRelOf-like ORDERS_5:def 9 :

registration

let A be Preorder;

cluster EqRelOf A -> EqRelOf-like ;

end;

registration

let A be Preorder;

cluster Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive EqRelOf-like for Element of K16(K17( the carrier of A, the carrier of A));

proof end;

end;

definition

let A be Preorder;
let R be EqRelOf-like Equivalence_Relation of the carrier of A;
let x be Element of A;
:: original: Im
redefine func Class (R,x) -> Element of (QuotientOrder A);
coherence

proof end;

end;

theorem Th47: :: ORDERS_5:38

for A being Preorder holds the carrier of (QuotientOrder A) is a_partition of the carrier of A

proof end;

theorem Th48: :: ORDERS_5:39

for A being non empty Preorder
for D being non empty a_partition of the carrier of A st D = the carrier of (QuotientOrder A) holds
proj A = proj D

proof end;

definition

let A be set ;
let D be a_partition of A;

func PreorderFromPartition D -> strict RelStr equals :: ORDERS_5:def 10
RelStr(# A,(ERl D) #);

end;

:: deftheorem defines PreorderFromPartition ORDERS_5:def 10 :

registration

let A be non empty set ;
let D be a_partition of A;

cluster PreorderFromPartition D -> non empty strict ;

end;

registration

let A be set ;
let D be a_partition of A;

cluster PreorderFromPartition D -> strict reflexive transitive ;

coherence ;

cluster PreorderFromPartition D -> strict symmetric ;

proof end;

end;

theorem Th49: :: ORDERS_5:40

for A being set
for D being a_partition of A holds ERl D = EqRelOf (PreorderFromPartition D)

proof end;

Def5: for A being set
for D being a_partition of A holds Class (ERl D) = D
by PARTIT1:38;

theorem Th50: :: ORDERS_5:41

for A being set
for D being a_partition of A holds D = Class (EqRelOf (PreorderFromPartition D))

proof end;

theorem Th51: :: ORDERS_5:42

for A being set
for D being a_partition of A holds D = the carrier of (QuotientOrder (PreorderFromPartition D))

proof end;

definition

let A be set ;
let D be a_partition of A;
let X be Element of D;
let f be Function;

func eqSupport (f,X) -> Subset of A equals :: ORDERS_5:def 11
(support f) /\ X;

proof end;

end;

:: deftheorem defines eqSupport ORDERS_5:def 11 :

definition

let A be Preorder;
let X be Element of (QuotientOrder A);
let f be Function;

func eqSupport (f,X) -> Subset of A means :Def12: :: ORDERS_5:def 12
ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of (QuotientOrder A) & Y = X & it = eqSupport (f,Y) );

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines eqSupport ORDERS_5:def 12 :

definition

let A be Preorder;
let X be Element of (QuotientOrder A);
let f be Function;

redefine func eqSupport (f,X) equals :: ORDERS_5:def 13
(support f) /\ X;

proof end;

end;

:: deftheorem defines eqSupport ORDERS_5:def 13 :

registration

let A be set ;
let D be a_partition of A;
let f be finite-support Function;
let X be Element of D;

cluster eqSupport (f,X) -> finite ;

end;

registration

let A be Preorder;
let f be finite-support Function;
let X be Element of (QuotientOrder A);

cluster eqSupport (f,X) -> finite ;

end;

registration

let A be Order;
let X be Element of the carrier of (QuotientOrder A);
let f be finite-support Function of A,REAL;

cluster eqSupport (f,X) -> trivial ;

proof end;

end;

theorem Th52: :: ORDERS_5:43

for A being set
for D being a_partition of A
for X being Element of D
for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

proof end;

theorem :: ORDERS_5:44

for A being Preorder
for X being Element of (QuotientOrder A)
for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

proof end;

definition

let A be set ;
let D be a_partition of A;
let f be finite-support Function of A,REAL;

func D eqSumOf f -> Function of D,REAL means :Def14: :: ORDERS_5:def 14
for X being Element of D st X in D holds
it . X = Sum (f * (canFS (eqSupport (f,X))));

proof end;

proof end;

end;

:: deftheorem Def14 defines eqSumOf ORDERS_5:def 14 :

definition

let A be Preorder;
let f be finite-support Function of A,REAL;

func eqSumOf f -> Function of (QuotientOrder A),REAL means :Def15: :: ORDERS_5:def 15
ex D being a_partition of the carrier of A st
( D = the carrier of (QuotientOrder A) & it = D eqSumOf f );

proof end;

uniqueness ;

end;

:: deftheorem Def15 defines eqSumOf ORDERS_5:def 15 :

definition

let A be Preorder;
let f be finite-support Function of A,REAL;

redefine func eqSumOf f means :Def16: :: ORDERS_5:def 16
for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds
it . X = Sum (f * (canFS (eqSupport (f,X))));

proof end;

end;

:: deftheorem Def16 defines eqSumOf ORDERS_5:def 16 :

theorem Th54: :: ORDERS_5:45

for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)

proof end;

theorem Th55: :: ORDERS_5:46

for A being Preorder
for f being finite-support Function of A,REAL holds eqSumOf (- f) = - (eqSumOf f)

proof end;

Th56: for A being set
for D being a_partition of A
for f being nonnegative-yielding finite-support Function of A,REAL holds D eqSumOf f is nonnegative-yielding

proof end;

registration

let A be Preorder;
let f be nonnegative-yielding finite-support Function of A,REAL;

cluster eqSumOf f -> nonnegative-yielding ;

proof end;

end;

registration

let A be set ;
let D be a_partition of A;
let f be nonnegative-yielding finite-support Function of A,REAL;

cluster D eqSumOf f -> nonnegative-yielding ;

coherence by Th56;

end;

theorem Th58: :: ORDERS_5:47

for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
D eqSumOf f is nonpositive-yielding

proof end;

theorem :: ORDERS_5:48

for A being Preorder
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
eqSumOf f is nonpositive-yielding

proof end;

theorem Th60: :: ORDERS_5:49

for A being Preorder
for f being finite-support Function of A,REAL
for x being Element of A st ( for y being Element of A st x =~ y holds
x = y ) holds
((eqSumOf f) * (proj A)) . x = f . x

proof end;

theorem Th61: :: ORDERS_5:50

for A being Order
for f being finite-support Function of A,REAL holds (eqSumOf f) * (proj A) = f

proof end;

theorem :: ORDERS_5:51

for A being Order
for f1, f2 being finite-support Function of A,REAL st eqSumOf f1 = eqSumOf f2 holds
f1 = f2

proof end;

theorem Th63: :: ORDERS_5:52

for A being Preorder
for f being finite-support Function of A,REAL holds support (eqSumOf f) c= (proj A) .: (support f)

proof end;

theorem Th64: :: ORDERS_5:53

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL holds support (D eqSumOf f) c= (proj D) .: (support f)

proof end;

:: more general:
:: for x holds (for y in (proj A).x holds f.y >= 0) or
:: (for y in (proj A).x holds f.y <= 0)

theorem Th65: :: ORDERS_5:54

for A being Preorder
for f being finite-support Function of A,REAL st f is nonnegative-yielding holds
(proj A) .: (support f) = support (eqSumOf f)

proof end;

theorem :: ORDERS_5:55

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL st f is nonnegative-yielding holds
(proj D) .: (support f) = support (D eqSumOf f)

proof end;

theorem Th67: :: ORDERS_5:56

for A being Preorder
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
(proj A) .: (support f) = support (eqSumOf f)

proof end;

theorem :: ORDERS_5:57

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
(proj D) .: (support f) = support (D eqSumOf f)

proof end;

registration

let A be Preorder;
let f be finite-support Function of A,REAL;

cluster eqSumOf f -> finite-support ;

proof end;

end;

registration

let A be set ;
let D be a_partition of A;
let f be finite-support Function of A,REAL;

cluster D eqSumOf f -> finite-support ;

proof end;

end;

theorem Th69: :: ORDERS_5:58

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

proof end;

theorem Th70: :: ORDERS_5:59

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s1 = support f & rng s2 = support (D eqSumOf f) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)

proof end;

theorem :: ORDERS_5:60

for A being Preorder
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds
Sum ((eqSumOf f) * s2) = Sum (f * s1)

proof end;

definition

let A be RelStr ;
let s be FinSequence of A;

attr s is weakly-ascending means :: ORDERS_5:def 17
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <= s /. m;

end;

:: deftheorem defines weakly-ascending ORDERS_5:def 17 :

definition

let A be RelStr ;
let s be FinSequence of A;

attr s is ascending means :: ORDERS_5:def 18
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <~ s /. m;

end;

:: deftheorem defines ascending ORDERS_5:def 18 :

:: it is surprising that this isn't a trivial proof by Def4

registration

let A be RelStr ;

cluster ascending -> weakly-ascending for FinSequence of the carrier of A;

proof end;

end;

definition

let A be antisymmetric RelStr ;
let s be FinSequence of A;

redefine attr s is ascending means :Def19: :: ORDERS_5:def 19
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n < s /. m;

proof end;

end;

:: deftheorem Def19 defines ascending ORDERS_5:def 19 :

definition

let A be RelStr ;
let s be FinSequence of A;

attr s is weakly-descending means :: ORDERS_5:def 20
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m <= s /. n;

end;

:: deftheorem defines weakly-descending ORDERS_5:def 20 :

definition

let A be RelStr ;
let s be FinSequence of A;

attr s is descending means :: ORDERS_5:def 21
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m <~ s /. n;

end;

:: deftheorem defines descending ORDERS_5:def 21 :

registration

let A be RelStr ;

cluster descending -> weakly-descending for FinSequence of the carrier of A;

proof end;

end;

definition

let A be antisymmetric RelStr ;
let s be FinSequence of A;

redefine attr s is descending means :: ORDERS_5:def 22
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m < s /. n;

proof end;

end;

:: deftheorem defines descending ORDERS_5:def 22 :

registration

let A be antisymmetric RelStr ;

cluster one-to-one weakly-ascending -> ascending for FinSequence of the carrier of A;

proof end;

cluster one-to-one weakly-descending -> descending for FinSequence of the carrier of A;

proof end;

end;

registration

let A be antisymmetric RelStr ;

cluster weakly-ascending weakly-descending -> constant for FinSequence of the carrier of A;

proof end;

end;

registration

let A be reflexive RelStr ;

cluster constant -> weakly-ascending weakly-descending for FinSequence of the carrier of A;

proof end;

end;

registration

let A be RelStr ;

cluster <*> the carrier of A -> weakly-ascending ascending weakly-descending descending ;

end;

registration

let A be RelStr ;

cluster Relation-like NAT -defined the carrier of A -valued empty Function-like finite FinSequence-like FinSubsequence-like finite-support weakly-ascending ascending weakly-descending descending for FinSequence of the carrier of A;

proof end;

end;

Th72: for A being non empty RelStr
for x being Element of A holds
( <*x*> is ascending & <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )

proof end;

registration

let A be non empty RelStr ;
let x be Element of A;

cluster <*x*> -> weakly-ascending ascending weakly-descending descending for FinSequence of A;

coherence by Th72;

end;

registration

let A be non empty RelStr ;

cluster Relation-like NAT -defined the carrier of A -valued non empty Function-like one-to-one finite FinSequence-like FinSubsequence-like finite-support weakly-ascending ascending weakly-descending descending for FinSequence of the carrier of A;

proof end;

end;

definition

let A be RelStr ;
let s be FinSequence of A;

attr s is asc_ordering means :: ORDERS_5:def 23
( s is one-to-one & s is weakly-ascending );

attr s is desc_ordering means :: ORDERS_5:def 24
( s is one-to-one & s is weakly-descending );

end;

:: deftheorem defines asc_ordering ORDERS_5:def 23 :

:: deftheorem defines desc_ordering ORDERS_5:def 24 :

registration

let A be RelStr ;

cluster asc_ordering -> one-to-one weakly-ascending for FinSequence of the carrier of A;

coherence ;

cluster one-to-one weakly-ascending -> asc_ordering for FinSequence of the carrier of A;

coherence ;

cluster desc_ordering -> one-to-one weakly-descending for FinSequence of the carrier of A;

coherence ;

cluster one-to-one weakly-descending -> desc_ordering for FinSequence of the carrier of A;

end;

:: I thought the following registration would only work with trasitivity
:: but apparently ascending implies asc_ordering

registration

let A be RelStr ;

cluster ascending -> asc_ordering for FinSequence of the carrier of A;

proof end;

cluster descending -> desc_ordering for FinSequence of the carrier of A;

proof end;

end;

definition

let A be RelStr ;
let B be Subset of A;
let s be FinSequence of A;

attr s is B -asc_ordering means :: ORDERS_5:def 25
( s is asc_ordering & rng s = B );

attr s is B -desc_ordering means :: ORDERS_5:def 26
( s is desc_ordering & rng s = B );

end;

:: deftheorem defines -asc_ordering ORDERS_5:def 25 :

:: deftheorem defines -desc_ordering ORDERS_5:def 26 :

registration

let A be RelStr ;
let B be Subset of A;

cluster B -asc_ordering -> asc_ordering for FinSequence of the carrier of A;

coherence ;

cluster B -desc_ordering -> desc_ordering for FinSequence of the carrier of A;

end;

registration

let A be RelStr ;
let B be empty Subset of A;

cluster B -asc_ordering -> empty for FinSequence of the carrier of A;

coherence ;

cluster B -desc_ordering -> empty for FinSequence of the carrier of A;

end;

theorem Th73: :: ORDERS_5:61

for A being RelStr
for s being FinSequence of A holds
( s is weakly-ascending iff Rev s is weakly-descending )

proof end;

theorem :: ORDERS_5:62

for A being RelStr
for s being FinSequence of A holds
( s is ascending iff Rev s is descending )

proof end;

theorem Th75: :: ORDERS_5:63

for A being RelStr
for B being Subset of A
for s being FinSequence of A holds
( s is B -asc_ordering iff Rev s is B -desc_ordering )

proof end;

:: this seems trivial, I'm unsure why

theorem :: ORDERS_5:64

for A being RelStr
for B being Subset of A
for s being FinSequence of A st ( s is B -asc_ordering or s is B -desc_ordering ) holds
B is finite ;

registration

let A be antisymmetric RelStr ;

cluster asc_ordering -> ascending for FinSequence of the carrier of A;

coherence ;

cluster desc_ordering -> descending for FinSequence of the carrier of A;