:: On the Isomorphism Between Finite Chains
:: by Marta Pruszy\'nska and Marek Dudzicz
::
:: Received June 29, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

definition
mode Chain  ->  RelStr  means :Def1: :: ORDERS_4:def 1
( it is non empty connected Poset or it is empty );
existence
 ex b1 being RelStr st
( b1 is non empty connected Poset or b1 is empty )
proofend;
end;

:: deftheorem Def1 defines Chain ORDERS_4:def_1_:_
 for b1 being RelStr holds
( b1 is Chain iff ( b1 is non empty connected Poset or b1 is empty ) );

registration
cluster empty  ->  reflexive transitive antisymmetric for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proofend;
end;

registration
cluster  ->  reflexive transitive antisymmetric for Chain ;
coherence
 for b1 being Chain holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proofend;
end;

registration
cluster non empty V80() reflexive transitive antisymmetric for Chain ;
existence
 not for b1 being Chain holds b1 is empty
proofend;
end;

registration
cluster non empty  ->  non empty connected for Chain ;
coherence
 for b1 being non empty Chain holds b1 is connected by Def1;
end;

definition
let L be 1-sorted ;
attrL is countable  means :Def2: :: ORDERS_4:def 2
 the carrier of L is countable ;
end;

:: deftheorem Def2 defines countable ORDERS_4:def_2_:_
 for L being 1-sorted holds
( L is countable iff the carrier of L is countable );

registration
cluster non empty finite V80() reflexive transitive antisymmetric for Chain ;
existence
 ex b1 being Chain st
( b1 is finite & not b1 is empty )
proofend;
end;

registration
clusterV80() reflexive transitive antisymmetric countable for Chain ;
existence
 ex b1 being Chain st b1 is countable
proofend;
end;

registration
let A be non empty connected RelStr ;
cluster non empty full  ->  non empty connected for SubRelStr of A;
correctness
coherence
for b1 being non empty SubRelStr of A st b1 is full holds
b1 is connected ;
proofend;
end;

registration
let A be finite RelStr ;
cluster  ->  finite for SubRelStr of A;
correctness
coherence
for b1 being SubRelStr of A holds b1 is finite ;
proofend;
end;

theorem Th1: :: ORDERS_4:1
for n, m being Nat st n <= m holds
InclPoset n is full SubRelStr of InclPoset m
proofend;

definition
let L be RelStr ;
let A, B be set ;
predA,B form_upper_lower_partition_of L means :Def3: :: ORDERS_4:def 3
( A \/ B = the carrier of L &amp; ( for a, b being Element of L st a in A &amp; b in B holds
a < b ) );
end;

:: deftheorem Def3 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 &amp; ( for a, b being Element of L st a in A &amp; b in B holds
a < b ) ) );

theorem Th2: :: ORDERS_4:2
for L being RelStr
for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
proofend;

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

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 <> {} ) &amp; ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) &amp; ( the carrier of L2 <> {} or the carrier of L1 = {} ) &amp; ( the carrier of L1 = {} implies the carrier of L2 = {} ) &amp; ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
proofend;

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 &amp; h is isomorphic )
proofend;

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