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


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

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

registration
cluster non empty V87() reflexive transitive antisymmetric for Chain ;
existence
not for b1 being Chain holds b1 is empty
proof end;
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 ;
attr L is countable means :: ORDERS_4:def 2
 the carrier of L is countable ;
end;

:: deftheorem 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 V87() reflexive transitive antisymmetric for Chain ;
existence
ex b1 being Chain st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
cluster V87() reflexive transitive antisymmetric countable for Chain ;
existence
ex b1 being Chain st b1 is countable
proof end;
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 ;
proof end;
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 ;
proof end;
end;

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

definition
let L be RelStr ;
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 ) );
end;

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

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

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 = {} ) )
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 )
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
proof end;