:: About Quotient Orders and Ordering Sequences
:: by Sebastian Koch
::
:: Copyright (c) 2017-2021 Association of Mizar Users

:: into SUBSET_1 ?
theorem Th1: :: ORDERS_5:1
for A, B being set
for x being object st A = B \ {x} & x in B holds
B \ A = {x}
proof end;

:: into RELAT_1 ? present in FOMODEL0
registration
let Y be set ;
let X be Subset of Y;
coherence
for b1 being Relation st b1 is X -defined holds
b1 is Y -defined
by RELAT_1:182;
end;

:: placement in CARD_2 also seems appropriate because of CARD_2:60
theorem Th2: :: ORDERS_5:2
for X being set
for x being object st x in X & card X = 1 holds
{x} = X
proof end;

:: into FINSEQ_1 ?
:: interesting enough, trivdemo didn't recognized this one as trivial
theorem :: ORDERS_5:3
for X being set
for k being Nat st X c= Seg k holds
rng (Sgm X) c= Seg k
proof end;

:: into FINSEQ_1 ?
registration
let s be FinSequence;
let N be Subset of (dom s);
cluster (Sgm N) * s -> FinSequence-like ;
coherence
s * (Sgm N) is FinSequence-like
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;
coherence
proof end;
end;

:: into FINSEQ_2 ?
registration
let s be FinSequence;
cluster (idseq (len s)) * s -> FinSequence-like ;
coherence
s * (idseq (len s)) is FinSequence-like
proof end;
end;

:: into FINSEQ_5 ?
registration
let s be FinSequence;
reduce Rev (Rev s) to s;
reducibility
Rev (Rev s) = s
;
end;

:: into FINSET_1 ?
scheme :: ORDERS_5:sch 1
Finite2{ F1() -> set , F2() -> Subset of F1(), P1[ set ] } :
P1[F1()]
provided
A1: F1() is finite and
A2: P1[F2()] and
A3: for x, C being set st x in F1() \ F2() & F2() c= C & C c= F1() & P1[C] holds
P1[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
f .: B is Subset of T
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;
coherence
proof end;
end;

:: into PARTFUN3 ?
registration
let X be set ;
let f be Function;
let g be negative-yielding Function of X,REAL;
coherence
proof end;
end;

:: into PARTFUN3 ?
registration
let X be set ;
let f be Function;
let g be nonpositive-yielding Function of X,REAL;
coherence
proof end;
end;

:: into PARTFUN3 ?
registration
let X be set ;
let f be Function;
let g be nonnegative-yielding Function of X,REAL;
coherence
proof end;
end;

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

::: into PRE_POLY ?
registration
let X be set ;
existence
ex b1 being Function of X,REAL st
( b1 is finite-support & b1 is nonnegative-yielding )
proof end;
end;

::: into PRE_POLY ?
registration
let X be set ;
existence
ex b1 being Function of X,COMPLEX st
( b1 is nonnegative-yielding & b1 is finite-support )
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;
coherence
proof end;
end;

:: into CFUNCT_1 as a consequence?
registration
let A be set ;
let f be finite-support Function of A,REAL;
coherence
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 :
for A being RelStr holds
( A is connected iff the InternalRel of A is_connected_in the carrier of A );

:: deftheorem defines strongly_connected ORDERS_5:def 2 :
for A being RelStr holds
( A is strongly_connected iff the InternalRel of A is_strongly_connected_in the carrier of A );

registration
existence
ex b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is strongly_connected & b1 is strict & b1 is total )
proof end;
end;

registration
coherence
for b1 being RelStr st b1 is strongly_connected holds
( b1 is reflexive & b1 is connected )
proof end;
end;

registration
coherence
for b1 being RelStr st b1 is reflexive & b1 is connected holds
b1 is strongly_connected
proof end;
end;

registration
coherence
for b1 being RelStr st b1 is empty holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive & b1 is connected & b1 is strongly_connected )
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 :
for A being RelStr
for a1, a2 being Element of A holds
( a1 =~ a2 iff ( a1 <= a2 & a2 <= a1 ) );

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
for a1 being Element of A holds (A,b1,b1)
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
for a1 being Element of A holds
( not a1 <= a1 or a1 <= a1 )
;
end;

:: deftheorem defines <~ ORDERS_5:def 4 :
for A being RelStr
for a1, a2 being Element of A holds
( a1 <~ a2 iff ( a1 <= a2 & not a2 <= a1 ) );

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
for a1, a2 being Element of A st (A,b1,b2) holds
not (A,b2,b1)
;
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
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
y <= x ) )
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 end;

registration
coherence
for b1 being Preorder holds b1 is quasi_ordered
by DICKSON:def 3;
end;

registration
existence
ex b1 being LinearOrder st b1 is empty
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 ;

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 ;

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{ F1() -> transitive connected RelStr , F2() -> finite Subset of F1(), P1[ Element of F1()] } :
ex x being Element of F1() st
( x in F2() & P1[x] & ( for y being Element of F1() st y in F2() & y <~ x holds
not P1[y] ) )
provided
A1: ex x being Element of F1() st
( x in F2() & P1[x] )
proof end;

scheme :: ORDERS_5:sch 3
RelStrMax{ F1() -> transitive connected RelStr , F2() -> finite Subset of F1(), P1[ Element of F1()] } :
ex x being Element of F1() st
( x in F2() & P1[x] & ( for y being Element of F1() st y in F2() & x <~ y holds
not P1[y] ) )
provided
A1: ex x being Element of F1() st
( x in F2() & P1[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 ) );
existence
ex b1 being Equivalence_Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b1 iff ( x <= y & y <= x ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b1 iff ( x <= y & y <= x ) ) ) & ( for x, y being Element of A holds
( [x,y] in b2 iff ( x <= y & y <= x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem ORDERS_5:def 5 :
canceled;

:: deftheorem Def6 defines EqRelOf ORDERS_5:def 6 :
for A being Preorder
for b2 being Equivalence_Relation of the carrier of A holds
( b2 = EqRelOf A iff for x, y being Element of A holds
( [x,y] in b2 iff ( x <= y & y <= x ) ) );

theorem Th41: :: ORDERS_5:32
for A being Preorder holds EqRelOf A = EqRel A
proof end;

registration
let A be empty Preorder;
coherence
EqRelOf A is empty
;
end;

registration
let A be non empty Preorder;
cluster EqRelOf A -> non empty ;
coherence
not EqRelOf A is 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 () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of it iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of b1 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of b1 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) & the carrier of b2 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of b2 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines QuotientOrder ORDERS_5:def 7 :
for A being Preorder
for b2 being strict RelStr holds
( b2 = QuotientOrder A iff ( the carrier of b2 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of b2 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) ) );

registration
let A be empty Preorder;
coherence
proof end;
end;

theorem Th43: :: ORDERS_5:34
for A being non empty Preorder
for x being Element of A holds Class ((),x) in the carrier of ()
proof end;

registration
let A be non empty Preorder;
coherence
not QuotientOrder A is empty
by Th43;
end;

theorem Th44: :: ORDERS_5:35
for A being Preorder holds the InternalRel of () = <=E A
proof end;

registration
let A be Preorder;
coherence
proof end;
end;

:: this generalizes DICKSON:10 to possibly empty RelStr
registration
let A be LinearPreorder;
coherence
proof end;
end;

definition
let A be Preorder;
func proj A -> Function of A,() means :Def8: :: ORDERS_5:def 8
for x being Element of A holds it . x = Class ((),x);
existence
ex b1 being Function of A,() st
for x being Element of A holds b1 . x = Class ((),x)
proof end;
uniqueness
for b1, b2 being Function of A,() st ( for x being Element of A holds b1 . x = Class ((),x) ) & ( for x being Element of A holds b2 . x = Class ((),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines proj ORDERS_5:def 8 :
for A being Preorder
for b2 being Function of A,() holds
( b2 = proj A iff for x being Element of A holds b2 . x = Class ((),x) );

registration
let A be empty Preorder;
cluster proj A -> empty ;
coherence
proj A is empty
;
end;

registration
let A be non empty Preorder;
cluster proj A -> non empty ;
coherence
not proj A is 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 :
for A being Preorder
for R being Equivalence_Relation of the carrier of A holds
( R is EqRelOf-like iff R = EqRelOf A );

registration
let A be Preorder;
correctness
coherence ;
;
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));
existence
ex b1 being Equivalence_Relation of the carrier of A st b1 is EqRelOf-like
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 ();
coherence
Im (R,x) is Element of ()
proof end;
end;

theorem Th47: :: ORDERS_5:38
for A being Preorder holds the carrier of () 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 () 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) #);
correctness
coherence
RelStr(# A,(ERl D) #) is strict RelStr
;
;
end;

:: deftheorem defines PreorderFromPartition ORDERS_5:def 10 :
for A being set
for D being a_partition of A holds PreorderFromPartition D = RelStr(# A,(ERl D) #);

registration
let A be non empty set ;
let D be a_partition of A;
coherence ;
end;

registration
let A be set ;
let D be a_partition of A;
coherence ;
coherence
proof end;
end;

theorem Th49: :: ORDERS_5:40
for A being set
for D being a_partition of A holds ERl D = EqRelOf
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 ()
proof end;

theorem Th51: :: ORDERS_5:42
for A being set
for D being a_partition of A holds D = the carrier of
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
() /\ X;
correctness
coherence
() /\ X is Subset of A
;
proof end;
end;

:: deftheorem defines eqSupport ORDERS_5:def 11 :
for A being set
for D being a_partition of A
for X being Element of D
for f being Function holds eqSupport (f,X) = () /\ X;

definition
let A be Preorder;
let X be Element of ();
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 () & Y = X & it = eqSupport (f,Y) );
existence
ex b1 being Subset of A ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of () & Y = X & b1 = eqSupport (f,Y) )
proof end;
uniqueness
for b1, b2 being Subset of A st ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of () & Y = X & b1 = eqSupport (f,Y) ) & ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of () & Y = X & b2 = eqSupport (f,Y) ) holds
b1 = b2
;
end;

:: deftheorem Def12 defines eqSupport ORDERS_5:def 12 :
for A being Preorder
for X being Element of ()
for f being Function
for b4 being Subset of A holds
( b4 = eqSupport (f,X) iff ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of () & Y = X & b4 = eqSupport (f,Y) ) );

definition
let A be Preorder;
let X be Element of ();
let f be Function;
redefine func eqSupport (f,X) equals :: ORDERS_5:def 13
() /\ X;
correctness
compatibility
for b1 being Subset of A holds
( b1 = eqSupport (f,X) iff b1 = () /\ X )
;
proof end;
end;

:: deftheorem defines eqSupport ORDERS_5:def 13 :
for A being Preorder
for X being Element of ()
for f being Function holds eqSupport (f,X) = () /\ X;

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 ;
correctness
coherence
eqSupport (f,X) is finite
;
;
end;

registration
let A be Preorder;
let f be finite-support Function;
let X be Element of ();
cluster eqSupport (f,X) -> finite ;
correctness
coherence
eqSupport (f,X) is finite
;
;
end;

registration
let A be Order;
let X be Element of the carrier of ();
let f be finite-support Function of A,REAL;
cluster eqSupport (f,X) -> trivial ;
coherence
eqSupport (f,X) is 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 ()
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))));
existence
ex b1 being Function of D,REAL st
for X being Element of D st X in D holds
b1 . X = Sum (f * (canFS (eqSupport (f,X))))
proof end;
uniqueness
for b1, b2 being Function of D,REAL st ( for X being Element of D st X in D holds
b1 . X = Sum (f * (canFS (eqSupport (f,X)))) ) & ( for X being Element of D st X in D holds
b2 . X = Sum (f * (canFS (eqSupport (f,X)))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines eqSumOf ORDERS_5:def 14 :
for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL
for b4 being Function of D,REAL holds
( b4 = D eqSumOf f iff for X being Element of D st X in D holds
b4 . X = Sum (f * (canFS (eqSupport (f,X)))) );

definition
let A be Preorder;
let f be finite-support Function of A,REAL;
func eqSumOf f -> Function of (),REAL means :Def15: :: ORDERS_5:def 15
ex D being a_partition of the carrier of A st
( D = the carrier of () & it = D eqSumOf f );
existence
ex b1 being Function of (),REAL ex D being a_partition of the carrier of A st
( D = the carrier of () & b1 = D eqSumOf f )
proof end;
uniqueness
for b1, b2 being Function of (),REAL st ex D being a_partition of the carrier of A st
( D = the carrier of () & b1 = D eqSumOf f ) & ex D being a_partition of the carrier of A st
( D = the carrier of () & b2 = D eqSumOf f ) holds
b1 = b2
;
end;

:: deftheorem Def15 defines eqSumOf ORDERS_5:def 15 :
for A being Preorder
for f being finite-support Function of A,REAL
for b3 being Function of (),REAL holds
( b3 = eqSumOf f iff ex D being a_partition of the carrier of A st
( D = the carrier of () & b3 = D eqSumOf f ) );

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 () st X in the carrier of () holds
it . X = Sum (f * (canFS (eqSupport (f,X))));
correctness
compatibility
for b1 being Function of (),REAL holds
( b1 = eqSumOf f iff for X being Element of () st X in the carrier of () holds
b1 . X = Sum (f * (canFS (eqSupport (f,X)))) )
;
proof end;
end;

:: deftheorem Def16 defines eqSumOf ORDERS_5:def 16 :
for A being Preorder
for f being finite-support Function of A,REAL
for b3 being Function of (),REAL holds
( b3 = eqSumOf f iff for X being Element of () st X in the carrier of () holds
b3 . X = Sum (f * (canFS (eqSupport (f,X)))) );

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) = - ()
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;
coherence
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;
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
(() * (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 () * (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 () c= (proj A) .: ()
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) .: ()
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 ()
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 (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 ()
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 (D eqSumOf f)
proof end;

registration
let A be Preorder;
let f be finite-support Function of A,REAL;
coherence
proof end;
end;

registration
let A be set ;
let D be a_partition of A;
let f be finite-support Function of A,REAL;
coherence
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 () st rng s1 = support f & rng s2 = support () holds
Sum (() * 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 :
for A being RelStr
for s being FinSequence of A holds
( s is weakly-ascending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <= s /. m );

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 :
for A being RelStr
for s being FinSequence of A holds
( s is ascending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <~ s /. m );

:: 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;
coherence
for b1 being FinSequence of A st b1 is ascending holds
b1 is weakly-ascending
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;
correctness
compatibility
( s is ascending iff 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 :
for A being antisymmetric RelStr
for s being FinSequence of A holds
( s is ascending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n < s /. m );

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 :
for A being RelStr
for s being FinSequence of A holds
( s is weakly-descending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m <= s /. n );

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 :
for A being RelStr
for s being FinSequence of A holds
( s is descending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m <~ s /. n );

registration
let A be RelStr ;
cluster descending -> weakly-descending for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is descending holds
b1 is weakly-descending
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;
correctness
compatibility
( s is descending iff 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 :
for A being antisymmetric RelStr
for s being FinSequence of A holds
( s is descending iff for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. m < s /. n );

registration
let A be antisymmetric RelStr ;
cluster one-to-one weakly-ascending -> ascending for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is one-to-one & b1 is weakly-ascending holds
b1 is ascending
proof end;
cluster one-to-one weakly-descending -> descending for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is one-to-one & b1 is weakly-descending holds
b1 is descending
proof end;
end;

registration
let A be antisymmetric RelStr ;
coherence
for b1 being FinSequence of A st b1 is weakly-ascending & b1 is weakly-descending holds
b1 is constant
proof end;
end;

registration
let A be reflexive RelStr ;
coherence
for b1 being FinSequence of A st b1 is constant holds
( b1 is weakly-ascending & b1 is weakly-descending )
proof end;
end;

registration
let A be RelStr ;
coherence
( <*> the carrier of A is ascending & <*> the carrier of A is weakly-ascending & <*> the carrier of A is descending & <*> the carrier of A is weakly-descending )
;
end;

registration
let A be RelStr ;
existence
ex b1 being FinSequence of A st
( b1 is empty & b1 is ascending & b1 is weakly-ascending & b1 is descending & b1 is weakly-descending )
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;
coherence
for b1 being FinSequence of A st b1 = <*x*> holds
( b1 is ascending & b1 is weakly-ascending & b1 is descending & b1 is weakly-descending )
by Th72;
end;

registration
let A be non empty RelStr ;
existence
ex b1 being FinSequence of A st
( not b1 is empty & b1 is one-to-one & b1 is ascending & b1 is weakly-ascending & b1 is descending & b1 is weakly-descending )
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 :
for A being RelStr
for s being FinSequence of A holds
( s is asc_ordering iff ( s is one-to-one & s is weakly-ascending ) );

:: deftheorem defines desc_ordering ORDERS_5:def 24 :
for A being RelStr
for s being FinSequence of A holds
( s is desc_ordering iff ( s is one-to-one & s is weakly-descending ) );

registration
let A be RelStr ;
cluster asc_ordering -> one-to-one weakly-ascending for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is asc_ordering holds
( b1 is one-to-one & b1 is weakly-ascending )
;
cluster one-to-one weakly-ascending -> asc_ordering for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is one-to-one & b1 is weakly-ascending holds
b1 is asc_ordering
;
coherence
for b1 being FinSequence of A st b1 is desc_ordering holds
( b1 is one-to-one & b1 is weakly-descending )
;
coherence
for b1 being FinSequence of A st b1 is one-to-one & b1 is weakly-descending holds
b1 is desc_ordering
;
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;
coherence
for b1 being FinSequence of A st b1 is ascending holds
b1 is asc_ordering
proof end;
cluster descending -> desc_ordering for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is descending holds
b1 is desc_ordering
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 :
for A being RelStr
for B being Subset of A
for s being FinSequence of A holds
( s is B -asc_ordering iff ( s is asc_ordering & rng s = B ) );

:: deftheorem defines -desc_ordering ORDERS_5:def 26 :
for A being RelStr
for B being Subset of A
for s being FinSequence of A holds
( s is B -desc_ordering iff ( s is desc_ordering & rng s = B ) );

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
for b1 being FinSequence of A st b1 is B -asc_ordering holds
b1 is asc_ordering
;
cluster B -desc_ordering -> desc_ordering for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is B -desc_ordering holds
b1 is desc_ordering
;
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
for b1 being FinSequence of A st b1 is B -asc_ordering holds
b1 is empty
;
cluster B -desc_ordering -> empty for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is B -desc_ordering holds
b1 is empty
;
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
for b1 being FinSequence of A st b1 is asc_ordering holds
b1 is ascending
;
cluster desc_ordering -> descending for FinSequence of the carrier of A;
coherence
for b1 being FinSequence of A st b1 is desc_ordering holds
b1 is descending
;
end;

theorem Th77: :: ORDERS_5:65
for A being antisymmetric RelStr
for B being Subset of A
for s1, s2 being FinSequence of A st s1 is B -asc_ordering & s2 is B -asc_ordering holds
s1 = s2
proof end;

theorem :: ORDERS_5:66
for A being antisymmetric RelStr
for B being Subset of A
for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds
s1 = s2
proof end;

theorem Th79: :: ORDERS_5:67
for A being LinearOrder
for B being finite Subset of A
for s being FinSequence of A holds
( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )
proof end;

registration
let A be LinearOrder;
let B be finite Subset of A;
cluster SgmX ( the InternalRel of A,B) -> B -asc_ordering ;
coherence
SgmX ( the InternalRel of A,B) is B -asc_ordering
by Th79;
end;

theorem Th80: :: ORDERS_5:68
for A being RelStr
for B, C being Subset of A
for s being FinSequence of A st s is B -asc_ordering & C c= B holds
ex s2 being FinSequence of A st s2 is C -asc_ordering
proof end;

theorem :: ORDERS_5:69
for A being RelStr
for B, C being Subset of A
for s being FinSequence of A st s is B -desc_ordering & C c= B holds
ex s2 being FinSequence of A st s2 is C -desc_ordering
proof end;

theorem Th82: :: ORDERS_5:70
for A being RelStr
for B being Subset of A
for s being FinSequence of A
for x being Element of A st B = {x} & s = <*x*> holds
( s is B -asc_ordering & s is B -desc_ordering )
proof end;

theorem Th83: :: ORDERS_5:71
for A being RelStr
for B being Subset of A
for s being FinSequence of A st s is B -asc_ordering holds
the InternalRel of A is_connected_in B
proof end;

theorem :: ORDERS_5:72
for A being RelStr
for B being Subset of A
for s being FinSequence of A st s is B -desc_ordering holds
the InternalRel of A is_connected_in B
proof end;

theorem Th85: :: ORDERS_5:73
for A being transitive RelStr
for B, C being Subset of A
for s1 being FinSequence of A
for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds
x <= y ) holds
ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & s2 is B -asc_ordering )
proof end;

theorem Th86: :: ORDERS_5:74
for A being transitive RelStr
for B, C being Subset of A
for s1 being FinSequence of A
for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds
y <= x ) holds
ex s2 being FinSequence of A st
( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )
proof end;

theorem :: ORDERS_5:75
for A being transitive RelStr
for B, C being Subset of A
for s1 being FinSequence of A
for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds
x <= y ) holds
ex s2 being FinSequence of A st
( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )
proof end;

theorem :: ORDERS_5:76
for A being transitive RelStr
for B, C being Subset of A
for s1 being FinSequence of A
for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds
y <= x ) holds
ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & s2 is B -desc_ordering )
proof end;

theorem Th89: :: ORDERS_5:77
for A being transitive RelStr
for B being finite Subset of A st the InternalRel of A is_connected_in B holds
ex s being FinSequence of A st s is B -asc_ordering
proof end;

theorem :: ORDERS_5:78
for A being transitive RelStr
for B being finite Subset of A st the InternalRel of A is_connected_in B holds
ex s being FinSequence of A st s is B -desc_ordering
proof end;

theorem Th91: :: ORDERS_5:79
for A being transitive connected RelStr
for B being finite Subset of A ex s being FinSequence of A st s is B -asc_ordering
proof end;

theorem Th92: :: ORDERS_5:80
for A being transitive connected RelStr
for B being finite Subset of A ex s being FinSequence of A st s is B -desc_ordering
proof end;

registration
let A be transitive connected RelStr ;
let B be finite Subset of A;
existence
ex b1 being FinSequence of A st b1 is B -asc_ordering
by Th91;
existence
ex b1 being FinSequence of A st b1 is B -desc_ordering
by Th92;
end;

theorem Th93: :: ORDERS_5:81
for A being Preorder
for B being Subset of A st the InternalRel of A is_connected_in B holds
the InternalRel of () is_connected_in (proj A) .: B
proof end;

theorem Th94: :: ORDERS_5:82
for A being Preorder
for B being Subset of A
for s1 being FinSequence of A st s1 is B -asc_ordering holds
ex s2 being FinSequence of () st s2 is (proj A) .: B -asc_ordering
proof end;

theorem :: ORDERS_5:83
for A being Preorder
for B being Subset of A
for s1 being FinSequence of A st s1 is B -desc_ordering holds
ex s2 being FinSequence of () st s2 is (proj A) .: B -desc_ordering
proof end;