:: by Sebastian Koch

::

:: Received June 27, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

:: into SUBSET_1 ?

:: into RELAT_1 ? present in FOMODEL0

registration

let Y be set ;

let X be Subset of Y;

coherence

for b_{1} being Relation st b_{1} is X -defined holds

b_{1} is Y -defined
by RELAT_1:182;

end;
let X be Subset of Y;

coherence

for b

b

:: placement in CARD_2 also seems appropriate because of CARD_2:60

:: into FINSEQ_1 ?

:: interesting enough, trivdemo didn't recognized this one as trivial

:: interesting enough, trivdemo didn't recognized this one as trivial

:: into FINSEQ_1 ?

registration

let s be FinSequence;

let N be Subset of (dom s);

coherence

s * (Sgm N) is FinSequence-like

end;
let N be Subset of (dom s);

coherence

s * (Sgm N) is FinSequence-like

proof end;

:: into FINSEQ_2 ?

:: compare FINSEQ_2:32

:: 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

g * f is FinSequence-like

end;
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

g * f is FinSequence-like

proof end;

:: into FINSEQ_2 ?

registration
end;

:: into FINSEQ_5 ?

:: into FINSET_1 ?

:: into STRUCT_0 ?

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

:: 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;
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;

::$CT

:: into RVSUM_1 ?

:: into RVSUM_1 ?

:: into RVSUM_1 ?

:: similar to RVSUM_1:85

:: 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

( 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

:: 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

( 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)

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

g * f is positive-yielding

end;
let f be Function;

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

coherence

g * f is positive-yielding

proof end;

:: into PARTFUN3 ?

registration

let X be set ;

let f be Function;

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

coherence

g * f is negative-yielding

end;
let f be Function;

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

coherence

g * f is negative-yielding

proof end;

:: into PARTFUN3 ?

registration

let X be set ;

let f be Function;

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

coherence

g * f is nonpositive-yielding

end;
let f be Function;

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

coherence

g * f is nonpositive-yielding

proof end;

:: into PARTFUN3 ?

registration

let X be set ;

let f be Function;

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

coherence

g * f is nonnegative-yielding

end;
let f be Function;

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

coherence

g * f is nonnegative-yielding

proof 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;
:: original: support

redefine func support s -> Subset of (dom s);

coherence

support s is Subset of (dom s) by PRE_POLY:37;

::: into PRE_POLY ?

registration

let X be set ;

ex b_{1} being Function of X,REAL st

( b_{1} is finite-support & b_{1} is nonnegative-yielding )

end;
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));

existence ex b

( b

proof end;

::: into PRE_POLY ?

registration

let X be set ;

ex b_{1} being Function of X,COMPLEX st

( b_{1} is nonnegative-yielding & b_{1} is finite-support )

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

existence ex b

( b

proof end;

:: into CFUNCT_1 ?

:: into CFUNCT_1 ?

registration

let A be set ;

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

coherence

- f is finite-support

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

coherence

- f is finite-support

proof end;

:: into CFUNCT_1 as a consequence?

registration

let A be set ;

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

coherence

- f is finite-support

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

coherence

- f is finite-support

proof 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

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

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

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 ;

end;
attr A is connected means :Def1: :: ORDERS_5:def 1

the InternalRel of A is_connected_in the carrier of A;

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;

the InternalRel of A is_strongly_connected_in the carrier of A;

:: 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 );

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 );

for A being RelStr holds

( A is strongly_connected iff the InternalRel of A is_strongly_connected_in the carrier of A );

registration

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is connected & b_{1} is strongly_connected & b_{1} is strict & b_{1} is total )
end;

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

existence ex b

( not b

proof end;

registration

coherence

for b_{1} being RelStr st b_{1} is strongly_connected holds

( b_{1} is reflexive & b_{1} is connected )

end;
for b

( b

proof end;

registration

coherence

for b_{1} being RelStr st b_{1} is reflexive & b_{1} is connected holds

b_{1} is strongly_connected

end;
for b

b

proof end;

registration

coherence

for b_{1} being RelStr st b_{1} is empty holds

( b_{1} is reflexive & b_{1} is antisymmetric & b_{1} is transitive & b_{1} is connected & b_{1} is strongly_connected )

end;
for b

( b

proof 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 ) );

for A being RelStr

for a1, a2 being Element of A holds

( a1 =~ a2 iff ( a1 <= a2 & a2 <= a1 ) );

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,b_{1},b_{1})
by Th22;

end;
let a1, a2 be Element of A;

:: original: =~

redefine pred a1 =~ a2;

reflexivity

for a1 being Element of A holds (A,b

definition

let A be RelStr ;

let a1, a2 be Element of A;

irreflexivity

for a1 being Element of A holds

( not a1 <= a1 or a1 <= a1 ) ;

end;
let a1, a2 be Element of A;

irreflexivity

for a1 being Element of A holds

( not a1 <= a1 or a1 <= a1 ) ;

:: 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 ) );

for A being RelStr

for a1, a2 being Element of A holds

( a1 <~ a2 iff ( a1 <= a2 & not a2 <= a1 ) );

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,b_{1},b_{2}) holds

not (A,b_{2},b_{1})
;

end;
let a1, a2 be Element of A;

:: original: <~

redefine pred a1 <~ a2;

asymmetry

for a1, a2 being Element of A st (A,b

not (A,b

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 )

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;

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 )

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

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

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 )

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 )

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

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 ) )

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 ) )

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 ) )

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 ) )

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;
mode LinearPreorder is transitive strongly_connected RelStr ;

mode Order is reflexive transitive antisymmetric RelStr ;

mode LinearOrder is transitive antisymmetric strongly_connected RelStr ;

registration

ex b_{1} being LinearOrder st b_{1} is empty
end;

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

existence ex b

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;

( 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;

( 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 )

( A is reflexive & A is transitive & A is antisymmetric & A is connected )

proof end;

scheme :: ORDERS_5:sch 2

RelStrMin{ F_{1}() -> transitive connected RelStr , F_{2}() -> finite Subset of F_{1}(), P_{1}[ Element of F_{1}()] } :

RelStrMin{ F

ex x being Element of F_{1}() st

( x in F_{2}() & P_{1}[x] & ( for y being Element of F_{1}() st y in F_{2}() & y <~ x holds

not P_{1}[y] ) )

provided
( x in F

not P

proof end;

scheme :: ORDERS_5:sch 3

RelStrMax{ F_{1}() -> transitive connected RelStr , F_{2}() -> finite Subset of F_{1}(), P_{1}[ Element of F_{1}()] } :

RelStrMax{ F

ex x being Element of F_{1}() st

( x in F_{2}() & P_{1}[x] & ( for y being Element of F_{1}() st y in F_{2}() & x <~ y holds

not P_{1}[y] ) )

provided
( x in F

not P

proof end;

definition

let A be Preorder;

ex b_{1} being Equivalence_Relation of the carrier of A st

for x, y being Element of A holds

( [x,y] in b_{1} iff ( x <= y & y <= x ) )

for b_{1}, b_{2} being Equivalence_Relation of the carrier of A st ( for x, y being Element of A holds

( [x,y] in b_{1} iff ( x <= y & y <= x ) ) ) & ( for x, y being Element of A holds

( [x,y] in b_{2} iff ( x <= y & y <= x ) ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of A holds

( [x,y] in it iff ( x <= y & y <= x ) );

ex b

for x, y being Element of A holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def6 defines EqRelOf ORDERS_5:def 6 :

for A being Preorder

for b_{2} being Equivalence_Relation of the carrier of A holds

( b_{2} = EqRelOf A iff for x, y being Element of A holds

( [x,y] in b_{2} iff ( x <= y & y <= x ) ) );

for A being Preorder

for b

( b

( [x,y] in b

registration
end;

registration
end;

definition

let A be Preorder;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of b_{1} iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of b_{1} iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) & the carrier of b_{2} = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of b_{2} iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) holds

b_{1} = b_{2}

end;
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 ) ) ) );

existence ( 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 ) ) ) );

ex b

( the carrier of b

( [X,Y] in the InternalRel of b

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) )

proof end;

uniqueness for b

( [X,Y] in the InternalRel of b

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) & the carrier of b

( [X,Y] in the InternalRel of b

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) holds

b

proof end;

:: deftheorem Def7 defines QuotientOrder ORDERS_5:def 7 :

for A being Preorder

for b_{2} being strict RelStr holds

( b_{2} = QuotientOrder A iff ( the carrier of b_{2} = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of b_{2} iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) ) );

for A being Preorder

for b

( b

( [X,Y] in the InternalRel of b

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) ) );

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)

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

proof end;

registration

let A be Preorder;

coherence

( QuotientOrder A is reflexive & QuotientOrder A is total & QuotientOrder A is antisymmetric & QuotientOrder A is transitive )

end;
coherence

( QuotientOrder A is reflexive & QuotientOrder A is total & QuotientOrder A is antisymmetric & QuotientOrder A is transitive )

proof end;

:: this generalizes DICKSON:10 to possibly empty RelStr

registration

let A be LinearPreorder;

coherence

( QuotientOrder A is connected & QuotientOrder A is strongly_connected )

end;
coherence

( QuotientOrder A is connected & QuotientOrder A is strongly_connected )

proof end;

definition

let A be Preorder;

ex b_{1} being Function of A,(QuotientOrder A) st

for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x)

for b_{1}, b_{2} being Function of A,(QuotientOrder A) st ( for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds b_{2} . x = Class ((EqRelOf A),x) ) holds

b_{1} = b_{2}

end;
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);

existence for x being Element of A holds it . x = Class ((EqRelOf A),x);

ex b

for x being Element of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines proj ORDERS_5:def 8 :

for A being Preorder

for b_{2} being Function of A,(QuotientOrder A) holds

( b_{2} = proj A iff for x being Element of A holds b_{2} . x = Class ((EqRelOf A),x) );

for A being Preorder

for b

( b

registration
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

for x, y being Element of A st x <= y holds

(proj A) . x <= (proj A) . y

proof 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 );

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;

ex b_{1} being Equivalence_Relation of the carrier of A st b_{1} is EqRelOf-like

end;
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 b

proof 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

Im (R,x) is Element of (QuotientOrder A)

end;
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

Im (R,x) is Element of (QuotientOrder 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

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;

correctness

coherence

RelStr(# A,(ERl D) #) is strict RelStr ;

;

end;
let D be a_partition of A;

correctness

coherence

RelStr(# A,(ERl D) #) is strict RelStr ;

;

:: 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) #);

for A being set

for D being a_partition of A holds PreorderFromPartition D = RelStr(# A,(ERl D) #);

registration
end;

registration

let A be set ;

let D be a_partition of A;

coherence

( PreorderFromPartition D is reflexive & PreorderFromPartition D is transitive ) ;

coherence

PreorderFromPartition D is symmetric

end;
let D be a_partition of A;

coherence

( PreorderFromPartition D is reflexive & PreorderFromPartition D is transitive ) ;

coherence

PreorderFromPartition D is symmetric

proof end;

Def5: for A being set

for D being a_partition of A holds Class (ERl D) = D

by PARTIT1:38;

theorem Th51: :: ORDERS_5:42

for A being set

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

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;

correctness

coherence

(support f) /\ X is Subset of A;

end;
let D be a_partition of A;

let X be Element of D;

let f be Function;

correctness

coherence

(support f) /\ X is Subset of A;

proof 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) = (support f) /\ X;

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) = (support f) /\ X;

definition

let A be Preorder;

let X be Element of (QuotientOrder A);

let f be Function;

ex b_{1} 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 (QuotientOrder A) & Y = X & b_{1} = eqSupport (f,Y) )

for b_{1}, b_{2} 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 (QuotientOrder A) & Y = X & b_{1} = eqSupport (f,Y) ) & 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 & b_{2} = eqSupport (f,Y) ) holds

b_{1} = b_{2}
;

end;
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) );

existence 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) );

ex b

( D = the carrier of (QuotientOrder A) & Y = X & b

proof end;

uniqueness for b

( D = the carrier of (QuotientOrder A) & Y = X & b

( D = the carrier of (QuotientOrder A) & Y = X & b

b

:: deftheorem Def12 defines eqSupport ORDERS_5:def 12 :

for A being Preorder

for X being Element of (QuotientOrder A)

for f being Function

for b_{4} being Subset of A holds

( b_{4} = 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 (QuotientOrder A) & Y = X & b_{4} = eqSupport (f,Y) ) );

for A being Preorder

for X being Element of (QuotientOrder A)

for f being Function

for b

( b

( D = the carrier of (QuotientOrder A) & Y = X & b

definition

let A be Preorder;

let X be Element of (QuotientOrder A);

let f be Function;

correctness

compatibility

for b_{1} being Subset of A holds

( b_{1} = eqSupport (f,X) iff b_{1} = (support f) /\ X );

end;
let X be Element of (QuotientOrder A);

let f be Function;

correctness

compatibility

for b

( b

proof end;

:: deftheorem defines eqSupport ORDERS_5:def 13 :

for A being Preorder

for X being Element of (QuotientOrder A)

for f being Function holds eqSupport (f,X) = (support f) /\ X;

for A being Preorder

for X being Element of (QuotientOrder A)

for f being Function holds eqSupport (f,X) = (support f) /\ 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;

correctness

coherence

eqSupport (f,X) is finite ;

;

end;
let D be a_partition of A;

let f be finite-support Function;

let X be Element of D;

correctness

coherence

eqSupport (f,X) is finite ;

;

registration

let A be Preorder;

let f be finite-support Function;

let X be Element of (QuotientOrder A);

correctness

coherence

eqSupport (f,X) is finite ;

;

end;
let f be finite-support Function;

let X be Element of (QuotientOrder A);

correctness

coherence

eqSupport (f,X) is finite ;

;

registration

let A be Order;

let X be Element of the carrier of (QuotientOrder A);

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

coherence

eqSupport (f,X) is trivial

end;
let X be Element of the carrier of (QuotientOrder A);

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

coherence

eqSupport (f,X) is trivial

proof 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)

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)

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;

ex b_{1} being Function of D,REAL st

for X being Element of D st X in D holds

b_{1} . X = Sum (f * (canFS (eqSupport (f,X))))

for b_{1}, b_{2} being Function of D,REAL st ( for X being Element of D st X in D holds

b_{1} . X = Sum (f * (canFS (eqSupport (f,X)))) ) & ( for X being Element of D st X in D holds

b_{2} . X = Sum (f * (canFS (eqSupport (f,X)))) ) holds

b_{1} = b_{2}

end;
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 for X being Element of D st X in D holds

it . X = Sum (f * (canFS (eqSupport (f,X))));

ex b

for X being Element of D st X in D holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being Function of D,REAL holds

( b_{4} = D eqSumOf f iff for X being Element of D st X in D holds

b_{4} . X = Sum (f * (canFS (eqSupport (f,X)))) );

for A being set

for D being a_partition of A

for f being finite-support Function of A,REAL

for b

( b

b

definition

let A be Preorder;

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

ex b_{1} being Function of (QuotientOrder A),REAL ex D being a_partition of the carrier of A st

( D = the carrier of (QuotientOrder A) & b_{1} = D eqSumOf f )

for b_{1}, b_{2} being Function of (QuotientOrder A),REAL st ex D being a_partition of the carrier of A st

( D = the carrier of (QuotientOrder A) & b_{1} = D eqSumOf f ) & ex D being a_partition of the carrier of A st

( D = the carrier of (QuotientOrder A) & b_{2} = D eqSumOf f ) holds

b_{1} = b_{2}
;

end;
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 );

existence ex D being a_partition of the carrier of A st

( D = the carrier of (QuotientOrder A) & it = D eqSumOf f );

ex b

( D = the carrier of (QuotientOrder A) & b

proof end;

uniqueness for b

( D = the carrier of (QuotientOrder A) & b

( D = the carrier of (QuotientOrder A) & b

b

:: deftheorem Def15 defines eqSumOf ORDERS_5:def 15 :

for A being Preorder

for f being finite-support Function of A,REAL

for b_{3} being Function of (QuotientOrder A),REAL holds

( b_{3} = eqSumOf f iff ex D being a_partition of the carrier of A st

( D = the carrier of (QuotientOrder A) & b_{3} = D eqSumOf f ) );

for A being Preorder

for f being finite-support Function of A,REAL

for b

( b

( D = the carrier of (QuotientOrder A) & b

definition

let A be Preorder;

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

compatibility

for b_{1} being Function of (QuotientOrder A),REAL holds

( b_{1} = eqSumOf f iff for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds

b_{1} . X = Sum (f * (canFS (eqSupport (f,X)))) );

end;
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))));

correctness for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds

it . X = Sum (f * (canFS (eqSupport (f,X))));

compatibility

for b

( b

b

proof end;

:: deftheorem Def16 defines eqSumOf ORDERS_5:def 16 :

for A being Preorder

for f being finite-support Function of A,REAL

for b_{3} being Function of (QuotientOrder A),REAL holds

( b_{3} = eqSumOf f iff for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds

b_{3} . X = Sum (f * (canFS (eqSupport (f,X)))) );

for A being Preorder

for f being finite-support Function of A,REAL

for b

( b

b

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)

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)

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;

coherence

eqSumOf f is nonnegative-yielding

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

coherence

eqSumOf f is nonnegative-yielding

proof 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

D eqSumOf f is nonnegative-yielding by Th56;

end;
let D be a_partition of A;

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

coherence

D eqSumOf f is nonnegative-yielding by Th56;

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

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

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

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 :: 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

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)

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)

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)

:: 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)

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)

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)

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)

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;

coherence

eqSumOf f is finite-support

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

coherence

eqSumOf f is finite-support

proof end;

registration

let A be set ;

let D be a_partition of A;

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

coherence

D eqSumOf f is finite-support

end;
let D be a_partition of A;

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

coherence

D eqSumOf f is finite-support

proof 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)

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)

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)

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;

:: 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 );

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 );

:: 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 );

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 ;

coherence

for b_{1} being FinSequence of A st b_{1} is ascending holds

b_{1} is weakly-ascending

end;
coherence

for b

b

proof end;

definition

let A be antisymmetric RelStr ;

let s be FinSequence of A;

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 );

end;
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 for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. n < s /. m;

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;

:: 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 );

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 );

:: 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 );

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 );

:: 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 );

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 ;

coherence

for b_{1} being FinSequence of A st b_{1} is descending holds

b_{1} is weakly-descending

end;
coherence

for b

b

proof end;

definition

let A be antisymmetric RelStr ;

let s be FinSequence of A;

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 );

end;
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 for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. m < s /. n;

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;

:: 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 );

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 ;

coherence

for b_{1} being FinSequence of A st b_{1} is one-to-one & b_{1} is weakly-ascending holds

b_{1} is ascending

for b_{1} being FinSequence of A st b_{1} is one-to-one & b_{1} is weakly-descending holds

b_{1} is descending

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let A be antisymmetric RelStr ;

coherence

for b_{1} being FinSequence of A st b_{1} is weakly-ascending & b_{1} is weakly-descending holds

b_{1} is constant

end;
coherence

for b

b

proof end;

registration

let A be reflexive RelStr ;

coherence

for b_{1} being FinSequence of A st b_{1} is constant holds

( b_{1} is weakly-ascending & b_{1} is weakly-descending )

end;
coherence

for b

( b

proof 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;
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 ) ;

registration

let A be RelStr ;

ex b_{1} being FinSequence of A st

( b_{1} is empty & b_{1} is ascending & b_{1} is weakly-ascending & b_{1} is descending & b_{1} is weakly-descending )

end;
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;

existence ex b

( b

proof 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 b_{1} being FinSequence of A st b_{1} = <*x*> holds

( b_{1} is ascending & b_{1} is weakly-ascending & b_{1} is descending & b_{1} is weakly-descending )
by Th72;

end;
let x be Element of A;

coherence

for b

( b

registration

let A be non empty RelStr ;

ex b_{1} being FinSequence of A st

( not b_{1} is empty & b_{1} is one-to-one & b_{1} is ascending & b_{1} is weakly-ascending & b_{1} is descending & b_{1} is weakly-descending )

end;
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;

existence ex b

( not b

proof 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 ) );

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 ) );

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 ;

coherence

for b_{1} being FinSequence of A st b_{1} is asc_ordering holds

( b_{1} is one-to-one & b_{1} is weakly-ascending )
;

coherence

for b_{1} being FinSequence of A st b_{1} is one-to-one & b_{1} is weakly-ascending holds

b_{1} is asc_ordering
;

coherence

for b_{1} being FinSequence of A st b_{1} is desc_ordering holds

( b_{1} is one-to-one & b_{1} is weakly-descending )
;

coherence

for b_{1} being FinSequence of A st b_{1} is one-to-one & b_{1} is weakly-descending holds

b_{1} is desc_ordering
;

end;
coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

:: I thought the following registration would only work with trasitivity

:: but apparently ascending implies asc_ordering

:: but apparently ascending implies asc_ordering

registration

let A be RelStr ;

coherence

for b_{1} being FinSequence of A st b_{1} is ascending holds

b_{1} is asc_ordering

for b_{1} being FinSequence of A st b_{1} is descending holds

b_{1} is desc_ordering

end;
coherence

for b

b

proof end;

coherence for b

b

proof 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 ) );

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 ) );

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;

coherence

for b_{1} being FinSequence of A st b_{1} is B -asc_ordering holds

b_{1} is asc_ordering
;

coherence

for b_{1} being FinSequence of A st b_{1} is B -desc_ordering holds

b_{1} is desc_ordering
;

end;
let B be Subset of A;

coherence

for b

b

coherence

for b

b

registration

let A be RelStr ;

let B be empty Subset of A;

coherence

for b_{1} being FinSequence of A st b_{1} is B -asc_ordering holds

b_{1} is empty
;

coherence

for b_{1} being FinSequence of A st b_{1} is B -desc_ordering holds

b_{1} is empty
;

end;
let B be empty Subset of A;

coherence

for b

b

coherence

for b

b

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 )

for s being FinSequence of A holds

( s is weakly-ascending iff Rev s is weakly-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 )

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 ;

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 ;

coherence

for b_{1} being FinSequence of A st b_{1} is asc_ordering holds

b_{1} is ascending
;

coherence

for b_{1} being FinSequence of A st b_{1} is desc_ordering holds

b_{1} is descending
;

end;
coherence

for b

b

coherence

for b

b

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

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

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) )

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;

coherence

SgmX ( the InternalRel of A,B) is B -asc_ordering by Th79;

end;
let B be finite Subset of A;

coherence

SgmX ( the InternalRel of A,B) is B -asc_ordering by Th79;

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

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

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 )

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

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

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 )

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 )

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 )

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 )

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

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

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

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

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;

ex b_{1} being FinSequence of A st b_{1} is B -asc_ordering
by Th91;

ex b_{1} being FinSequence of A st b_{1} is B -desc_ordering
by Th92;

end;
let B be finite Subset of A;

cluster Relation-like NAT -defined the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like finite-support B -asc_ordering for FinSequence of the carrier of A;

existence ex b

cluster Relation-like NAT -defined the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like finite-support B -desc_ordering for FinSequence of the carrier of A;

existence ex b

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 (QuotientOrder A) is_connected_in (proj A) .: B

for B being Subset of A st the InternalRel of A is_connected_in B holds

the InternalRel of (QuotientOrder A) 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 (QuotientOrder A) st s2 is (proj A) .: B -asc_ordering

for B being Subset of A

for s1 being FinSequence of A st s1 is B -asc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) 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 (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering

for B being Subset of A

for s1 being FinSequence of A st s1 is B -desc_ordering holds

ex s2 being FinSequence of (QuotientOrder A) st s2 is (proj A) .: B -desc_ordering

proof end;