:: by Marta Pruszy\'nska and Marek Dudzicz

::

:: Received June 29, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

definition

ex b_{1} being RelStr st

( b_{1} is non empty connected Poset or b_{1} is empty )
end;

mode Chain -> RelStr means :Def1: :: ORDERS_4:def 1

( it is non empty connected Poset or it is empty );

existence ( it is non empty connected Poset or it is empty );

ex b

( b

proof end;

:: deftheorem Def1 defines Chain ORDERS_4:def 1 :

for b_{1} being RelStr holds

( b_{1} is Chain iff ( b_{1} is non empty connected Poset or b_{1} is empty ) );

for b

( b

registration

coherence

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

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

end;
for b

( b

proof end;

registration

coherence

for b_{1} being Chain holds

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

end;
for b

( b

proof end;

definition
end;

:: deftheorem defines countable ORDERS_4:def 2 :

for L being 1-sorted holds

( L is countable iff the carrier of L is countable );

for L being 1-sorted holds

( L is countable iff the carrier of L is countable );

registration
end;

registration

let A be non empty connected RelStr ;

correctness

coherence

for b_{1} being non empty SubRelStr of A st b_{1} is full holds

b_{1} is connected ;

end;
correctness

coherence

for b

b

proof end;

registration

let A be finite RelStr ;

correctness

coherence

for b_{1} being SubRelStr of A holds b_{1} is finite ;

end;
correctness

coherence

for b

proof end;

definition

let L be RelStr ;

let A, B be set ;

end;
let A, B be set ;

pred A,B form_upper_lower_partition_of L means :: ORDERS_4:def 3

( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds

a < b ) );

( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds

a < b ) );

:: deftheorem defines form_upper_lower_partition_of ORDERS_4:def 3 :

for L being RelStr

for A, B being set holds

( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds

a < b ) ) );

for L being RelStr

for A, B being set holds

( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds

a < b ) ) );

theorem Th3: :: ORDERS_4:3

for L being non empty antisymmetric upper-bounded RelStr holds the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L

proof end;

theorem Th4: :: ORDERS_4:4

for L1, L2 being RelStr

for f being Function of L1,L2 st f is isomorphic holds

( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

for f being Function of L1,L2 st f is isomorphic holds

( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

proof end;

theorem Th5: :: ORDERS_4:5

for L1, L2 being antisymmetric RelStr

for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds

for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds

for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds

for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds

for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

proof end;

theorem :: ORDERS_4:6

for A being finite Chain

for n being Nat st card the carrier of A = n holds

A, InclPoset n are_isomorphic

for n being Nat st card the carrier of A = n holds

A, InclPoset n are_isomorphic

proof end;