:: by Freek Wiedijk

::

:: Received August 13, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

definition

let A, B9 be non empty set ;

let B be non empty Subset of B9;

let f be Function of A,B;

let x be Element of A;

:: original: .

redefine func f . x -> Element of B;

coherence

f . x is Element of B

end;
let B be non empty Subset of B9;

let f be Function of A,B;

let x be Element of A;

:: original: .

redefine func f . x -> Element of B;

coherence

f . x is Element of B

proof end;

theorem Th1: :: ARROW:1

for A being finite set st card A >= 2 holds

for a being Element of A ex b being Element of A st b <> a

for a being Element of A ex b being Element of A st b <> a

proof end;

theorem Th2: :: ARROW:2

for A being finite set st card A >= 3 holds

for a, b being Element of A ex c being Element of A st

( c <> a & c <> b )

for a, b being Element of A ex c being Element of A st

( c <> a & c <> b )

proof end;

definition

let A be non empty set ;

defpred S_{1}[ set ] means ( $1 is Relation of A & ( for a, b being Element of A holds

( [a,b] in $1 or [b,a] in $1 ) ) & ( for a, b, c being Element of A st [a,b] in $1 & [b,c] in $1 holds

[a,c] in $1 ) );

defpred S_{2}[ set ] means for R being set holds

( R in $1 iff S_{1}[R] );

ex b_{1} being set st

for R being set holds

( R in b_{1} iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) )

for b_{1}, b_{2} being set st ( for R being set holds

( R in b_{1} iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) ) & ( for R being set holds

( R in b_{2} iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) ) holds

b_{1} = b_{2}

end;
defpred S

( [a,b] in $1 or [b,a] in $1 ) ) & ( for a, b, c being Element of A st [a,b] in $1 & [b,c] in $1 holds

[a,c] in $1 ) );

defpred S

( R in $1 iff S

func LinPreorders A -> set means :Def1: :: ARROW:def 1

for R being set holds

( R in it iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) );

existence for R being set holds

( R in it iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) );

ex b

for R being set holds

( R in b

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) )

proof end;

uniqueness for b

( R in b

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) ) & ( for R being set holds

( R in b

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) ) holds

b

proof end;

:: deftheorem Def1 defines LinPreorders ARROW:def 1 :

for A being non empty set

for b_{2} being set holds

( b_{2} = LinPreorders A iff for R being set holds

( R in b_{2} iff ( R is Relation of A & ( for a, b being Element of A holds

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) );

for A being non empty set

for b

( b

( R in b

( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds

[a,c] in R ) ) ) );

definition

let A be non empty set ;

defpred S_{1}[ set ] means for a, b being Element of A st [a,b] in $1 & [b,a] in $1 holds

a = b;

defpred S_{2}[ set ] means for R being Element of LinPreorders A holds

( R in $1 iff S_{1}[R] );

ex b_{1} being Subset of (LinPreorders A) st

for R being Element of LinPreorders A holds

( R in b_{1} iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b )

for b_{1}, b_{2} being Subset of (LinPreorders A) st ( for R being Element of LinPreorders A holds

( R in b_{1} iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b ) ) & ( for R being Element of LinPreorders A holds

( R in b_{2} iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b ) ) holds

b_{1} = b_{2}

end;
defpred S

a = b;

defpred S

( R in $1 iff S

func LinOrders A -> Subset of (LinPreorders A) means :Def2: :: ARROW:def 2

for R being Element of LinPreorders A holds

( R in it iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b );

existence for R being Element of LinPreorders A holds

( R in it iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b );

ex b

for R being Element of LinPreorders A holds

( R in b

a = b )

proof end;

uniqueness for b

( R in b

a = b ) ) & ( for R being Element of LinPreorders A holds

( R in b

a = b ) ) holds

b

proof end;

:: deftheorem Def2 defines LinOrders ARROW:def 2 :

for A being non empty set

for b_{2} being Subset of (LinPreorders A) holds

( b_{2} = LinOrders A iff for R being Element of LinPreorders A holds

( R in b_{2} iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b ) );

for A being non empty set

for b

( b

( R in b

a = b ) );

registration

let A be set ;

ex b_{1} being Order of A st b_{1} is connected

end;
cluster Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive for Element of bool [:A,A:];

existence ex b

proof end;

definition

let A be non empty set ;

for b_{1} being Subset of (LinPreorders A) holds

( b_{1} = LinOrders A iff for R being set holds

( R in b_{1} iff R is connected Order of A ) )

end;
redefine func LinOrders A means :Def3: :: ARROW:def 3

for R being set holds

( R in it iff R is connected Order of A );

compatibility for R being set holds

( R in it iff R is connected Order of A );

for b

( b

( R in b

proof end;

:: deftheorem Def3 defines LinOrders ARROW:def 3 :

for A being non empty set

for b_{2} being Subset of (LinPreorders A) holds

( b_{2} = LinOrders A iff for R being set holds

( R in b_{2} iff R is connected Order of A ) );

for A being non empty set

for b

( b

( R in b

registration

let A be non empty set ;

coherence

for b_{1} being Element of LinPreorders A holds b_{1} is Relation-like
by Def1;

coherence

for b_{1} being Element of LinOrders A holds b_{1} is Relation-like
;

end;
coherence

for b

coherence

for b

:: deftheorem defines <=_ ARROW:def 4 :

for o being Relation

for a, b being set holds

( a <=_ o,b iff [a,b] in o );

for o being Relation

for a, b being set holds

( a <=_ o,b iff [a,b] in o );

notation

let o be Relation;

let a, b be set ;

synonym b >=_ o,a for a <=_ o,b;

antonym b <_ o,a for a <=_ o,b;

antonym a >_ o,b for a <=_ o,b;

end;
let a, b be set ;

synonym b >=_ o,a for a <=_ o,b;

antonym b <_ o,a for a <=_ o,b;

antonym a >_ o,b for a <=_ o,b;

theorem Th5: :: ARROW:5

for A being non empty set

for a, b, c being Element of A

for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds

a <=_ o,c

for a, b, c being Element of A

for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds

a <=_ o,c

proof end;

theorem Th7: :: ARROW:7

for A being non empty set

for a, b, c being Element of A st a <> b & b <> c & a <> c holds

ex o being Element of LinPreorders A st

( a <_ o,b & b <_ o,c )

for a, b, c being Element of A st a <> b & b <> c & a <> c holds

ex o being Element of LinPreorders A st

( a <_ o,b & b <_ o,c )

proof end;

theorem Th8: :: ARROW:8

for A being non empty set

for b being Element of A ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

b <_ o,a

for b being Element of A ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

b <_ o,a

proof end;

theorem Th9: :: ARROW:9

for A being non empty set

for b being Element of A ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

a <_ o,b

for b being Element of A ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

a <_ o,b

proof end;

theorem Th10: :: ARROW:10

for A being non empty set

for a, b, c being Element of A

for o9 being Element of LinPreorders A st a <> b & a <> c holds

ex o being Element of LinPreorders A st

( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )

for a, b, c being Element of A

for o9 being Element of LinPreorders A st a <> b & a <> c holds

ex o being Element of LinPreorders A st

( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )

proof end;

theorem Th11: :: ARROW:11

for A being non empty set

for a, b, c being Element of A

for o9 being Element of LinPreorders A st a <> b & a <> c holds

ex o being Element of LinPreorders A st

( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )

for a, b, c being Element of A

for o9 being Element of LinPreorders A st a <> b & a <> c holds

ex o being Element of LinPreorders A st

( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )

proof end;

theorem :: ARROW:12

for A being non empty set

for a, b being Element of A

for o, o9 being Element of LinOrders A holds

( not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )

for a, b being Element of A

for o, o9 being Element of LinOrders A holds

( not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )

proof end;

theorem Th13: :: ARROW:13

for A being non empty set

for o being Element of LinOrders A

for o9 being Element of LinPreorders A holds

( ( for a, b being Element of A st a <_ o,b holds

a <_ o9,b ) iff for a, b being Element of A holds

( a <_ o,b iff a <_ o9,b ) )

for o being Element of LinOrders A

for o9 being Element of LinPreorders A holds

( ( for a, b being Element of A st a <_ o,b holds

a <_ o9,b ) iff for a, b being Element of A holds

( a <_ o,b iff a <_ o9,b ) )

proof end;

theorem Th14: :: ARROW:14

for A, N being non empty finite set

for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds

a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st ( for i being Element of N holds

( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds

( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds

ex n being Element of N st

for p being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st a <_ p . n,b holds

a <_ f . p,b

for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds

a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st ( for i being Element of N holds

( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds

( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds

ex n being Element of N st

for p being Element of Funcs (N,(LinPreorders A))

for a, b being Element of A st a <_ p . n,b holds

a <_ f . p,b

proof end;

theorem :: ARROW:15

for A, N being non empty finite set

for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders A))

for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds

a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))

for a, b being Element of A st ( for i being Element of N holds

( a <_ p . i,b iff a <_ p9 . i,b ) ) holds

( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds

ex n being Element of N st

for p being Element of Funcs (N,(LinOrders A))

for a, b being Element of A holds

( a <_ p . n,b iff a <_ f . p,b )

for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders A))

for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds

a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))

for a, b being Element of A st ( for i being Element of N holds

( a <_ p . i,b iff a <_ p9 . i,b ) ) holds

( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds

ex n being Element of N st

for p being Element of Funcs (N,(LinOrders A))

for a, b being Element of A holds

( a <_ p . n,b iff a <_ f . p,b )

proof end;